2010-01-21T09:09:00-05:00 defined(multiplicative_inverse(a)) cnf(333,plain, ( defined(multiplicative_inverse(a)) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[28,45,30])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#333 TPTP Formula 0 Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation Unknown Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation Inference rule: resolution, forward subsumption resolution, passive clause reanimation 2010-01-21T09:09:00-05:00 ~ equalish(a,additive_identity) cnf(30,negated_conjecture, ( ~ equalish(a,additive_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#30 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 $false cnf(296647,plain, ( $false ), inference('resolution, forward subsumption resolution',[status(thm)],[29,333,44,296646])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#296647 TPTP Formula 0 Inference rule: resolution, forward subsumption resolution Unknown 2010-01-21T09:09:00-05:00 ~ defined(multiply(multiplicative_inverse(a),b)) cnf(296646,plain, ( ~ defined(multiply(multiplicative_inverse(a),b)) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[296613,165849,13502])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#296646 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(multiplicative_inverse(a),b),multiplicative_identity) cnf(13502,plain, ( equalish(multiply(multiplicative_inverse(a),b),multiplicative_identity) ), inference('resolution, passive clause reanimation',[status(thm)],[13486,52])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#13502 TPTP Formula 0 Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Unknown Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation Inference rule: resolution, passive clause reanimation 2010-01-21T09:09:00-05:00 ~ equalish(X1,X0) | equalish(X0,X1) cnf(52,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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#52 TPTP Formula 0 2010-01-21T09:09:00-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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#22 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiplicative_identity,multiply(multiplicative_inverse(a),b)) cnf(13486,plain, ( equalish(multiplicative_identity,multiply(multiplicative_inverse(a),b)) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[13457,40,29,333])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#13486 TPTP Formula 0 2010-01-21T09:09:00-05:00 defined(b) cnf(29,hypothesis, ( defined(b) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#29 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 ~ defined(X0) | ~ defined(X1) | equalish(multiply(X0,X1),multiply(X1,X0)) cnf(40,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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#40 TPTP Formula 0 2010-01-21T09:09:00-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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#8 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 ~ equalish(multiply(b,multiplicative_inverse(a)),X1) | equalish(multiplicative_identity,X1) cnf(13457,plain, ( ~ equalish(multiply(b,multiplicative_inverse(a)),X1) | equalish(multiplicative_identity,X1) ), inference('resolution, passive clause reanimation',[status(thm)],[31,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#13457 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(X0,X1) | ~ equalish(X1,X2) | equalish(X0,X2) cnf(53,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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#53 TPTP Formula 0 2010-01-21T09:09:00-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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#23 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) cnf(31,negated_conjecture, ( equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#31 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 ~ equalish(multiply(a,multiply(multiplicative_inverse(a),b)),a) cnf(165849,plain, ( ~ equalish(multiply(a,multiply(multiplicative_inverse(a),b)),a) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[165718,32226,253])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#165849 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(b,b) cnf(253,plain, ( equalish(b,b) ), inference('resolution, passive clause reanimation',[status(thm)],[29,51])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#253 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ defined(X0) | equalish(X0,X0) cnf(51,plain, ( ~ defined(X0) | equalish(X0,X0) ), inference(normalize,[status(thm)],[21])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#51 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(X0,X0) | ~ defined(X0) cnf(21,axiom, ( equalish(X0,X0) | ~ defined(X0) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#21 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 ~ equalish(X1,X2) | ~ equalish(X2,b) | ~ equalish(X1,a) cnf(32226,plain, ( ~ equalish(X1,X2) | ~ equalish(X2,b) | ~ equalish(X1,a) ), inference('resolution, passive clause reanimation',[status(thm)],[18403,52])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#32226 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(X1,X2) | ~ equalish(X1,b) | ~ equalish(X2,a) cnf(18403,plain, ( ~ equalish(X1,X2) | ~ equalish(X1,b) | ~ equalish(X2,a) ), inference('resolution, passive clause reanimation',[status(thm)],[2595,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#18403 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(X1,a) | ~ equalish(X1,b) cnf(2595,plain, ( ~ equalish(X1,a) | ~ equalish(X1,b) ), inference('resolution, passive clause reanimation',[status(thm)],[467,52])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#2595 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(a,X1) | ~ equalish(X1,b) cnf(467,plain, ( ~ equalish(a,X1) | ~ equalish(X1,b) ), inference('resolution, passive clause reanimation',[status(thm)],[32,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#467 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(a,b) cnf(32,negated_conjecture, ( ~ equalish(a,b) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#32 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiply(a,multiply(multiplicative_inverse(a),b)),b) cnf(165718,plain, ( equalish(multiply(a,multiply(multiplicative_inverse(a),b)),b) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[165546,106252,28,333])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#165718 TPTP Formula 0 2010-01-21T09:09:00-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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#28 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiply(multiply(a,multiplicative_inverse(a)),b),b) cnf(106252,plain, ( equalish(multiply(multiply(a,multiplicative_inverse(a)),b),b) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[105590,8571,29])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#106252 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(X1,multiply(multiplicative_identity,b)) | equalish(X1,b) cnf(8571,plain, ( ~ equalish(X1,multiply(multiplicative_identity,b)) | equalish(X1,b) ), inference('resolution, passive clause reanimation',[status(thm)],[944,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#8571 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(multiplicative_identity,b),b) cnf(944,plain, ( equalish(multiply(multiplicative_identity,b),b) ), inference('resolution, passive clause reanimation',[status(thm)],[29,38])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#944 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ defined(X0) | equalish(multiply(multiplicative_identity,X0),X0) cnf(38,plain, ( ~ defined(X0) | equalish(multiply(multiplicative_identity,X0),X0) ), inference(normalize,[status(thm)],[6])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#38 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(multiplicative_identity,X0),X0) | ~ defined(X0) cnf(6,axiom, ( equalish(multiply(multiplicative_identity,X0),X0) | ~ defined(X0) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#6 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiply(multiply(a,multiplicative_inverse(a)),X1),multiply(multiplicative_identity,X1)) | ~ defined(X1) cnf(105590,plain, ( equalish(multiply(multiply(a,multiplicative_inverse(a)),X1),multiply(multiplicative_identity,X1)) | ~ defined(X1) ), inference('resolution, passive clause reanimation',[status(thm)],[979,55])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#105590 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ defined(X2) | ~ equalish(X0,X1) | equalish(multiply(X0,X2),multiply(X1,X2)) cnf(55,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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#55 TPTP Formula 0 2010-01-21T09:09:00-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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#25 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity) cnf(979,plain, ( equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[28,30,39])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#979 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ defined(X0) | equalish(X0,additive_identity) | equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity) cnf(39,plain, ( ~ defined(X0) | equalish(X0,additive_identity) | equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity) ), inference(normalize,[status(thm)],[7])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#39 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity) | ~ defined(X0) | equalish(X0,additive_identity) cnf(7,axiom, ( equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity) | ~ defined(X0) | equalish(X0,additive_identity) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#7 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 ~ equalish(multiply(multiply(X1,X2),b),X3) | equalish(multiply(X1,multiply(X2,b)),X3) | ~ defined(X2) | ~ defined(X1) cnf(165546,plain, ( ~ equalish(multiply(multiply(X1,X2),b),X3) | equalish(multiply(X1,multiply(X2,b)),X3) | ~ defined(X2) | ~ defined(X1) ), inference('resolution, passive clause reanimation',[status(thm)],[1536,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#165546 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(X1,multiply(X2,b)),multiply(multiply(X1,X2),b)) | ~ defined(X2) | ~ defined(X1) cnf(1536,plain, ( equalish(multiply(X1,multiply(X2,b)),multiply(multiply(X1,X2),b)) | ~ defined(X2) | ~ defined(X1) ), inference('resolution, passive clause reanimation',[status(thm)],[29,37])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#1536 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ defined(X0) | ~ defined(X1) | ~ defined(X2) | equalish(multiply(X0,multiply(X1,X2)),multiply(multiply(X0,X1),X2)) cnf(37,plain, ( ~ defined(X0) | ~ defined(X1) | ~ defined(X2) | equalish(multiply(X0,multiply(X1,X2)),multiply(multiply(X0,X1),X2)) ), inference(normalize,[status(thm)],[5])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#37 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(X0,multiply(X1,X2)),multiply(multiply(X0,X1),X2)) | ~ defined(X0) | ~ defined(X1) | ~ defined(X2) cnf(5,axiom, ( equalish(multiply(X0,multiply(X1,X2)),multiply(multiply(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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#5 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 equalish(multiply(a,X1),a) | ~ equalish(X1,multiplicative_identity) | ~ defined(X1) cnf(296613,plain, ( equalish(multiply(a,X1),a) | ~ equalish(X1,multiplicative_identity) | ~ defined(X1) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[296340,40,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#296613 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(X1,multiply(X2,a)) | equalish(X1,a) | ~ equalish(X2,multiplicative_identity) cnf(296340,plain, ( ~ equalish(X1,multiply(X2,a)) | equalish(X1,a) | ~ equalish(X2,multiplicative_identity) ), inference('resolution, passive clause reanimation',[status(thm)],[11707,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#296340 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(X1,a),a) | ~ equalish(X1,multiplicative_identity) cnf(11707,plain, ( equalish(multiply(X1,a),a) | ~ equalish(X1,multiplicative_identity) ), inference('resolution, forward subsumption resolution, passive clause reanimation',[status(thm)],[8675,55,28])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#11707 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ equalish(X1,multiply(multiplicative_identity,a)) | equalish(X1,a) cnf(8675,plain, ( ~ equalish(X1,multiply(multiplicative_identity,a)) | equalish(X1,a) ), inference('resolution, passive clause reanimation',[status(thm)],[958,53])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#8675 TPTP Formula 0 2010-01-21T09:09:00-05:00 equalish(multiply(multiplicative_identity,a),a) cnf(958,plain, ( equalish(multiply(multiplicative_identity,a),a) ), inference('resolution, passive clause reanimation',[status(thm)],[28,38])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#958 TPTP Formula 0 2010-01-21T09:09:00-05:00 ~ defined(X0) | ~ defined(X1) | defined(multiply(X0,X1)) cnf(44,plain, ( ~ defined(X0) | ~ defined(X1) | defined(multiply(X0,X1)) ), inference(normalize,[status(thm)],[13])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#44 TPTP Formula 0 2010-01-21T09:09:00-05:00 defined(multiply(X0,X1)) | ~ defined(X0) | ~ defined(X1) cnf(13,axiom, ( defined(multiply(X0,X1)) | ~ defined(X0) | ~ defined(X1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=FLD&File=FLD038-1&System=Vampire---11.0.UNS-Ref.s#13 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown 2010-01-21T09:09:00-05:00 ~ defined(X0) | defined(multiplicative_inverse(X0)) | equalish(X0,additive_identity) cnf(45,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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#45 TPTP Formula 0 2010-01-21T09:09:00-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=FLD038-1&System=Vampire---11.0.UNS-Ref.s#15 TPTP Formula 0 2010-01-21T09:09:00-05:00 file://input unknown