2010-01-21T09:09:17-05:00 equalish(multiplicative_inverse(multiplicative_identity),multiplicative_identity) cnf(66761,plain, ( equalish(multiplicative_inverse(multiplicative_identity),multiplicative_identity) ), inference(resolution,[status(thm)],[21127,19446])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#66761 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiply(multiplicative_identity,multiplicative_inverse(multiplicative_identity))) | equalish(X1,multiplicative_identity) cnf(19446,plain, ( ~ equalish(X1,multiply(multiplicative_identity,multiplicative_inverse(multiplicative_identity))) | equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[51,19029])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19446 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(multiplicative_identity,multiplicative_inverse(multiplicative_identity)),multiplicative_identity) cnf(19029,plain, ( equalish(multiply(multiplicative_identity,multiplicative_inverse(multiplicative_identity)),multiplicative_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[14,37,18953])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19029 TPTP Formula 0 Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Unknown Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution Inference rule: resolution, forward subsumption resolution 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_identity,additive_identity) cnf(18953,plain, ( ~ equalish(multiplicative_identity,additive_identity) ), inference(resolution,[status(thm)],[371,18948])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#18953 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_identity,multiplicative_inverse(a)) cnf(18948,plain, ( ~ equalish(multiplicative_identity,multiplicative_inverse(a)) ), inference(resolution,[status(thm)],[4128,18189])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#18948 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiply(multiplicative_inverse(a),a),a) cnf(18189,plain, ( ~ equalish(multiply(multiplicative_inverse(a),a),a) ), inference(resolution,[status(thm)],[2061,18097])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#18189 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_identity,X1) | ~ equalish(X1,a) cnf(18097,plain, ( ~ equalish(multiplicative_identity,X1) | ~ equalish(X1,a) ), inference(resolution,[status(thm)],[51,18094])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#18097 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_identity,a) cnf(18094,plain, ( ~ equalish(multiplicative_identity,a) ), inference(resolution,[status(thm)],[1770,2034])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#18094 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(X1,multiplicative_inverse(a)),multiplicative_identity) | ~ equalish(X1,a) cnf(2034,plain, ( equalish(multiply(X1,multiplicative_inverse(a)),multiplicative_identity) | ~ equalish(X1,a) ), inference('resolution, forward subsumption resolution',[status(thm)],[86,53,187])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2034 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiply(a,multiplicative_inverse(a))) | equalish(X1,multiplicative_identity) cnf(187,plain, ( ~ equalish(X1,multiply(a,multiplicative_inverse(a))) | equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[51,85])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#187 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity) cnf(85,plain, ( equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,37,29])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#85 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(a,additive_identity) cnf(29,negated_conjecture, ( ~ equalish(a,additive_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#29 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 $false cnf(130603,plain, ( $false ), inference('resolution, forward subsumption resolution',[status(thm)],[28,11,42,130602])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130603 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ defined(multiply(additive_identity,a)) cnf(130602,plain, ( ~ defined(multiply(additive_identity,a)) ), inference('resolution, forward subsumption resolution',[status(thm)],[22539,128966,130530])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130602 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(a,add(a,X1)) | ~ defined(X1) | ~ equalish(X1,multiplicative_identity) cnf(130530,plain, ( ~ equalish(a,add(a,X1)) | ~ defined(X1) | ~ equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[15635,130404])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130530 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(a,additive_identity),add(X1,a)) | ~ equalish(X1,multiplicative_identity) cnf(130404,plain, ( ~ equalish(add(a,additive_identity),add(X1,a)) | ~ equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[4370,130400])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130404 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(multiplicative_identity,a),add(a,additive_identity)) cnf(130400,plain, ( ~ equalish(add(multiplicative_identity,a),add(a,additive_identity)) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,46791,130290])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130400 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(a,add(multiply(a,multiplicative_inverse(a)),a)) cnf(130290,plain, ( ~ equalish(a,add(multiply(a,multiplicative_inverse(a)),a)) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,184,130274])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130290 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(multiplicative_identity,a)) | ~ equalish(a,X1) cnf(130274,plain, ( ~ equalish(X1,add(multiplicative_identity,a)) | ~ equalish(a,X1) ), inference('resolution, forward subsumption resolution',[status(thm)],[14,5398,130270])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130274 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(a,add(a,multiplicative_identity)) cnf(130270,plain, ( ~ equalish(a,add(a,multiplicative_identity)) ), inference(resolution,[status(thm)],[54506,130269])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130270 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(add(a,multiplicative_identity),additive_inverse(a)),additive_identity) cnf(130269,plain, ( ~ equalish(add(add(a,multiplicative_identity),additive_inverse(a)),additive_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[14,5419,88398])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#130269 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(add(multiplicative_identity,additive_inverse(a)),a),X1) | ~ equalish(X1,additive_identity) cnf(88398,plain, ( ~ equalish(add(add(multiplicative_identity,additive_inverse(a)),a),X1) | ~ equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[51,88320])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#88398 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(add(multiplicative_identity,additive_inverse(a)),a),additive_identity) cnf(88320,plain, ( ~ equalish(add(add(multiplicative_identity,additive_inverse(a)),a),additive_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[94,14,608,88250])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#88320 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(multiplicative_identity,add(additive_inverse(a),a)),additive_identity) cnf(88250,plain, ( ~ equalish(add(multiplicative_identity,add(additive_inverse(a),a)),additive_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[1125,59599,88228])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#88250 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(additive_identity,add(multiplicative_identity,add(additive_inverse(a),a))) cnf(88228,plain, ( ~ equalish(additive_identity,add(multiplicative_identity,add(additive_inverse(a),a))) ), inference('resolution, forward subsumption resolution',[status(thm)],[94,14,63044,7324])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#88228 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,add(add(X2,a),X3)) | ~ defined(X2) | ~ defined(X3) | ~ equalish(X1,add(X3,add(X2,a))) cnf(7324,plain, ( equalish(X1,add(add(X2,a),X3)) | ~ defined(X2) | ~ defined(X3) | ~ equalish(X1,add(X3,add(X2,a))) ), inference(resolution,[status(thm)],[51,491])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#7324 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,add(X2,a)),add(add(X2,a),X1)) | ~ defined(X2) | ~ defined(X1) cnf(491,plain, ( equalish(add(X1,add(X2,a)),add(add(X2,a),X1)) | ~ defined(X2) | ~ defined(X1) ), inference(resolution,[status(thm)],[34,104])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#491 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(add(X1,a)) | ~ defined(X1) cnf(104,plain, ( defined(add(X1,a)) | ~ defined(X1) ), inference(resolution,[status(thm)],[40,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#104 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(a) cnf(28,hypothesis, ( defined(a) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#28 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ defined(X0) | ~ defined(X1) | defined(add(X0,X1)) cnf(40,plain, ( ~ defined(X0) | ~ defined(X1) | defined(add(X0,X1)) ), inference(normalize,[status(thm)],[10])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#40 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(add(X0,X1)) | ~ defined(X0) | ~ defined(X1) cnf(10,axiom, ( defined(add(X0,X1)) | ~ defined(X0) | ~ defined(X1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#10 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ defined(X0) | ~ defined(X1) | equalish(add(X0,X1),add(X1,X0)) cnf(34,plain, ( ~ defined(X0) | ~ defined(X1) | equalish(add(X0,X1),add(X1,X0)) ), inference(normalize,[status(thm)],[4])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#34 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X0,X1),add(X1,X0)) | ~ defined(X0) | ~ defined(X1) cnf(4,axiom, ( equalish(add(X0,X1),add(X1,X0)) | ~ defined(X0) | ~ defined(X1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#4 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ equalish(X0,X1) | ~ equalish(X1,X2) | equalish(X0,X2) cnf(51,plain, ( ~ equalish(X0,X1) | ~ equalish(X1,X2) | equalish(X0,X2) ), inference(normalize,[status(thm)],[23])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#51 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X0,X2) | ~ equalish(X0,X1) | ~ equalish(X1,X2) cnf(23,axiom, ( equalish(X0,X2) | ~ equalish(X0,X1) | ~ equalish(X1,X2) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#23 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ equalish(additive_identity,add(add(additive_inverse(a),a),multiplicative_identity)) cnf(63044,plain, ( ~ equalish(additive_identity,add(add(additive_inverse(a),a),multiplicative_identity)) ), inference('resolution, forward subsumption resolution',[status(thm)],[14,19978,3088])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#63044 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(add(additive_inverse(a),a),X1),add(additive_identity,X1)) | ~ defined(X1) cnf(3088,plain, ( equalish(add(add(additive_inverse(a),a),X1),add(additive_identity,X1)) | ~ defined(X1) ), inference(resolution,[status(thm)],[52,2974])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#3088 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(additive_inverse(a),a),additive_identity) cnf(2974,plain, ( equalish(add(additive_inverse(a),a),additive_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,41,34,257])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2974 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(a,additive_inverse(a))) | equalish(X1,additive_identity) cnf(257,plain, ( ~ equalish(X1,add(a,additive_inverse(a))) | equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[51,92])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#257 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(a,additive_inverse(a)),additive_identity) cnf(92,plain, ( equalish(add(a,additive_inverse(a)),additive_identity) ), inference(resolution,[status(thm)],[33,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#92 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ defined(X0) | equalish(add(X0,additive_inverse(X0)),additive_identity) cnf(33,plain, ( ~ defined(X0) | equalish(add(X0,additive_inverse(X0)),additive_identity) ), inference(normalize,[status(thm)],[3])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#33 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X0,additive_inverse(X0)),additive_identity) | ~ defined(X0) cnf(3,axiom, ( equalish(add(X0,additive_inverse(X0)),additive_identity) | ~ defined(X0) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#3 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ defined(X0) | defined(additive_inverse(X0)) cnf(41,plain, ( ~ defined(X0) | defined(additive_inverse(X0)) ), inference(normalize,[status(thm)],[12])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#41 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(additive_inverse(X0)) | ~ defined(X0) cnf(12,axiom, ( defined(additive_inverse(X0)) | ~ defined(X0) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#12 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ defined(X2) | ~ equalish(X0,X1) | equalish(add(X0,X2),add(X1,X2)) cnf(52,plain, ( ~ defined(X2) | ~ equalish(X0,X1) | equalish(add(X0,X2),add(X1,X2)) ), inference(normalize,[status(thm)],[24])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#52 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X0,X2),add(X1,X2)) | ~ defined(X2) | ~ equalish(X0,X1) cnf(24,axiom, ( equalish(add(X0,X2),add(X1,X2)) | ~ defined(X2) | ~ equalish(X0,X1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#24 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(additive_identity,multiplicative_identity)) | ~ equalish(additive_identity,X1) cnf(19978,plain, ( ~ equalish(X1,add(additive_identity,multiplicative_identity)) | ~ equalish(additive_identity,X1) ), inference(resolution,[status(thm)],[51,19936])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19978 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(additive_identity,add(additive_identity,multiplicative_identity)) cnf(19936,plain, ( ~ equalish(additive_identity,add(additive_identity,multiplicative_identity)) ), inference(resolution,[status(thm)],[50,19886])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19936 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(additive_identity,multiplicative_identity),additive_identity) cnf(19886,plain, ( ~ equalish(add(additive_identity,multiplicative_identity),additive_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[14,32,19496])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19886 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiplicative_identity) | ~ equalish(X1,additive_identity) cnf(19496,plain, ( ~ equalish(X1,multiplicative_identity) | ~ equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[50,19032])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19496 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_identity,X1) | ~ equalish(X1,additive_identity) cnf(19032,plain, ( ~ equalish(multiplicative_identity,X1) | ~ equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[51,18953])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19032 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,X0) | equalish(X0,X1) cnf(50,plain, ( ~ equalish(X1,X0) | equalish(X0,X1) ), inference(normalize,[status(thm)],[22])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#50 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X0,X1) | ~ equalish(X1,X0) cnf(22,axiom, ( equalish(X0,X1) | ~ equalish(X1,X0) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#22 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 ~ defined(X0) | equalish(add(additive_identity,X0),X0) cnf(32,plain, ( ~ defined(X0) | equalish(add(additive_identity,X0),X0) ), inference(normalize,[status(thm)],[2])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#32 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(additive_identity,X0),X0) | ~ defined(X0) cnf(2,axiom, ( equalish(add(additive_identity,X0),X0) | ~ defined(X0) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 defined(multiplicative_identity) cnf(14,axiom, ( defined(multiplicative_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#14 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 defined(additive_inverse(a)) cnf(94,plain, ( defined(additive_inverse(a)) ), inference(resolution,[status(thm)],[41,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#94 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,X2) | ~ equalish(additive_identity,X1) | ~ equalish(X2,additive_identity) cnf(59599,plain, ( equalish(X1,X2) | ~ equalish(additive_identity,X1) | ~ equalish(X2,additive_identity) ), inference(resolution,[status(thm)],[2238,2728])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#59599 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_inverse(a),X1) | ~ equalish(additive_identity,X2) | equalish(X2,X1) cnf(2728,plain, ( ~ equalish(multiplicative_inverse(a),X1) | ~ equalish(additive_identity,X2) | equalish(X2,X1) ), inference(resolution,[status(thm)],[51,1137])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2728 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,multiplicative_inverse(a)) | ~ equalish(additive_identity,X1) cnf(1137,plain, ( equalish(X1,multiplicative_inverse(a)) | ~ equalish(additive_identity,X1) ), inference(resolution,[status(thm)],[50,138])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#1137 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiplicative_inverse(a),X1) | ~ equalish(additive_identity,X1) cnf(138,plain, ( equalish(multiplicative_inverse(a),X1) | ~ equalish(additive_identity,X1) ), inference(resolution,[status(thm)],[51,30])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#138 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiplicative_inverse(a),additive_identity) cnf(30,negated_conjecture, ( equalish(multiplicative_inverse(a),additive_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#30 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 equalish(multiplicative_inverse(a),X1) | ~ equalish(X1,additive_identity) cnf(2238,plain, ( equalish(multiplicative_inverse(a),X1) | ~ equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[50,371])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2238 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,multiplicative_inverse(a)) | ~ equalish(X1,additive_identity) cnf(371,plain, ( equalish(X1,multiplicative_inverse(a)) | ~ equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[51,136])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#371 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(additive_identity,multiplicative_inverse(a)) cnf(136,plain, ( equalish(additive_identity,multiplicative_inverse(a)) ), inference(resolution,[status(thm)],[50,30])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#136 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(additive_identity,additive_identity) cnf(1125,plain, ( equalish(additive_identity,additive_identity) ), inference(resolution,[status(thm)],[136,137])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#1125 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiplicative_inverse(a)) | equalish(X1,additive_identity) cnf(137,plain, ( ~ equalish(X1,multiplicative_inverse(a)) | equalish(X1,additive_identity) ), inference(resolution,[status(thm)],[51,30])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#137 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,add(X2,a)),X3) | ~ defined(X2) | ~ defined(X1) | ~ equalish(add(add(X1,X2),a),X3) cnf(608,plain, ( equalish(add(X1,add(X2,a)),X3) | ~ defined(X2) | ~ defined(X1) | ~ equalish(add(add(X1,X2),a),X3) ), inference(resolution,[status(thm)],[51,112])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#608 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,add(X2,a)),add(add(X1,X2),a)) | ~ defined(X2) | ~ defined(X1) cnf(112,plain, ( equalish(add(X1,add(X2,a)),add(add(X1,X2),a)) | ~ defined(X2) | ~ defined(X1) ), inference(resolution,[status(thm)],[31,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#112 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ defined(X0) | ~ defined(X1) | ~ defined(X2) | equalish(add(X0,add(X1,X2)),add(add(X0,X1),X2)) cnf(31,plain, ( ~ defined(X0) | ~ defined(X1) | ~ defined(X2) | equalish(add(X0,add(X1,X2)),add(add(X0,X1),X2)) ), inference(normalize,[status(thm)],[1])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#31 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X0,add(X1,X2)),add(add(X0,X1),X2)) | ~ defined(X0) | ~ defined(X1) | ~ defined(X2) cnf(1,axiom, ( equalish(add(X0,add(X1,X2)),add(add(X0,X1),X2)) | ~ defined(X0) | ~ defined(X1) | ~ defined(X2) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#1 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 equalish(add(add(X1,additive_inverse(a)),a),add(add(a,X1),additive_inverse(a))) | ~ defined(X1) cnf(5419,plain, ( equalish(add(add(X1,additive_inverse(a)),a),add(add(a,X1),additive_inverse(a))) | ~ defined(X1) ), inference('resolution, forward subsumption resolution',[status(thm)],[212,28,220,377])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#5419 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(a,X1),X2) | ~ defined(X1) | equalish(add(X1,a),X2) cnf(377,plain, ( ~ equalish(add(a,X1),X2) | ~ defined(X1) | equalish(add(X1,a),X2) ), inference(resolution,[status(thm)],[51,98])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#377 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,a),add(a,X1)) | ~ defined(X1) cnf(98,plain, ( equalish(add(X1,a),add(a,X1)) | ~ defined(X1) ), inference(resolution,[status(thm)],[34,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#98 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,add(X2,additive_inverse(a))),add(add(X1,X2),additive_inverse(a))) | ~ defined(X2) | ~ defined(X1) cnf(220,plain, ( equalish(add(X1,add(X2,additive_inverse(a))),add(add(X1,X2),additive_inverse(a))) | ~ defined(X2) | ~ defined(X1) ), inference(resolution,[status(thm)],[31,94])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#220 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(add(X1,additive_inverse(a))) | ~ defined(X1) cnf(212,plain, ( defined(add(X1,additive_inverse(a))) | ~ defined(X1) ), inference(resolution,[status(thm)],[40,94])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#212 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,additive_inverse(a)),additive_identity) | ~ equalish(a,X1) cnf(54506,plain, ( equalish(add(X1,additive_inverse(a)),additive_identity) | ~ equalish(a,X1) ), inference(resolution,[status(thm)],[257,2248])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#54506 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,additive_inverse(a)),add(X2,additive_inverse(a))) | ~ equalish(X2,X1) cnf(2248,plain, ( equalish(add(X1,additive_inverse(a)),add(X2,additive_inverse(a))) | ~ equalish(X2,X1) ), inference(resolution,[status(thm)],[50,204])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2248 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,additive_inverse(a)),add(X2,additive_inverse(a))) | ~ equalish(X1,X2) cnf(204,plain, ( equalish(add(X1,additive_inverse(a)),add(X2,additive_inverse(a))) | ~ equalish(X1,X2) ), inference(resolution,[status(thm)],[52,94])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#204 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,add(a,X2)) | ~ defined(X2) | ~ equalish(X3,add(X2,a)) | ~ equalish(X1,X3) cnf(5398,plain, ( equalish(X1,add(a,X2)) | ~ defined(X2) | ~ equalish(X3,add(X2,a)) | ~ equalish(X1,X3) ), inference(resolution,[status(thm)],[51,376])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#5398 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,add(a,X2)) | ~ defined(X2) | ~ equalish(X1,add(X2,a)) cnf(376,plain, ( equalish(X1,add(a,X2)) | ~ defined(X2) | ~ equalish(X1,add(X2,a)) ), inference(resolution,[status(thm)],[51,98])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#376 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(multiply(a,multiplicative_inverse(a)),X1),add(multiplicative_identity,X1)) | ~ defined(X1) cnf(184,plain, ( equalish(add(multiply(a,multiplicative_inverse(a)),X1),add(multiplicative_identity,X1)) | ~ defined(X1) ), inference(resolution,[status(thm)],[52,85])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#184 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(a,add(multiply(a,multiplicative_inverse(a)),X1)) | ~ defined(X1) | ~ equalish(add(multiplicative_identity,X1),add(a,additive_identity)) cnf(46791,plain, ( equalish(a,add(multiply(a,multiplicative_inverse(a)),X1)) | ~ defined(X1) | ~ equalish(add(multiplicative_identity,X1),add(a,additive_identity)) ), inference(resolution,[status(thm)],[7785,1941])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#46791 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(multiply(a,multiplicative_inverse(a)),X1),X2) | ~ defined(X1) | ~ equalish(add(multiplicative_identity,X1),X2) cnf(1941,plain, ( equalish(add(multiply(a,multiplicative_inverse(a)),X1),X2) | ~ defined(X1) | ~ equalish(add(multiplicative_identity,X1),X2) ), inference(resolution,[status(thm)],[51,184])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#1941 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(a,additive_identity)) | equalish(a,X1) cnf(7785,plain, ( ~ equalish(X1,add(a,additive_identity)) | equalish(a,X1) ), inference(resolution,[status(thm)],[50,2907])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#7785 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(add(a,additive_identity),X1) | equalish(a,X1) cnf(2907,plain, ( ~ equalish(add(a,additive_identity),X1) | equalish(a,X1) ), inference(resolution,[status(thm)],[51,2897])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2907 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(a,add(a,additive_identity)) cnf(2897,plain, ( equalish(a,add(a,additive_identity)) ), inference(resolution,[status(thm)],[50,2873])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2897 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(a,additive_identity),a) cnf(2873,plain, ( equalish(add(a,additive_identity),a) ), inference('resolution, forward subsumption resolution',[status(thm)],[11,28,34,245])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2873 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(additive_identity,a)) | equalish(X1,a) cnf(245,plain, ( ~ equalish(X1,add(additive_identity,a)) | equalish(X1,a) ), inference(resolution,[status(thm)],[51,90])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#245 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(additive_identity,a),a) cnf(90,plain, ( equalish(add(additive_identity,a),a) ), inference(resolution,[status(thm)],[32,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#90 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(additive_identity) cnf(11,axiom, ( defined(additive_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#11 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 equalish(add(X1,a),X2) | ~ equalish(X2,add(X3,a)) | ~ equalish(X3,X1) cnf(4370,plain, ( equalish(add(X1,a),X2) | ~ equalish(X2,add(X3,a)) | ~ equalish(X3,X1) ), inference(resolution,[status(thm)],[50,315])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#4370 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(X1,add(X2,a)) | ~ equalish(X1,add(X3,a)) | ~ equalish(X3,X2) cnf(315,plain, ( equalish(X1,add(X2,a)) | ~ equalish(X1,add(X3,a)) | ~ equalish(X3,X2) ), inference(resolution,[status(thm)],[51,96])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#315 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(X1,a),add(X2,a)) | ~ equalish(X1,X2) cnf(96,plain, ( equalish(add(X1,a),add(X2,a)) | ~ equalish(X1,X2) ), inference(resolution,[status(thm)],[52,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#96 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(a,additive_identity),add(X1,a)) | ~ defined(X1) | ~ equalish(a,add(a,X1)) cnf(15635,plain, ( equalish(add(a,additive_identity),add(X1,a)) | ~ defined(X1) | ~ equalish(a,add(a,X1)) ), inference(resolution,[status(thm)],[2902,846])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#15635 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(a,X2)) | ~ defined(X2) | equalish(X1,add(X2,a)) cnf(846,plain, ( ~ equalish(X1,add(a,X2)) | ~ defined(X2) | equalish(X1,add(X2,a)) ), inference(resolution,[status(thm)],[51,120])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#846 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(a,X1),add(X1,a)) | ~ defined(X1) cnf(120,plain, ( equalish(add(a,X1),add(X1,a)) | ~ defined(X1) ), inference(resolution,[status(thm)],[34,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#120 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(a,additive_identity),X1) | ~ equalish(a,X1) cnf(2902,plain, ( equalish(add(a,additive_identity),X1) | ~ equalish(a,X1) ), inference(resolution,[status(thm)],[51,2873])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2902 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(a,add(a,multiply(additive_identity,a))) cnf(128966,plain, ( equalish(a,add(a,multiply(additive_identity,a))) ), inference('resolution, forward subsumption resolution',[status(thm)],[93,86264,128964])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#128966 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(a,multiply(additive_identity,a)),a) cnf(128964,plain, ( equalish(add(a,multiply(additive_identity,a)),a) ), inference('resolution, forward subsumption resolution',[status(thm)],[11,9623,128595])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#128964 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiply(add(multiplicative_identity,additive_identity),a)) | equalish(X1,a) cnf(128595,plain, ( ~ equalish(X1,multiply(add(multiplicative_identity,additive_identity),a)) | equalish(X1,a) ), inference(resolution,[status(thm)],[51,128575])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#128595 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(add(multiplicative_identity,additive_identity),a),a) cnf(128575,plain, ( equalish(multiply(add(multiplicative_identity,additive_identity),a),a) ), inference(resolution,[status(thm)],[118095,128566])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#128575 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(a,additive_identity),add(multiplicative_identity,additive_identity)) cnf(128566,plain, ( equalish(multiply(a,additive_identity),add(multiplicative_identity,additive_identity)) ), inference('resolution, forward subsumption resolution',[status(thm)],[11,85116,46600])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#128566 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiplicative_identity,add(multiply(a,multiplicative_inverse(a)),X1)) | ~ defined(X1) | equalish(multiply(a,additive_identity),add(multiplicative_identity,X1)) cnf(46600,plain, ( ~ equalish(multiplicative_identity,add(multiply(a,multiplicative_inverse(a)),X1)) | ~ defined(X1) | equalish(multiply(a,additive_identity),add(multiplicative_identity,X1)) ), inference(resolution,[status(thm)],[30132,1940])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#46600 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(multiply(a,multiplicative_inverse(a)),X2)) | ~ defined(X2) | equalish(X1,add(multiplicative_identity,X2)) cnf(1940,plain, ( ~ equalish(X1,add(multiply(a,multiplicative_inverse(a)),X2)) | ~ defined(X2) | equalish(X1,add(multiplicative_identity,X2)) ), inference(resolution,[status(thm)],[51,184])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#1940 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(a,additive_identity),X1) | ~ equalish(multiplicative_identity,X1) cnf(30132,plain, ( equalish(multiply(a,additive_identity),X1) | ~ equalish(multiplicative_identity,X1) ), inference(resolution,[status(thm)],[51,30122])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#30132 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(a,additive_identity),multiplicative_identity) cnf(30122,plain, ( equalish(multiply(a,additive_identity),multiplicative_identity) ), inference(resolution,[status(thm)],[50,30040])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#30122 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiplicative_identity,multiply(a,additive_identity)) cnf(30040,plain, ( equalish(multiplicative_identity,multiply(a,additive_identity)) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,11,38,22541])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#30040 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(multiply(additive_identity,a),X1) | equalish(multiplicative_identity,X1) cnf(22541,plain, ( ~ equalish(multiply(additive_identity,a),X1) | equalish(multiplicative_identity,X1) ), inference(resolution,[status(thm)],[51,22460])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#22541 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiplicative_identity,multiply(additive_identity,a)) cnf(22460,plain, ( equalish(multiplicative_identity,multiply(additive_identity,a)) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,2061,1103])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#22460 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiply(multiplicative_inverse(a),X2)) | ~ defined(X2) | equalish(X1,multiply(additive_identity,X2)) cnf(1103,plain, ( ~ equalish(X1,multiply(multiplicative_inverse(a),X2)) | ~ defined(X2) | equalish(X1,multiply(additive_identity,X2)) ), inference(resolution,[status(thm)],[51,133])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#1103 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(multiplicative_inverse(a),X1),multiply(additive_identity,X1)) | ~ defined(X1) cnf(133,plain, ( equalish(multiply(multiplicative_inverse(a),X1),multiply(additive_identity,X1)) | ~ defined(X1) ), inference(resolution,[status(thm)],[53,30])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#133 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ defined(X2) | ~ equalish(X0,X1) | equalish(multiply(X0,X2),multiply(X1,X2)) cnf(53,plain, ( ~ defined(X2) | ~ equalish(X0,X1) | equalish(multiply(X0,X2),multiply(X1,X2)) ), inference(normalize,[status(thm)],[25])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#53 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(X0,X2),multiply(X1,X2)) | ~ defined(X2) | ~ equalish(X0,X1) cnf(25,axiom, ( equalish(multiply(X0,X2),multiply(X1,X2)) | ~ defined(X2) | ~ equalish(X0,X1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#25 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 equalish(multiplicative_identity,multiply(multiplicative_inverse(a),a)) cnf(2061,plain, ( equalish(multiplicative_identity,multiply(multiplicative_inverse(a),a)) ), inference(resolution,[status(thm)],[50,2033])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2061 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(multiplicative_inverse(a),a),multiplicative_identity) cnf(2033,plain, ( equalish(multiply(multiplicative_inverse(a),a),multiplicative_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,86,38,187])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#2033 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ defined(X0) | ~ defined(X1) | equalish(multiply(X0,X1),multiply(X1,X0)) cnf(38,plain, ( ~ defined(X0) | ~ defined(X1) | equalish(multiply(X0,X1),multiply(X1,X0)) ), inference(normalize,[status(thm)],[8])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#38 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(multiply(X0,X1),multiply(X1,X0)) | ~ defined(X0) | ~ defined(X1) cnf(8,axiom, ( equalish(multiply(X0,X1),multiply(X1,X0)) | ~ defined(X0) | ~ defined(X1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#8 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 defined(multiplicative_inverse(a)) cnf(86,plain, ( defined(multiplicative_inverse(a)) ), inference('resolution, forward subsumption resolution',[status(thm)],[28,43,29])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#86 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ defined(X0) | defined(multiplicative_inverse(X0)) | equalish(X0,additive_identity) cnf(43,plain, ( ~ defined(X0) | defined(multiplicative_inverse(X0)) | equalish(X0,additive_identity) ), inference(normalize,[status(thm)],[15])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#43 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(multiplicative_inverse(X0)) | ~ defined(X0) | equalish(X0,additive_identity) cnf(15,axiom, ( defined(multiplicative_inverse(X0)) | ~ defined(X0) | equalish(X0,additive_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#15 TPTP Formula 0 2010-01-21T09:09:17-05:00 file://input unknown 2010-01-21T09:09:17-05:00 equalish(multiplicative_identity,add(multiply(a,multiplicative_inverse(a)),additive_identity)) cnf(85116,plain, ( equalish(multiplicative_identity,add(multiply(a,multiplicative_inverse(a)),additive_identity)) ), inference(resolution,[status(thm)],[50,85099])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#85116 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(multiply(a,multiplicative_inverse(a)),additive_identity),multiplicative_identity) cnf(85099,plain, ( equalish(add(multiply(a,multiplicative_inverse(a)),additive_identity),multiplicative_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[11,66764,2043,79768])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#85099 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(multiplicative_inverse(multiplicative_identity),additive_identity)) | equalish(X1,multiplicative_identity) cnf(79768,plain, ( ~ equalish(X1,add(multiplicative_inverse(multiplicative_identity),additive_identity)) | equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[51,79750])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#79768 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(multiplicative_inverse(multiplicative_identity),additive_identity),multiplicative_identity) cnf(79750,plain, ( equalish(add(multiplicative_inverse(multiplicative_identity),additive_identity),multiplicative_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[11,19030,34,67178])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#79750 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,add(additive_identity,multiplicative_inverse(multiplicative_identity))) | equalish(X1,multiplicative_identity) cnf(67178,plain, ( ~ equalish(X1,add(additive_identity,multiplicative_inverse(multiplicative_identity))) | equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[51,67154])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#67178 TPTP Formula 0 2010-01-21T09:09:17-05:00 equalish(add(additive_identity,multiplicative_inverse(multiplicative_identity)),multiplicative_identity) cnf(67154,plain, ( equalish(add(additive_identity,multiplicative_inverse(multiplicative_identity)),multiplicative_identity) ), inference('resolution, forward subsumption resolution',[status(thm)],[19030,32,66765])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#67154 TPTP Formula 0 2010-01-21T09:09:17-05:00 ~ equalish(X1,multiplicative_inverse(multiplicative_identity)) | equalish(X1,multiplicative_identity) cnf(66765,plain, ( ~ equalish(X1,multiplicative_inverse(multiplicative_identity)) | equalish(X1,multiplicative_identity) ), inference(resolution,[status(thm)],[51,66761])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#66765 TPTP Formula 0 2010-01-21T09:09:17-05:00 defined(multiplicative_inverse(multiplicative_identity)) cnf(19030,plain, ( defined(multiplicative_inverse(multiplicative_identity)) ), inference('resolution, forward subsumption resolution',[status(thm)],[14,43,18953])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD040-1&System=Vampire---11.0.UNS-Ref.s#19030 TPTP Formula 0