2009-09-21T20:58:24-04:00 equalish(X1,X2) | ~ equalish(X2,X1) cnf(22,axiom, ( equalish(X1,X2) | ~ equalish(X2,X1) ), file('/home/graph/tptp/TPTP/Axioms/FLD001-0.ax',symmetry_of_equality)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#22 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Axioms&File=FLD001-0.ax#symmetry_of_equality symmetry_of_equality 2009-09-21T20:58:24-04:00 $false cnf(42012,negated_conjecture, ( $false ), 42011, [proof]). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#42012 TPTP Formula 0 2009-09-21T20:58:24-04:00 $false cnf(42011,negated_conjecture, ( $false ), inference(sr,[status(thm)],[42010,34,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#42011 TPTP Formula 0 2009-09-21T20:58:24-04:00 ~ equalish(multiply(a,c),multiply(d,b)) cnf(34,negated_conjecture, ( ~ equalish(multiply(a,c),multiply(d,b)) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',multiply_not_equal_to_multiply_7)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#34 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#multiply_not_equal_to_multiply_7 multiply_not_equal_to_multiply_7 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(d,b)) cnf(42010,negated_conjecture, ( equalish(multiply(a,c),multiply(d,b)) ), inference(cn,[status(thm)],[42009,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#42010 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(d,b)) | $false | $false cnf(42009,negated_conjecture, ( equalish(multiply(a,c),multiply(d,b)) | $false | $false ), inference(rw,[status(thm)],[42008,29,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#42009 TPTP Formula 0 2009-09-21T20:58:24-04:00 defined(b) cnf(29,axiom, ( defined(b) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',b_is_defined)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#29 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#b_is_defined b_is_defined 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(d,b)) | $false | ~ defined(b) cnf(42008,negated_conjecture, ( equalish(multiply(a,c),multiply(d,b)) | $false | ~ defined(b) ), inference(rw,[status(thm)],[42004,31,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#42008 TPTP Formula 0 2009-09-21T20:58:24-04:00 defined(d) cnf(31,axiom, ( defined(d) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',d_is_defined)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#31 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#d_is_defined d_is_defined 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(d,b)) | ~ defined(d) | ~ defined(b) cnf(42004,negated_conjecture, ( equalish(multiply(a,c),multiply(d,b)) | ~ defined(d) | ~ defined(b) ), inference(spm,[status(thm)],[128,41804,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#42004 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(b,d)) cnf(41804,negated_conjecture, ( equalish(multiply(a,c),multiply(b,d)) ), inference(cn,[status(thm)],[41803,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#41804 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(b,d)) | $false | $false cnf(41803,negated_conjecture, ( equalish(multiply(a,c),multiply(b,d)) | $false | $false ), inference(rw,[status(thm)],[41802,28,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#41803 TPTP Formula 0 2009-09-21T20:58:24-04:00 defined(a) cnf(28,axiom, ( defined(a) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',a_is_defined)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#28 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#a_is_defined a_is_defined 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(b,d)) | $false | ~ defined(a) cnf(41802,negated_conjecture, ( equalish(multiply(a,c),multiply(b,d)) | $false | ~ defined(a) ), inference(rw,[status(thm)],[41654,31,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#41802 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(a,c),multiply(b,d)) | ~ defined(d) | ~ defined(a) cnf(41654,negated_conjecture, ( equalish(multiply(a,c),multiply(b,d)) | ~ defined(d) | ~ defined(a) ), inference(spm,[status(thm)],[1510,15141,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#41654 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(X1,c),multiply(X1,d)) | ~ defined(X1) cnf(15141,negated_conjecture, ( equalish(multiply(X1,c),multiply(X1,d)) | ~ defined(X1) ), inference(cn,[status(thm)],[15140,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#15141 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(X1,c),multiply(X1,d)) | ~ defined(X1) | $false cnf(15140,negated_conjecture, ( equalish(multiply(X1,c),multiply(X1,d)) | ~ defined(X1) | $false ), inference(rw,[status(thm)],[15134,31,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#15140 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(X1,c),multiply(X1,d)) | ~ defined(X1) | ~ defined(d) cnf(15134,negated_conjecture, ( equalish(multiply(X1,c),multiply(X1,d)) | ~ defined(X1) | ~ defined(d) ), inference(spm,[status(thm)],[128,10370,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#15134 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(X1,c),multiply(d,X1)) | ~ defined(X1) cnf(10370,negated_conjecture, ( equalish(multiply(X1,c),multiply(d,X1)) | ~ defined(X1) ), inference(spm,[status(thm)],[22,3591,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#10370 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(d,X1),multiply(X1,c)) | ~ defined(X1) cnf(3591,negated_conjecture, ( equalish(multiply(d,X1),multiply(X1,c)) | ~ defined(X1) ), inference(cn,[status(thm)],[3590,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#3591 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(d,X1),multiply(X1,c)) | ~ defined(X1) | $false cnf(3590,negated_conjecture, ( equalish(multiply(d,X1),multiply(X1,c)) | ~ defined(X1) | $false ), inference(rw,[status(thm)],[3262,30,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#3590 TPTP Formula 0 2009-09-21T20:58:24-04:00 defined(c) cnf(30,axiom, ( defined(c) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',c_is_defined)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#30 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#c_is_defined c_is_defined 2009-09-21T20:58:24-04:00 equalish(multiply(d,X1),multiply(X1,c)) | ~ defined(X1) | ~ defined(c) cnf(3262,negated_conjecture, ( equalish(multiply(d,X1),multiply(X1,c)) | ~ defined(X1) | ~ defined(c) ), inference(spm,[status(thm)],[128,93,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#3262 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(d,X1),multiply(c,X1)) | ~ defined(X1) cnf(93,negated_conjecture, ( equalish(multiply(d,X1),multiply(c,X1)) | ~ defined(X1) ), inference(spm,[status(thm)],[25,36,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#93 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(d,c) cnf(36,negated_conjecture, ( equalish(d,c) ), inference(spm,[status(thm)],[22,33,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#36 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(c,d) cnf(33,negated_conjecture, ( equalish(c,d) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',c_equals_d_6)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#33 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#c_equals_d_6 c_equals_d_6 2009-09-21T20:58:24-04:00 equalish(multiply(X1,X2),multiply(X3,X2)) | ~ defined(X2) | ~ equalish(X1,X3) cnf(25,axiom, ( equalish(multiply(X1,X2),multiply(X3,X2)) | ~ defined(X2) | ~ equalish(X1,X3) ), file('/home/graph/tptp/TPTP/Axioms/FLD001-0.ax',compatibility_of_equality_and_multiplication)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#25 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Axioms&File=FLD001-0.ax#compatibility_of_equality_and_multiplication compatibility_of_equality_and_multiplication 2009-09-21T20:58:24-04:00 equalish(X1,multiply(X2,X3)) | ~ equalish(X1,multiply(X3,X2)) | ~ defined(X2) | ~ defined(X3) cnf(128,plain, ( equalish(X1,multiply(X2,X3)) | ~ equalish(X1,multiply(X3,X2)) | ~ defined(X2) | ~ defined(X3) ), inference(spm,[status(thm)],[23,8,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#128 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(X1,X2),multiply(X2,X1)) | ~ defined(X1) | ~ defined(X2) cnf(8,axiom, ( equalish(multiply(X1,X2),multiply(X2,X1)) | ~ defined(X1) | ~ defined(X2) ), file('/home/graph/tptp/TPTP/Axioms/FLD001-0.ax',commutativity_multiplication)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#8 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Axioms&File=FLD001-0.ax#commutativity_multiplication commutativity_multiplication 2009-09-21T20:58:24-04:00 equalish(X1,X2) | ~ equalish(X1,X3) | ~ equalish(X3,X2) cnf(23,axiom, ( equalish(X1,X2) | ~ equalish(X1,X3) | ~ equalish(X3,X2) ), file('/home/graph/tptp/TPTP/Axioms/FLD001-0.ax',transitivity_of_equality)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#23 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Axioms&File=FLD001-0.ax#transitivity_of_equality transitivity_of_equality 2009-09-21T20:58:24-04:00 equalish(X1,multiply(b,X2)) | ~ equalish(X1,multiply(a,X2)) | ~ defined(X2) cnf(1510,negated_conjecture, ( equalish(X1,multiply(b,X2)) | ~ equalish(X1,multiply(a,X2)) | ~ defined(X2) ), inference(spm,[status(thm)],[23,90,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#1510 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(multiply(a,X1),multiply(b,X1)) | ~ defined(X1) cnf(90,negated_conjecture, ( equalish(multiply(a,X1),multiply(b,X1)) | ~ defined(X1) ), inference(spm,[status(thm)],[25,32,theory(equality)])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#90 TPTP Formula 0 2009-09-21T20:58:24-04:00 equalish(a,b) cnf(32,negated_conjecture, ( equalish(a,b) ), file('/home/graph/tptp/TPTP/Problems/FLD/FLD025-1.p',a_equals_b_5)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD025-1&System=EP---1.1.UNS-CRf.s#32 TPTP Formula 0 2009-09-21T20:58:24-04:00 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=FLD&File=FLD025-1.p#a_equals_b_5 a_equals_b_5