2008-07-18T03:51:33-04:00 $false cnf(1238559,negated_conjecture, ( $false ), inference(rw,[status(thm)],[3,1238393,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1238559 0 2008-07-18T03:51:33-04:00 $false cnf(1238561,negated_conjecture, ( $false ), 1238560, [proof]). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1238561 0 2008-07-18T03:51:33-04:00 $false cnf(1238560,negated_conjecture, ( $false ), inference(cn,[status(thm)],[1238559,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1238560 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(X2,X2)),X2)) cnf(1238393,plain, ( is_a_theorem(or(not(or(X2,X2)),X2)) ), inference(spm,[status(thm)],[1051975,1235824,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1238393 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(or(X1,X1)),X1))) cnf(1235824,plain, ( is_a_theorem(or(X2,or(not(or(X1,X1)),X1))) ), inference(spm,[status(thm)],[1231601,1227812,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1235824 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(or(not(or(X2,X2)),X1),or(X3,X2))) cnf(1227812,plain, ( is_a_theorem(or(or(not(or(X2,X2)),X1),or(X3,X2))) ), inference(spm,[status(thm)],[1227216,157616,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1227812 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(or(not(or(X1,X2)),X3),or(X4,X1)))) cnf(157616,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(or(not(or(X1,X2)),X3),or(X4,X1)))) ), inference(spm,[status(thm)],[4,152836,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#157616 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(or(not(or(X2,X3)),X4),or(X3,X1)))) cnf(152836,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(or(not(or(X2,X3)),X4),or(X3,X1)))) ), inference(spm,[status(thm)],[4,151692,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#152836 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(or(not(X1),X3),X1))) cnf(151692,plain, ( is_a_theorem(or(X2,or(or(not(X1),X3),X1))) ), inference(spm,[status(thm)],[121634,138514,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#151692 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(not(or(X2,not(X2)))),X1)) cnf(138514,plain, ( is_a_theorem(or(not(not(or(X2,not(X2)))),X1)) ), inference(spm,[status(thm)],[138444,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#138514 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(not(X2),X1)),or(X3,or(X4,X5)))),or(not(or(not(X4),X2)),or(X3,or(X5,X2))))) cnf(2,axiom, ( is_a_theorem(or(not(or(not(or(not(X2),X1)),or(X3,or(X4,X5)))),or(not(or(not(X4),X2)),or(X3,or(X5,X2))))) ), file('/home/graph/tptp/TPTP/Problems/LCL/LCL005-1.p',an_CAMerideth)). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2 0 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=LCL&File=LCL005-1.p#an_CAMerideth an_CAMerideth 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(not(or(X2,not(X2)))),X1)) | ~ is_a_theorem(X3) cnf(138444,plain, ( is_a_theorem(or(not(not(or(X2,not(X2)))),X1)) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,137707,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#138444 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(not(or(X1,not(X1)))),X3))) cnf(137707,plain, ( is_a_theorem(or(X2,or(not(not(or(X1,not(X1)))),X3))) ), inference(spm,[status(thm)],[120491,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#137707 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(not(or(X1,not(X1)))),X3))) | ~ is_a_theorem(X4) cnf(120491,plain, ( is_a_theorem(or(X2,or(not(not(or(X1,not(X1)))),X3))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,120371,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#120491 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(not(or(X3,not(X3)))),X4)))) cnf(120371,plain, ( is_a_theorem(or(X2,or(X1,or(not(not(or(X3,not(X3)))),X4)))) ), inference(spm,[status(thm)],[9016,119503,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#120371 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(not(not(X2)),X1))) cnf(119503,plain, ( is_a_theorem(or(not(X2),or(not(not(X2)),X1))) ), inference(spm,[status(thm)],[117235,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#119503 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(not(not(X2)),X1))) | ~ is_a_theorem(X3) cnf(117235,plain, ( is_a_theorem(or(not(X2),or(not(not(X2)),X1))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[12838,116335,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#117235 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(not(X2)),X1)) | ~ is_a_theorem(X2) cnf(116335,plain, ( is_a_theorem(or(not(not(X2)),X1)) | ~ is_a_theorem(X2) ), inference(spm,[status(thm)],[116105,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#116335 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(not(X2)),X1)) | ~ is_a_theorem(X3) | ~ is_a_theorem(X2) cnf(116105,plain, ( is_a_theorem(or(not(not(X2)),X1)) | ~ is_a_theorem(X3) | ~ is_a_theorem(X2) ), inference(spm,[status(thm)],[1,115936,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#116105 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(not(X1)),X3))) | ~ is_a_theorem(X1) cnf(115936,plain, ( is_a_theorem(or(X2,or(not(not(X1)),X3))) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[1,115636,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#115936 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,or(not(not(X2)),X3)))) cnf(115636,plain, ( is_a_theorem(or(not(X2),or(X1,or(not(not(X2)),X3)))) ), inference(spm,[status(thm)],[12885,114693,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#115636 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X2,X1))) cnf(114693,plain, ( is_a_theorem(or(not(X2),or(X2,X1))) ), inference(spm,[status(thm)],[114235,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#114693 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X2,X1))) | ~ is_a_theorem(X3) cnf(114235,plain, ( is_a_theorem(or(not(X2),or(X2,X1))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,114156,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#114235 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X1,X3)))) cnf(114156,plain, ( is_a_theorem(or(X2,or(not(X1),or(X1,X3)))) ), inference(spm,[status(thm)],[6392,113174,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#114156 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,X2))) cnf(113174,plain, ( is_a_theorem(or(not(X2),or(X1,X2))) ), inference(spm,[status(thm)],[113012,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#113174 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,X2))) | ~ is_a_theorem(X3) cnf(113012,plain, ( is_a_theorem(or(not(X2),or(X1,X2))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,113006,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#113012 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X3,X1)))) cnf(113006,plain, ( is_a_theorem(or(X2,or(not(X1),or(X3,X1)))) ), inference(spm,[status(thm)],[112350,17930,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#113006 0 2008-07-18T03:51:33-04:00 is_a_theorem(not(not(or(X2,not(X2))))) cnf(17930,plain, ( is_a_theorem(not(not(or(X2,not(X2))))) ), inference(spm,[status(thm)],[17864,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#17930 0 2008-07-18T03:51:33-04:00 is_a_theorem(not(not(or(X2,not(X2))))) | ~ is_a_theorem(X1) cnf(17864,plain, ( is_a_theorem(not(not(or(X2,not(X2))))) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[1,17646,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#17864 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(not(or(X1,not(X1)))))) cnf(17646,plain, ( is_a_theorem(or(X2,not(not(or(X1,not(X1)))))) ), inference(spm,[status(thm)],[16728,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#17646 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(not(or(X1,not(X1)))))) | ~ is_a_theorem(X3) cnf(16728,plain, ( is_a_theorem(or(X2,not(not(or(X1,not(X1)))))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,16591,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#16728 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,not(not(or(X3,not(X3))))))) cnf(16591,plain, ( is_a_theorem(or(X2,or(X1,not(not(or(X3,not(X3))))))) ), inference(spm,[status(thm)],[9016,16358,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#16591 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),not(not(X2)))) cnf(16358,plain, ( is_a_theorem(or(not(X2),not(not(X2)))) ), inference(spm,[status(thm)],[16284,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#16358 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),not(not(X2)))) | ~ is_a_theorem(X1) cnf(16284,plain, ( is_a_theorem(or(not(X2),not(not(X2)))) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[1,16085,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#16284 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),not(not(X1))))) cnf(16085,plain, ( is_a_theorem(or(X2,or(not(X1),not(not(X1))))) ), inference(spm,[status(thm)],[15964,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#16085 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),not(not(X1))))) | ~ is_a_theorem(X3) cnf(15964,plain, ( is_a_theorem(or(X2,or(not(X1),not(not(X1))))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,15767,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#15964 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X3),not(not(X3)))))) cnf(15767,plain, ( is_a_theorem(or(X2,or(X1,or(not(X3),not(not(X3)))))) ), inference(spm,[status(thm)],[11884,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#15767 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X3),not(not(X3)))))) | ~ is_a_theorem(X4) cnf(11884,plain, ( is_a_theorem(or(X2,or(X1,or(not(X3),not(not(X3)))))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,11868,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#11884 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,or(not(X4),not(not(X4))))))) cnf(11868,plain, ( is_a_theorem(or(X2,or(X1,or(X3,or(not(X4),not(not(X4))))))) ), inference(spm,[status(thm)],[9016,11297,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#11868 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(X2,not(not(X1)))),or(X3,or(X2,not(not(X1)))))) cnf(11297,plain, ( is_a_theorem(or(not(or(X2,not(not(X1)))),or(X3,or(X2,not(not(X1)))))) ), inference(spm,[status(thm)],[4625,11143,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#11297 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X2,not(not(X1))))) cnf(11143,plain, ( is_a_theorem(or(not(X2),or(X2,not(not(X1))))) ), inference(spm,[status(thm)],[10952,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#11143 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X2,not(not(X1))))) | ~ is_a_theorem(X3) cnf(10952,plain, ( is_a_theorem(or(not(X2),or(X2,not(not(X1))))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,10823,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10952 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X1,not(not(X3)))))) cnf(10823,plain, ( is_a_theorem(or(X2,or(not(X1),or(X1,not(not(X3)))))) ), inference(spm,[status(thm)],[10427,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10823 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X1,not(not(X3)))))) | ~ is_a_theorem(X4) cnf(10427,plain, ( is_a_theorem(or(X2,or(not(X1),or(X1,not(not(X3)))))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,10388,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10427 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X3),or(X3,not(not(X4))))))) cnf(10388,plain, ( is_a_theorem(or(X2,or(X1,or(not(X3),or(X3,not(not(X4))))))) ), inference(spm,[status(thm)],[9016,4626,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10388 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X3),or(X3,X1)))) cnf(4626,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X3),or(X3,X1)))) ), inference(spm,[status(thm)],[4,4430,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4626 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X3,X1)))) cnf(4430,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X3,X1)))) ), inference(spm,[status(thm)],[3769,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4430 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X3,X1)))) | ~ is_a_theorem(X4) cnf(3769,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X3,X1)))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,3337,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#3769 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(X4,X3))))) cnf(3337,plain, ( is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(X4,X3))))) ), inference(spm,[status(thm)],[57,3290,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#3337 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X2)),or(not(X2),or(X1,X2)))) cnf(3290,plain, ( is_a_theorem(or(not(or(not(X2),X2)),or(not(X2),or(X1,X2)))) ), inference(spm,[status(thm)],[4,3260,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#3290 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X2),or(X2,X1)))) cnf(3260,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X2),or(X2,X1)))) ), inference(spm,[status(thm)],[4,3083,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#3260 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X1,X1)))) cnf(3083,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X1,X1)))) ), inference(spm,[status(thm)],[2983,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#3083 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X1,X1)))) | ~ is_a_theorem(X3) cnf(2983,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(X1,X1)))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,2982,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2983 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(X3,X3))))) cnf(2982,plain, ( is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(X3,X3))))) ), inference(spm,[status(thm)],[57,2933,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2982 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(not(X2),or(X1,X2))),X3)),or(not(X4),or(X4,X3)))) cnf(2933,plain, ( is_a_theorem(or(not(or(not(or(not(X2),or(X1,X2))),X3)),or(not(X4),or(X4,X3)))) ), inference(spm,[status(thm)],[4,2762,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2933 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(or(not(X3),or(X4,X3)),X1)))) cnf(2762,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(or(not(X3),or(X4,X3)),X1)))) ), inference(spm,[status(thm)],[2567,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2762 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(or(not(X3),or(X4,X3)),X1)))) | ~ is_a_theorem(X5) cnf(2567,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X1),or(or(not(X3),or(X4,X3)),X1)))) | ~ is_a_theorem(X5) ), inference(spm,[status(thm)],[1,2554,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2567 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(or(not(X4),or(X5,X4)),X3))))) cnf(2554,plain, ( is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(or(not(X4),or(X5,X4)),X3))))) ), inference(spm,[status(thm)],[57,58,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#2554 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(not(or(not(X2),X1))),X3)),or(X4,or(or(not(X1),or(X5,X1)),X3)))) cnf(58,plain, ( is_a_theorem(or(not(or(not(not(or(not(X2),X1))),X3)),or(X4,or(or(not(X1),or(X5,X1)),X3)))) ), inference(spm,[status(thm)],[4,42,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#58 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),or(not(X1),or(X3,X1)))),or(X4,or(not(or(not(X5),X1)),or(not(X1),or(X3,X1)))))) cnf(42,plain, ( is_a_theorem(or(not(or(not(X2),or(not(X1),or(X3,X1)))),or(X4,or(not(or(not(X5),X1)),or(not(X1),or(X3,X1)))))) ), inference(spm,[status(thm)],[10,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#42 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(X4,X1)))) | ~ is_a_theorem(or(not(or(not(X1),X5)),or(X4,X1))) cnf(10,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(X4,X1)))) | ~ is_a_theorem(or(not(or(not(X1),X5)),or(X4,X1))) ), inference(spm,[status(thm)],[1,9,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(not(X2),X1)),or(X3,X2))),or(not(or(not(X4),X2)),or(X5,or(X3,X2))))) cnf(9,plain, ( is_a_theorem(or(not(or(not(or(not(X2),X1)),or(X3,X2))),or(not(or(not(X4),X2)),or(X5,or(X3,X2))))) ), inference(spm,[status(thm)],[4,7,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#9 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(X2,X1)),X3)),or(not(or(not(X4),X1)),or(or(not(X1),X5),X3)))) cnf(7,plain, ( is_a_theorem(or(not(or(not(or(X2,X1)),X3)),or(not(or(not(X4),X1)),or(or(not(X1),X5),X3)))) ), inference(spm,[status(thm)],[4,5,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#7 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),or(not(X1),X3))),or(not(or(not(X4),X1)),or(or(X5,X1),or(not(X1),X3))))) cnf(5,plain, ( is_a_theorem(or(not(or(not(X2),or(not(X1),X3))),or(not(or(not(X4),X1)),or(or(X5,X1),or(not(X1),X3))))) ), inference(spm,[status(thm)],[4,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#5 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(X4,X1)))) | ~ is_a_theorem(or(not(or(not(X1),X5)),or(X3,or(X2,X4)))) cnf(4,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(X4,X1)))) | ~ is_a_theorem(or(not(or(not(X1),X5)),or(X3,or(X2,X4)))) ), inference(spm,[status(thm)],[1,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4 0 2008-07-18T03:51:33-04:00 is_a_theorem(X1) | ~ is_a_theorem(or(not(X2),X1)) | ~ is_a_theorem(X2) cnf(1,axiom, ( is_a_theorem(X1) | ~ is_a_theorem(or(not(X2),X1)) | ~ is_a_theorem(X2) ), file('/home/graph/tptp/TPTP/Problems/LCL/LCL005-1.p',condensed_detachment)). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1 0 http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=LCL&File=LCL005-1.p#condensed_detachment condensed_detachment 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(X4,X3))))) | ~ is_a_theorem(or(not(X5),or(not(X3),or(X4,X3)))) cnf(57,plain, ( is_a_theorem(or(X2,or(not(or(not(X1),X3)),or(not(X3),or(X4,X3))))) | ~ is_a_theorem(or(not(X5),or(not(X3),or(X4,X3)))) ), inference(spm,[status(thm)],[1,42,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#57 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(or(not(or(X4,not(X4))),X3)) cnf(9016,plain, ( is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(or(not(or(X4,not(X4))),X3)) ), inference(spm,[status(thm)],[1,8978,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#9016 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(X2,not(X2))),X1)),or(X3,or(X4,X1)))) cnf(8978,plain, ( is_a_theorem(or(not(or(not(or(X2,not(X2))),X1)),or(X3,or(X4,X1)))) ), inference(spm,[status(thm)],[4,8943,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#8978 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(or(X4,not(X4)),X1)))) cnf(8943,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(or(X4,not(X4)),X1)))) ), inference(spm,[status(thm)],[4,6451,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#8943 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),or(X1,not(X1)))),or(X3,or(X4,or(X1,not(X1)))))) cnf(6451,plain, ( is_a_theorem(or(not(or(not(X2),or(X1,not(X1)))),or(X3,or(X4,or(X1,not(X1)))))) ), inference(spm,[status(thm)],[10,6420,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#6451 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(X2,X1)),not(X2))),or(X3,or(X4,not(X2))))) cnf(6420,plain, ( is_a_theorem(or(not(or(not(or(X2,X1)),not(X2))),or(X3,or(X4,not(X2))))) ), inference(spm,[status(thm)],[4,6393,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#6420 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(not(X2)),X1)),or(X3,or(or(X2,X4),X1)))) cnf(6393,plain, ( is_a_theorem(or(not(or(not(not(X2)),X1)),or(X3,or(or(X2,X4),X1)))) ), inference(spm,[status(thm)],[4,4663,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#6393 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),or(X1,X3))),or(X4,or(not(X1),or(X1,X3))))) cnf(4663,plain, ( is_a_theorem(or(not(or(not(X2),or(X1,X3))),or(X4,or(not(X1),or(X1,X3))))) ), inference(spm,[status(thm)],[10,4626,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4663 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,X2))) | ~ is_a_theorem(or(not(X3),X2)) cnf(4625,plain, ( is_a_theorem(or(not(X2),or(X1,X2))) | ~ is_a_theorem(or(not(X3),X2)) ), inference(spm,[status(thm)],[1,4430,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4625 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X3,X1)))) | ~ is_a_theorem(not(X4)) cnf(112350,plain, ( is_a_theorem(or(X2,or(not(X1),or(X3,X1)))) | ~ is_a_theorem(not(X4)) ), inference(spm,[status(thm)],[5144,112232,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#112350 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(X2) cnf(112232,plain, ( is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(X2) ), inference(spm,[status(thm)],[1,111265,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#112232 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X2,or(X1,X3)))) cnf(111265,plain, ( is_a_theorem(or(not(X2),or(X2,or(X1,X3)))) ), inference(spm,[status(thm)],[111160,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#111265 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X2,or(X1,X3)))) | ~ is_a_theorem(X4) cnf(111160,plain, ( is_a_theorem(or(not(X2),or(X2,or(X1,X3)))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,109870,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#111160 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X1,or(X3,X4))))) cnf(109870,plain, ( is_a_theorem(or(X2,or(not(X1),or(X1,or(X3,X4))))) ), inference(spm,[status(thm)],[6392,8978,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#109870 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X1,X3)))) | ~ is_a_theorem(or(not(X4),or(X1,X3))) cnf(6392,plain, ( is_a_theorem(or(X2,or(not(X1),or(X1,X3)))) | ~ is_a_theorem(or(not(X4),or(X1,X3))) ), inference(spm,[status(thm)],[1,4663,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#6392 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X3,X1)))) | ~ is_a_theorem(or(not(X4),or(X3,X1))) cnf(5144,plain, ( is_a_theorem(or(X2,or(not(X1),or(X3,X1)))) | ~ is_a_theorem(or(not(X4),or(X3,X1))) ), inference(spm,[status(thm)],[1,4629,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#5144 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),or(X1,X3))),or(X4,or(not(X3),or(X1,X3))))) cnf(4629,plain, ( is_a_theorem(or(not(or(not(X2),or(X1,X3))),or(X4,or(not(X3),or(X1,X3))))) ), inference(spm,[status(thm)],[10,4430,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4629 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,X3))) | ~ is_a_theorem(or(not(not(not(X2))),X3)) cnf(12885,plain, ( is_a_theorem(or(not(X2),or(X1,X3))) | ~ is_a_theorem(or(not(not(not(X2))),X3)) ), inference(spm,[status(thm)],[1,12839,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#12885 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(not(not(X2))),X1)),or(not(X2),or(X3,X1)))) cnf(12839,plain, ( is_a_theorem(or(not(or(not(not(not(X2))),X1)),or(not(X2),or(X3,X1)))) ), inference(spm,[status(thm)],[4,12765,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#12839 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X3),or(not(not(X3)),X1)))) cnf(12765,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X3),or(not(not(X3)),X1)))) ), inference(spm,[status(thm)],[4,12609,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#12765 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X3,not(not(X1)))))) cnf(12609,plain, ( is_a_theorem(or(X2,or(not(X1),or(X3,not(not(X1)))))) ), inference(spm,[status(thm)],[10485,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#12609 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),or(X3,not(not(X1)))))) | ~ is_a_theorem(X4) cnf(10485,plain, ( is_a_theorem(or(X2,or(not(X1),or(X3,not(not(X1)))))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,10389,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10485 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X3),or(X4,not(not(X3))))))) cnf(10389,plain, ( is_a_theorem(or(X2,or(X1,or(not(X3),or(X4,not(not(X3))))))) ), inference(spm,[status(thm)],[9016,4660,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#10389 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(X2),or(X3,X1)))) cnf(4660,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(X2),or(X3,X1)))) ), inference(spm,[status(thm)],[4,4626,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4660 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(not(not(X2)),X1))) | ~ is_a_theorem(or(not(X3),X1)) cnf(12838,plain, ( is_a_theorem(or(not(X2),or(not(not(X2)),X1))) | ~ is_a_theorem(or(not(X3),X1)) ), inference(spm,[status(thm)],[1,12765,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#12838 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(or(not(X1),X3),X1))) | ~ is_a_theorem(or(not(X4),X1)) cnf(121634,plain, ( is_a_theorem(or(X2,or(or(not(X1),X3),X1))) | ~ is_a_theorem(or(not(X4),X1)) ), inference(spm,[status(thm)],[1,115605,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#121634 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(or(not(X1),X4),X1)))) cnf(115605,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(or(not(X1),X4),X1)))) ), inference(spm,[status(thm)],[10,114693,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#115605 0 2008-07-18T03:51:33-04:00 is_a_theorem(X2) | ~ is_a_theorem(or(not(or(not(X1),X1)),X2)) cnf(1227216,plain, ( is_a_theorem(X2) | ~ is_a_theorem(or(not(or(not(X1),X1)),X2)) ), inference(spm,[status(thm)],[877805,1223622,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1227216 0 2008-07-18T03:51:33-04:00 is_a_theorem(not(not(not(not(or(not(X2),X2)))))) cnf(1223622,plain, ( is_a_theorem(not(not(not(not(or(not(X2),X2)))))) ), inference(spm,[status(thm)],[1059578,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1223622 0 2008-07-18T03:51:33-04:00 is_a_theorem(not(not(not(not(or(not(X2),X2)))))) | ~ is_a_theorem(X1) cnf(1059578,plain, ( is_a_theorem(not(not(not(not(or(not(X2),X2)))))) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[853225,1059336,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1059578 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(not(or(not(X2),X2))),X1)) cnf(1059336,plain, ( is_a_theorem(or(not(not(or(not(X2),X2))),X1)) ), inference(spm,[status(thm)],[844877,1059111,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1059336 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(not(or(not(X1),X1))))) cnf(1059111,plain, ( is_a_theorem(or(X2,not(not(or(not(X1),X1))))) ), inference(spm,[status(thm)],[1051975,1056095,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1059111 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,not(not(or(not(X3),X3)))))) cnf(1056095,plain, ( is_a_theorem(or(X2,or(X1,not(not(or(not(X3),X3)))))) ), inference(spm,[status(thm)],[1051975,258791,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1056095 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(not(X2),X2)),X1)),or(X3,or(X4,X1)))) cnf(258791,plain, ( is_a_theorem(or(not(or(not(or(not(X2),X2)),X1)),or(X3,or(X4,X1)))) ), inference(spm,[status(thm)],[4,252786,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#258791 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(or(not(X4),X4),X1)))) cnf(252786,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(or(not(X4),X4),X1)))) ), inference(spm,[status(thm)],[4,252357,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#252786 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,or(not(X4),X4))))) cnf(252357,plain, ( is_a_theorem(or(X2,or(X1,or(X3,or(not(X4),X4))))) ), inference(spm,[status(thm)],[145068,218518,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#252357 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(X2,X1)),X3)),or(X4,or(not(X3),X3)))) cnf(218518,plain, ( is_a_theorem(or(not(or(not(or(X2,X1)),X3)),or(X4,or(not(X3),X3)))) ), inference(spm,[status(thm)],[4,212345,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#218518 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),not(X2))),or(X1,or(or(X3,X4),not(X2))))) cnf(212345,plain, ( is_a_theorem(or(not(or(not(X2),not(X2))),or(X1,or(or(X3,X4),not(X2))))) ), inference(spm,[status(thm)],[4717,211290,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#212345 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(not(X2)),X1)),or(X2,or(X3,X1)))) cnf(211290,plain, ( is_a_theorem(or(not(or(not(not(X2)),X1)),or(X2,or(X3,X1)))) ), inference(spm,[status(thm)],[4,210448,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#211290 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X1),X3)))) cnf(210448,plain, ( is_a_theorem(or(X2,or(X1,or(not(X1),X3)))) ), inference(spm,[status(thm)],[210333,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#210448 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X1),X3)))) | ~ is_a_theorem(X4) cnf(210333,plain, ( is_a_theorem(or(X2,or(X1,or(not(X1),X3)))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,209489,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#210333 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,or(not(X3),X4))))) cnf(209489,plain, ( is_a_theorem(or(X2,or(X1,or(X3,or(not(X3),X4))))) ), inference(spm,[status(thm)],[167621,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#209489 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,or(not(X3),X4))))) | ~ is_a_theorem(X5) cnf(167621,plain, ( is_a_theorem(or(X2,or(X1,or(X3,or(not(X3),X4))))) | ~ is_a_theorem(X5) ), inference(spm,[status(thm)],[1,163565,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#167621 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,or(X4,or(not(X4),X5)))))) cnf(163565,plain, ( is_a_theorem(or(X2,or(X1,or(X3,or(X4,or(not(X4),X5)))))) ), inference(spm,[status(thm)],[125566,145069,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#163565 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),or(not(X1),X3))),or(X4,or(X1,or(not(X1),X3))))) cnf(145069,plain, ( is_a_theorem(or(not(or(not(X2),or(not(X1),X3))),or(X4,or(X1,or(not(X1),X3))))) ), inference(spm,[status(thm)],[4,144785,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#145069 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(not(X2),X1)),X2)),or(X3,or(X4,X2)))) cnf(144785,plain, ( is_a_theorem(or(not(or(not(or(not(X2),X1)),X2)),or(X3,or(X4,X2)))) ), inference(spm,[status(thm)],[4717,114693,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#144785 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(X4,X1)))) | ~ is_a_theorem(or(not(or(not(X1),X5)),or(X2,X4))) cnf(4717,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(X3,or(X4,X1)))) | ~ is_a_theorem(or(not(or(not(X1),X5)),or(X2,X4))) ), inference(spm,[status(thm)],[4,4691,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4717 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,X3))) | ~ is_a_theorem(or(not(X2),X3)) cnf(4691,plain, ( is_a_theorem(or(not(X2),or(X1,X3))) | ~ is_a_theorem(or(not(X2),X3)) ), inference(spm,[status(thm)],[1,4660,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#4691 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(or(not(or(not(X1),X4)),X3)) cnf(125566,plain, ( is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(or(not(or(not(X1),X4)),X3)) ), inference(spm,[status(thm)],[1,121635,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#125566 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(or(not(X2),X1)),X3)),or(X4,or(X2,X3)))) cnf(121635,plain, ( is_a_theorem(or(not(or(not(or(not(X2),X1)),X3)),or(X4,or(X2,X3)))) ), inference(spm,[status(thm)],[4,115605,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#121635 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(or(not(or(not(X3),X4)),X3)) cnf(145068,plain, ( is_a_theorem(or(X2,or(X1,X3))) | ~ is_a_theorem(or(not(or(not(X3),X4)),X3)) ), inference(spm,[status(thm)],[1,144785,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#145068 0 2008-07-18T03:51:33-04:00 is_a_theorem(X2) | ~ is_a_theorem(or(not(or(X1,not(X1))),X2)) cnf(1051975,plain, ( is_a_theorem(X2) | ~ is_a_theorem(or(not(or(X1,not(X1))),X2)) ), inference(spm,[status(thm)],[877805,63545,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#1051975 0 2008-07-18T03:51:33-04:00 is_a_theorem(not(not(not(not(or(X2,not(X2))))))) cnf(63545,plain, ( is_a_theorem(not(not(not(not(or(X2,not(X2))))))) ), inference(spm,[status(thm)],[63453,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#63545 0 2008-07-18T03:51:33-04:00 is_a_theorem(not(not(not(not(or(X2,not(X2))))))) | ~ is_a_theorem(X1) cnf(63453,plain, ( is_a_theorem(not(not(not(not(or(X2,not(X2))))))) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[1,62745,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#63453 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(not(not(not(or(X1,not(X1)))))))) cnf(62745,plain, ( is_a_theorem(or(X2,not(not(not(not(or(X1,not(X1)))))))) ), inference(spm,[status(thm)],[62654,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#62745 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(not(not(not(or(X1,not(X1)))))))) | ~ is_a_theorem(X3) cnf(62654,plain, ( is_a_theorem(or(X2,not(not(not(not(or(X1,not(X1)))))))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,61945,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#62654 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,not(not(not(not(or(X3,not(X3))))))))) cnf(61945,plain, ( is_a_theorem(or(X2,or(X1,not(not(not(not(or(X3,not(X3))))))))) ), inference(spm,[status(thm)],[29075,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#61945 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,not(not(not(not(or(X3,not(X3))))))))) | ~ is_a_theorem(X4) cnf(29075,plain, ( is_a_theorem(or(X2,or(X1,not(not(not(not(or(X3,not(X3))))))))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,28053,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#29075 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,not(not(not(not(or(X4,not(X4)))))))))) cnf(28053,plain, ( is_a_theorem(or(X2,or(X1,or(X3,not(not(not(not(or(X4,not(X4)))))))))) ), inference(spm,[status(thm)],[9016,27808,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#28053 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),or(X1,not(not(not(not(X2))))))) cnf(27808,plain, ( is_a_theorem(or(not(X2),or(X1,not(not(not(not(X2))))))) ), inference(spm,[status(thm)],[12885,16358,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#27808 0 2008-07-18T03:51:33-04:00 is_a_theorem(X2) | ~ is_a_theorem(not(not(not(X1)))) | ~ is_a_theorem(or(X1,X2)) cnf(877805,plain, ( is_a_theorem(X2) | ~ is_a_theorem(not(not(not(X1)))) | ~ is_a_theorem(or(X1,X2)) ), inference(spm,[status(thm)],[875415,853375,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#877805 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(not(X2)),X1)) | ~ is_a_theorem(or(X2,X1)) cnf(853375,plain, ( is_a_theorem(or(not(not(X2)),X1)) | ~ is_a_theorem(or(X2,X1)) ), inference(spm,[status(thm)],[844877,844427,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#853375 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(not(X1)))) | ~ is_a_theorem(or(X1,X2)) cnf(844427,plain, ( is_a_theorem(or(X2,not(not(X1)))) | ~ is_a_theorem(or(X1,X2)) ), inference(spm,[status(thm)],[843938,74536,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#844427 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(X2))) cnf(74536,plain, ( is_a_theorem(or(X2,not(X2))) ), inference(spm,[status(thm)],[74444,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#74536 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,not(X2))) | ~ is_a_theorem(X1) cnf(74444,plain, ( is_a_theorem(or(X2,not(X2))) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[1,73712,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#74444 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,not(X1)))) cnf(73712,plain, ( is_a_theorem(or(X2,or(X1,not(X1)))) ), inference(spm,[status(thm)],[73612,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#73712 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,not(X1)))) | ~ is_a_theorem(X3) cnf(73612,plain, ( is_a_theorem(or(X2,or(X1,not(X1)))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,72878,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#73612 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,not(X3))))) cnf(72878,plain, ( is_a_theorem(or(X2,or(X1,or(X3,not(X3))))) ), inference(spm,[status(thm)],[72534,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#72878 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,not(X3))))) | ~ is_a_theorem(X4) cnf(72534,plain, ( is_a_theorem(or(X2,or(X1,or(X3,not(X3))))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,72500,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#72534 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(X3,or(X4,not(X4)))))) cnf(72500,plain, ( is_a_theorem(or(X2,or(X1,or(X3,or(X4,not(X4)))))) ), inference(spm,[status(thm)],[9016,71726,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#72500 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(X2,X1)),or(X3,or(X2,X1)))) cnf(71726,plain, ( is_a_theorem(or(not(or(X2,X1)),or(X3,or(X2,X1)))) ), inference(spm,[status(thm)],[71064,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#71726 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(X2,X1)),or(X3,or(X2,X1)))) | ~ is_a_theorem(X4) cnf(71064,plain, ( is_a_theorem(or(not(or(X2,X1)),or(X3,or(X2,X1)))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,70111,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#71064 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(or(X1,X3)),or(X4,or(X1,X3))))) cnf(70111,plain, ( is_a_theorem(or(X2,or(not(or(X1,X3)),or(X4,or(X1,X3))))) ), inference(spm,[status(thm)],[5144,8978,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#70111 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,X1)) | ~ is_a_theorem(or(X3,X2)) | ~ is_a_theorem(or(not(X3),X1)) cnf(843938,plain, ( is_a_theorem(or(X2,X1)) | ~ is_a_theorem(or(X3,X2)) | ~ is_a_theorem(or(not(X3),X1)) ), inference(spm,[status(thm)],[1,259131,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#843938 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(X2,X1)),or(X1,X3))) | ~ is_a_theorem(or(not(X2),X3)) cnf(259131,plain, ( is_a_theorem(or(not(or(X2,X1)),or(X1,X3))) | ~ is_a_theorem(or(not(X2),X3)) ), inference(spm,[status(thm)],[1,255065,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#259131 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(or(not(X2),X1)),or(not(or(X2,X3)),or(X3,X1)))) cnf(255065,plain, ( is_a_theorem(or(not(or(not(X2),X1)),or(not(or(X2,X3)),or(X3,X1)))) ), inference(spm,[status(thm)],[4,254156,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#255065 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),X1))) cnf(254156,plain, ( is_a_theorem(or(X2,or(not(X1),X1))) ), inference(spm,[status(thm)],[254065,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#254156 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(not(X1),X1))) | ~ is_a_theorem(X3) cnf(254065,plain, ( is_a_theorem(or(X2,or(not(X1),X1))) | ~ is_a_theorem(X3) ), inference(spm,[status(thm)],[1,253154,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#254065 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X3),X3)))) cnf(253154,plain, ( is_a_theorem(or(X2,or(X1,or(not(X3),X3)))) ), inference(spm,[status(thm)],[252785,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#253154 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,or(X1,or(not(X3),X3)))) | ~ is_a_theorem(X4) cnf(252785,plain, ( is_a_theorem(or(X2,or(X1,or(not(X3),X3)))) | ~ is_a_theorem(X4) ), inference(spm,[status(thm)],[1,252357,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#252785 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(X2,X1)) | ~ is_a_theorem(or(X1,X2)) cnf(844877,plain, ( is_a_theorem(or(X2,X1)) | ~ is_a_theorem(or(X1,X2)) ), inference(spm,[status(thm)],[843938,255153,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#844877 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),X2)) cnf(255153,plain, ( is_a_theorem(or(not(X2),X2)) ), inference(spm,[status(thm)],[255064,2,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=LCL&File=LCL005-1&System=EP---1.0pre.UNS-CRf.s#255153 0 2008-07-18T03:51:33-04:00 is_a_theorem(or(not(X2),X2)) | ~ is_a_theorem(X1) cnf(255064,plain, ( is_a_theorem(or(not(X2),X2)) | ~ is_a_theorem(X1) ), inference(spm,[status(thm)],[1,254156,theory(equality)])). TPTP Formula http://www.cs.miami.edu/~tptp