%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LAT393-1 : TPTP v8.1.0. Released v5.4.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 04:58:28 EDT 2022 % Result : Unsatisfiable 3.70s 4.09s % Output : CNFRefutation 3.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : LAT393-1 : TPTP v8.1.0. Released v5.4.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.11/0.33 % Computer : n007.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Thu Jun 30 00:07:23 EDT 2022 % 0.11/0.33 % CPUTime : % 3.70/4.09 Theorem Proved. % 3.70/4.09 % SZS status Unsatisfiable % 3.70/4.09 % SZS output start CNFRefutation % 3.70/4.09 [1=axiom,[], % 3.70/4.09 f(X10,X10) = neg(X10)]. % 3.70/4.09 [2=axiom,[1], % 3.70/4.09 neg(f(X10,X11)) = and(X10,X11)]. % 3.70/4.09 [3=axiom,[1,1], % 3.70/4.09 f(neg(X10),neg(X11)) = or(X10,X11)]. % 3.70/4.09 [4=axiom,[1], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,X12)),X13),f(X11,f(f(X11,f(neg(X10),X10)),X12))) = X11]. % 3.70/4.09 [5=axiom,[], % 3.70/4.09 thtop(X10,X10) = thmfalse]. % 3.70/4.09 [6=axiom,[1,2,1,2], % 3.70/4.09 thtop(f(x0,and(x1,x2)),f(x1,and(x0,x2))) = thmtrue]. % 3.70/4.09 [9=param(3,2),[], % 3.70/4.09 f(and(X10,X11),neg(X12)) = or(f(X10,X11),X12)]. % 3.70/4.09 [10=param(3,2),[], % 3.70/4.09 f(neg(X10),and(X11,X12)) = or(X10,f(X11,X12))]. % 3.70/4.09 [11=param(2,3),[], % 3.70/4.09 neg(or(X10,X11)) = and(neg(X10),neg(X11))]. % 3.70/4.09 [12=param(3,11),[], % 3.70/4.09 f(neg(X10),and(neg(X11),neg(X12))) = or(X10,or(X11,X12))]. % 3.70/4.09 [16=param(4,1),[1], % 3.70/4.09 f(f(neg(neg(X10)),X11),f(X10,f(f(X10,f(neg(X10),X10)),X10))) = X10]. % 3.70/4.09 [17=param(16,1),[], % 3.70/4.09 f(neg(neg(neg(X10))),f(X10,f(f(X10,f(neg(X10),X10)),X10))) = X10]. % 3.70/4.09 [18=param(2,16),[], % 3.70/4.09 and(f(neg(neg(X10)),X11),f(X10,f(f(X10,f(neg(X10),X10)),X10))) = neg(X10)]. % 3.70/4.09 [20=param(2,17),[], % 3.70/4.09 and(neg(neg(neg(X10))),f(X10,f(f(X10,f(neg(X10),X10)),X10))) = neg(X10)]. % 3.70/4.09 [24=param(4,1),[2], % 3.70/4.09 f(and(f(X10,X11),f(X11,X12)),f(X11,f(f(X11,f(neg(X10),X10)),X12))) = X11]. % 3.70/4.09 [25=param(4,1),[], % 3.70/4.09 f(f(f(neg(X10),f(X10,X11)),X12),f(X10,f(f(X10,f(neg(X10),X10)),X11))) = X10]. % 3.70/4.09 [26=param(4,1),[], % 3.70/4.09 f(f(f(f(X10,X11),neg(X11)),X12),f(X11,f(f(X11,f(neg(X10),X10)),X11))) = X11]. % 3.70/4.09 [28=param(24,1),[], % 3.70/4.09 f(and(f(X10,X11),neg(X11)),f(X11,f(f(X11,f(neg(X10),X10)),X11))) = X11]. % 3.70/4.09 [29=param(2,24),[], % 3.70/4.09 and(and(f(X11,X10),f(X10,X12)),f(X10,f(f(X10,f(neg(X11),X11)),X12))) = neg(X10)]. % 3.70/4.09 [31=param(2,28),[], % 3.70/4.09 and(and(f(X11,X10),neg(X10)),f(X10,f(f(X10,f(neg(X11),X11)),X10))) = neg(X10)]. % 3.70/4.09 [34=param(4,25),[3], % 3.70/4.09 f(X10,f(f(X10,X11),f(f(f(X10,X11),or(neg(X10),X10)),X12))) = f(X10,X11)]. % 3.70/4.09 [35=param(25,16),[3], % 3.70/4.09 f(X10,f(neg(X10),f(f(neg(X10),or(neg(X10),X10)),X11))) = neg(X10)]. % 3.70/4.09 [37=param(2,35),[], % 3.70/4.09 and(X10,f(neg(X10),f(f(neg(X10),or(neg(X10),X10)),X11))) = neg(neg(X10))]. % 3.70/4.09 [38=param(35,16),[], % 3.70/4.09 f(neg(X10),f(neg(neg(X10)),X10)) = neg(neg(X10))]. % 3.70/4.09 [40=param(38,3),[], % 3.70/4.09 f(neg(neg(X10)),or(neg(neg(X10)),X10)) = neg(neg(neg(X10)))]. % 3.70/4.09 [43=param(2,40),[], % 3.70/4.09 and(neg(neg(X10)),or(neg(neg(X10)),X10)) = neg(neg(neg(neg(X10))))]. % 3.70/4.09 [50=param(34,25),[], % 3.70/4.09 f(neg(X10),f(f(neg(X10),f(X10,X11)),X10)) = f(neg(X10),f(X10,X11))]. % 3.70/4.09 [51=param(34,26),[], % 3.70/4.09 f(f(X10,X11),f(f(f(X10,X11),neg(X11)),X11)) = f(f(X10,X11),neg(X11))]. % 3.70/4.09 [52=param(34,34),[], % 3.70/4.09 f(X10,f(f(X10,X11),or(neg(X10),X10))) = f(X10,X11)]. % 3.70/4.09 [55=param(2,52),[2], % 3.70/4.09 and(X10,f(f(X10,X11),or(neg(X10),X10))) = and(X10,X11)]. % 3.70/4.09 [65=param(2,50),[2], % 3.70/4.09 and(neg(X10),f(f(neg(X10),f(X10,X11)),X10)) = and(neg(X10),f(X10,X11))]. % 3.70/4.09 [68=param(2,51),[2], % 3.70/4.09 and(f(X10,X11),f(f(f(X10,X11),neg(X11)),X11)) = and(f(X10,X11),neg(X11))]. % 3.70/4.09 [77=param(2,4),[], % 3.70/4.09 and(f(f(f(X11,X10),f(X10,X12)),X13),f(X10,f(f(X10,f(neg(X11),X11)),X12))) = neg(X10)]. % 3.70/4.09 [81=param(16,3),[], % 3.70/4.09 f(f(neg(neg(neg(X10))),X11),f(neg(X10),f(f(neg(X10),or(neg(X10),X10)),neg(X10)))) = neg(X10)]. % 3.70/4.09 [107=param(4,1),[2], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,f(X11,f(neg(X10),X10)))),X12),f(X11,and(X11,f(neg(X10),X10)))) = X11]. % 3.70/4.09 [109=param(4,16),[3], % 3.70/4.09 f(f(X10,X11),f(X10,f(f(X10,or(neg(neg(X10)),neg(X10))),f(f(X10,f(neg(X10),X10)),X10)))) = X10]. % 3.70/4.09 [117=param(24,18),[3], % 3.70/4.09 f(neg(X10),f(X10,f(f(X10,or(neg(neg(X10)),neg(X10))),f(f(X10,f(neg(X10),X10)),X10)))) = X10]. % 3.70/4.09 [136=param(2,81),[], % 3.70/4.09 and(f(neg(neg(neg(X10))),X11),f(neg(X10),f(f(neg(X10),or(neg(X10),X10)),neg(X10)))) = neg(neg(X10))]. % 3.70/4.09 [142=param(109,1),[2], % 3.70/4.09 and(X10,f(f(X10,or(neg(neg(X10)),neg(X10))),f(f(X10,f(neg(X10),X10)),X10))) = X10]. % 3.70/4.09 [145=param(34,109),[1,2], % 3.70/4.09 f(X10,and(X10,X11)) = f(X10,X11)]. % 3.70/4.09 [150=demod(107),[145], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,f(X11,f(neg(X10),X10)))),X12),f(X11,f(neg(X10),X10))) = X11]. % 3.70/4.09 [153=param(35,109),[1], % 3.70/4.09 f(X10,neg(neg(X10))) = neg(X10)]. % 3.70/4.09 [157=param(37,109),[1], % 3.70/4.09 and(X10,neg(neg(X10))) = neg(neg(X10))]. % 3.70/4.09 [163=param(153,3),[], % 3.70/4.09 or(X10,neg(neg(X10))) = neg(neg(X10))]. % 3.70/4.09 [184=param(2,145),[2], % 3.70/4.09 and(X10,and(X10,X11)) = and(X10,X11)]. % 3.70/4.09 [185=param(4,145),[], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,X12)),X13),f(X11,f(f(X11,f(neg(X10),X10)),and(X11,X12)))) = X11]. % 3.70/4.09 [188=param(145,12),[3], % 3.70/4.09 or(X10,or(X10,X11)) = or(X10,X11)]. % 3.70/4.09 [194=param(145,20),[3,17], % 3.70/4.09 or(neg(neg(X10)),X10) = X10]. % 3.70/4.09 [195=demod(43),[194], % 3.70/4.09 and(neg(neg(X10)),X10) = neg(neg(neg(neg(X10))))]. % 3.70/4.09 [196=demod(40),[194], % 3.70/4.09 f(neg(neg(X10)),X10) = neg(neg(neg(X10)))]. % 3.70/4.09 [203=param(145,29),[9,24], % 3.70/4.09 or(f(f(X10,X11),f(X11,X12)),X11) = X11]. % 3.70/4.09 [205=param(145,31),[9,28], % 3.70/4.09 or(f(f(X10,X11),neg(X11)),X11) = X11]. % 3.70/4.09 [208=param(145,77),[4], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,X12)),X13),neg(X11)) = X11]. % 3.70/4.09 [212=param(194,2),[], % 3.70/4.09 or(neg(and(X10,X11)),f(X10,X11)) = f(X10,X11)]. % 3.70/4.09 [217=param(11,194),[195], % 3.70/4.09 neg(neg(neg(neg(neg(X10))))) = neg(X10)]. % 3.70/4.09 [223=param(153,217),[3,194], % 3.70/4.09 neg(neg(neg(neg(X10)))) = X10]. % 3.70/4.09 [225=demod(195),[223], % 3.70/4.09 and(neg(neg(X10)),X10) = X10]. % 3.70/4.09 [229=param(9,225),[196], % 3.70/4.09 f(X10,neg(X11)) = or(neg(neg(neg(X10))),X11)]. % 3.70/4.09 [237=demod(205),[229,2], % 3.70/4.09 or(or(neg(neg(and(X10,X11))),X11),X11) = X11]. % 3.70/4.09 [239=demod(68),[229,2], % 3.70/4.09 and(f(X10,X11),f(or(neg(neg(and(X10,X11))),X11),X11)) = and(f(X10,X11),neg(X11))]. % 3.70/4.09 [240=demod(51),[229,2,229,2], % 3.70/4.09 f(f(X10,X11),f(or(neg(neg(and(X10,X11))),X11),X11)) = or(neg(neg(and(X10,X11))),X11)]. % 3.70/4.09 [244=demod(136),[229,2], % 3.70/4.09 and(f(neg(neg(neg(X10))),X11),f(neg(X10),or(neg(neg(and(neg(X10),or(neg(X10),X10)))),X10))) = neg(neg(X10))]. % 3.70/4.09 [256=demod(208),[229,2], % 3.70/4.09 or(neg(neg(and(f(f(X10,X11),f(X11,X12)),X13))),X11) = X11]. % 3.70/4.09 [262=demod(9),[229], % 3.70/4.09 or(f(X10,X11),X12) = or(neg(neg(neg(and(X10,X11)))),X12)]. % 3.70/4.09 [266=demod(203),[262], % 3.70/4.09 or(neg(neg(neg(and(f(X10,X11),f(X11,X12))))),X11) = X11]. % 3.70/4.09 [268=param(10,225),[196], % 3.70/4.09 f(neg(X10),X11) = or(X10,neg(neg(neg(X11))))]. % 3.70/4.09 [278=demod(185),[268], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,X12)),X13),f(X11,f(f(X11,or(X10,neg(neg(neg(X10))))),and(X11,X12)))) = X11]. % 3.70/4.09 [281=demod(150),[268,268], % 3.70/4.09 f(f(f(f(X10,X11),f(X11,f(X11,or(X10,neg(neg(neg(X10))))))),X12),f(X11,or(X10,neg(neg(neg(X10)))))) = X11]. % 3.70/4.09 [286=demod(142),[268], % 3.70/4.09 and(X10,f(f(X10,or(neg(neg(X10)),neg(X10))),f(f(X10,or(X10,neg(neg(neg(X10))))),X10))) = X10]. % 3.70/4.09 [289=demod(109),[268], % 3.70/4.09 f(f(X10,X11),f(X10,f(f(X10,or(neg(neg(X10)),neg(X10))),f(f(X10,or(X10,neg(neg(neg(X10))))),X10)))) = X10]. % 3.70/4.09 [304=demod(10),[268], % 3.70/4.09 or(X10,f(X11,X12)) = or(X10,neg(neg(neg(and(X11,X12)))))]. % 3.70/4.09 [311=demod(212),[304,163], % 3.70/4.09 f(X10,X11) = neg(neg(neg(and(X10,X11))))]. % 3.70/4.09 [313=demod(229),[311], % 3.70/4.09 or(neg(neg(neg(X10))),X11) = neg(neg(neg(and(X10,neg(X11)))))]. % 3.70/4.09 [324=demod(289),[311,311,311,311,311,311,311], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X10,neg(neg(neg(and(neg(neg(neg(and(X10,or(neg(neg(X10)),neg(X10)))))),neg(neg(neg(and(neg(neg(neg(and(X10,or(X10,neg(neg(neg(X10)))))))),X10)))))))))))))))) = X10]. % 3.70/4.09 [325=demod(286),[311,311,311,311], % 3.70/4.09 and(X10,neg(neg(neg(and(neg(neg(neg(and(X10,or(neg(neg(X10)),neg(X10)))))),neg(neg(neg(and(neg(neg(neg(and(X10,or(X10,neg(neg(neg(X10)))))))),X10))))))))) = X10]. % 3.70/4.09 [326=demod(324),[325], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(X10))))))) = X10]. % 3.70/4.09 [329=demod(55),[311,311], % 3.70/4.09 and(X10,neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),or(neg(X10),X10)))))) = and(X10,X11)]. % 3.70/4.09 [331=demod(266),[311,311,313], % 3.70/4.09 neg(neg(neg(and(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,X12))))),neg(X11))))) = X11]. % 3.70/4.09 [332=demod(256),[311,311,311], % 3.70/4.09 or(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,X12)))))))),X13))),X11) = X11]. % 3.70/4.09 [341=demod(281),[311,311,311,311,311,311,311], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,neg(neg(neg(and(X11,or(X10,neg(neg(neg(X10)))))))))))))))),X12)))),neg(neg(neg(and(X11,or(X10,neg(neg(neg(X10)))))))))))) = X11]. % 3.70/4.09 [343=demod(278),[311,311,311,311,311,311,311,311], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,X12)))))))),X13)))),neg(neg(neg(and(X11,neg(neg(neg(and(neg(neg(neg(and(X11,or(X10,neg(neg(neg(X10)))))))),and(X11,X12))))))))))))) = X11]. % 3.70/4.09 [360=demod(240),[311,311,311], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(or(neg(neg(and(X10,X11))),X11),X11)))))))) = or(neg(neg(and(X10,X11))),X11)]. % 3.70/4.09 [361=demod(239),[311,311,311], % 3.70/4.09 and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(or(neg(neg(and(X10,X11))),X11),X11))))) = and(neg(neg(neg(and(X10,X11)))),neg(X11))]. % 3.70/4.09 [362=demod(360),[361], % 3.70/4.09 or(neg(neg(and(X10,X11))),X11) = neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(X11)))))]. % 3.70/4.09 [365=demod(237),[362,313], % 3.70/4.09 neg(neg(neg(and(and(neg(neg(neg(and(X10,X11)))),neg(X11)),neg(X11))))) = X11]. % 3.70/4.09 [371=demod(268),[311], % 3.70/4.09 or(X10,neg(neg(neg(X11)))) = neg(neg(neg(and(neg(X10),X11))))]. % 3.70/4.09 [381=demod(343),[371], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,X12)))))))),X13)))),neg(neg(neg(and(X11,neg(neg(neg(and(neg(neg(neg(and(X11,neg(neg(neg(and(neg(X10),X10)))))))),and(X11,X12))))))))))))) = X11]. % 3.70/4.09 [383=demod(341),[371,371], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,neg(neg(neg(and(X11,neg(neg(neg(and(neg(X10),X10)))))))))))))))),X12)))),neg(neg(neg(and(X11,neg(neg(neg(and(neg(X10),X10)))))))))))) = X11]. % 3.70/4.09 [392=demod(325),[371], % 3.70/4.09 and(X10,neg(neg(neg(and(neg(neg(neg(and(X10,or(neg(neg(X10)),neg(X10)))))),neg(neg(neg(and(neg(neg(neg(and(X10,neg(neg(neg(and(neg(X10),X10)))))))),X10))))))))) = X10]. % 3.70/4.09 [402=demod(12),[311], % 3.70/4.09 or(X10,or(X11,X12)) = neg(neg(neg(and(neg(X10),and(neg(X11),neg(X12))))))]. % 3.70/4.09 [403=demod(188),[402,184], % 3.70/4.09 or(X10,X11) = neg(neg(neg(and(neg(X10),neg(X11)))))]. % 3.70/4.09 [404=demod(392),[403], % 3.70/4.09 and(X10,neg(neg(neg(and(neg(neg(neg(and(X10,neg(neg(neg(and(neg(neg(neg(X10))),neg(neg(X10)))))))))),neg(neg(neg(and(neg(neg(neg(and(X10,neg(neg(neg(and(neg(X10),X10)))))))),X10))))))))) = X10]. % 3.70/4.09 [406=demod(332),[403], % 3.70/4.09 neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(X11,X12)))))))),X13)))),neg(X11))))) = X11]. % 3.70/4.09 [413=demod(329),[403], % 3.70/4.09 and(X10,neg(neg(neg(and(neg(neg(neg(and(X10,X11)))),neg(neg(neg(and(neg(neg(X10)),neg(X10)))))))))) = and(X10,X11)]. % 3.70/4.09 [421=demod(65),[311,311,311,311], % 3.70/4.09 and(neg(X10),neg(neg(neg(and(neg(neg(neg(and(neg(X10),neg(neg(neg(and(X10,X11)))))))),X10))))) = and(neg(X10),neg(neg(neg(and(X10,X11)))))]. % 3.70/4.09 [424=demod(117),[403,311,311,311,311,311,311,404,311,157,223], % 3.70/4.09 neg(neg(X10)) = X10]. % 3.70/4.09 [425=demod(225),[424], % 3.70/4.09 and(X10,X10) = X10]. % 3.70/4.09 [426=demod(311),[424], % 3.70/4.09 f(X10,X11) = neg(and(X10,X11))]. % 3.70/4.09 [427=demod(326),[424,424,424], % 3.70/4.09 neg(and(neg(and(X10,X11)),neg(X10))) = X10]. % 3.70/4.09 [430=demod(413),[424,424,424,424], % 3.70/4.09 and(X10,neg(and(neg(and(X10,X11)),neg(and(X10,neg(X10)))))) = and(X10,X11)]. % 3.70/4.09 [438=demod(403),[424], % 3.70/4.09 or(X10,X11) = neg(and(neg(X10),neg(X11)))]. % 3.70/4.09 [439=demod(421),[424,424,424,424], % 3.70/4.09 and(neg(X10),neg(and(neg(and(neg(X10),neg(and(X10,X11)))),X10))) = and(neg(X10),neg(and(X10,X11)))]. % 3.70/4.09 [444=demod(406),[424,424,424,424,424], % 3.70/4.09 neg(and(neg(and(neg(and(neg(and(X10,X11)),neg(and(X11,X12)))),X13)),neg(X11))) = X11]. % 3.70/4.09 [449=demod(331),[424,424,424], % 3.70/4.09 neg(and(and(neg(and(X10,X11)),neg(and(X11,X12))),neg(X11))) = X11]. % 3.70/4.09 [450=demod(365),[424,424], % 3.70/4.09 neg(and(and(neg(and(X10,X11)),neg(X11)),neg(X11))) = X11]. % 3.70/4.09 [461=demod(381),[424,424,424,424,424,424,424,424,424], % 3.70/4.09 neg(and(neg(and(neg(and(neg(and(X10,X11)),neg(and(X11,X12)))),X13)),neg(and(X11,neg(and(neg(and(X11,neg(and(neg(X10),X10)))),and(X11,X12))))))) = X11]. % 3.70/4.09 [468=demod(383),[424,424,424,424,424,424,424,424,424], % 3.70/4.09 neg(and(neg(and(neg(and(neg(and(X10,X11)),neg(and(X11,neg(and(X11,neg(and(neg(X10),X10)))))))),X12)),neg(and(X11,neg(and(neg(X10),X10)))))) = X11]. % 3.70/4.09 [508=demod(244),[424,426,438,424,424,438,426,424], % 3.70/4.09 and(neg(and(neg(X10),X11)),neg(and(neg(X10),neg(and(neg(and(neg(X10),neg(and(X10,neg(X10))))),neg(X10)))))) = X10]. % 3.70/4.09 [526=param(6,426),[426], % 3.70/4.09 thtop(neg(and(x0,and(x1,x2))),neg(and(x1,and(x0,x2)))) = thmtrue]. % 3.70/4.09 [527=param(427,424),[], % 3.70/4.09 neg(and(neg(and(neg(X10),X11)),X10)) = neg(X10)]. % 3.70/4.09 [528=demod(439),[527,425], % 3.70/4.09 and(neg(X10),neg(and(X10,X11))) = neg(X10)]. % 3.70/4.09 [530=demod(508),[528,424,528,424], % 3.70/4.09 and(neg(and(neg(X10),X11)),X10) = X10]. % 3.70/4.09 [534=param(424,427),[], % 3.70/4.09 and(neg(and(X10,X11)),neg(X10)) = neg(X10)]. % 3.70/4.09 [535=param(528,424),[424], % 3.70/4.09 and(X10,neg(and(neg(X10),X11))) = X10]. % 3.70/4.09 [537=param(528,534),[424,424,424], % 3.70/4.09 and(and(X10,X11),X10) = and(X10,X11)]. % 3.70/4.09 [541=param(424,450),[], % 3.70/4.09 and(and(neg(and(X11,X10)),neg(X10)),neg(X10)) = neg(X10)]. % 3.70/4.09 [542=param(541,424),[424,424], % 3.70/4.09 and(and(neg(and(X10,neg(X11))),X11),X11) = X11]. % 3.70/4.09 [548=param(537,542),[542], % 3.70/4.09 and(X10,and(neg(and(X11,neg(X10))),X10)) = X10]. % 3.70/4.09 [550=param(424,444),[], % 3.70/4.09 and(neg(and(neg(and(neg(and(X11,X10)),neg(and(X10,X12)))),X13)),neg(X10)) = neg(X10)]. % 3.70/4.09 [552=param(424,449),[], % 3.70/4.09 and(and(neg(and(X11,X10)),neg(and(X10,X12))),neg(X10)) = neg(X10)]. % 3.70/4.09 [557=param(552,534),[424,424,424], % 3.70/4.09 and(and(neg(and(X10,neg(and(X11,X12)))),X11),and(X11,X12)) = and(X11,X12)]. % 3.70/4.09 [559=param(552,537),[], % 3.70/4.09 and(and(neg(and(X10,X11)),neg(and(X10,X12))),neg(X10)) = neg(X10)]. % 3.70/4.09 [566=param(534,559),[424], % 3.70/4.09 and(X10,neg(and(neg(and(X10,X11)),neg(and(X10,X12))))) = neg(and(neg(and(X10,X11)),neg(and(X10,X12))))]. % 3.70/4.09 [567=demod(430),[566], % 3.70/4.09 neg(and(neg(and(X10,X11)),neg(and(X10,neg(X10))))) = and(X10,X11)]. % 3.70/4.09 [570=param(424,567),[], % 3.70/4.09 and(neg(and(X10,X11)),neg(and(X10,neg(X10)))) = neg(and(X10,X11))]. % 3.70/4.09 [573=param(570,534),[424,424,534,424], % 3.70/4.09 and(X10,neg(and(neg(and(X10,X11)),and(X10,X11)))) = X10]. % 3.70/4.09 [587=param(461,530),[424,424,424,573,535], % 3.70/4.09 neg(and(neg(and(and(X10,X11),X12)),neg(X10))) = X10]. % 3.70/4.09 [590=param(424,587),[], % 3.70/4.09 and(neg(and(and(X10,X11),X12)),neg(X10)) = neg(X10)]. % 3.70/4.09 [594=param(530,590),[424], % 3.70/4.09 and(X10,and(and(X10,X11),X12)) = and(and(X10,X11),X12)]. % 3.70/4.09 [597=param(590,541),[424,424,424], % 3.70/4.09 and(X10,and(X11,X10)) = and(X11,X10)]. % 3.70/4.09 [598=demod(548),[597], % 3.70/4.09 and(neg(and(X10,neg(X11))),X11) = X11]. % 3.70/4.09 [603=param(552,590),[424,424,424], % 3.70/4.09 and(and(neg(and(X10,neg(and(and(X11,X12),X13)))),X11),and(and(X11,X12),X13)) = and(and(X11,X12),X13)]. % 3.70/4.09 [609=param(528,597),[], % 3.70/4.09 and(neg(X10),neg(and(X11,X10))) = neg(X10)]. % 3.70/4.09 [610=param(535,597),[], % 3.70/4.09 and(X10,neg(and(X11,neg(X10)))) = X10]. % 3.70/4.09 [626=param(590,597),[], % 3.70/4.09 and(neg(and(and(X10,X11),X12)),neg(X11)) = neg(X11)]. % 3.70/4.09 [635=param(590,598),[424,424], % 3.70/4.09 and(neg(and(X10,X11)),and(X12,neg(X10))) = and(X12,neg(X10))]. % 3.70/4.09 [636=param(468,598),[424], % 3.70/4.09 and(X10,neg(and(neg(X11),X11))) = X10]. % 3.70/4.09 [668=param(550,636),[424,424,424], % 3.70/4.09 and(neg(and(and(X10,neg(X11)),X12)),X11) = X11]. % 3.70/4.09 [693=param(557,609),[424], % 3.70/4.09 and(and(X10,X11),and(X11,X10)) = and(X11,X10)]. % 3.70/4.09 [701=param(528,693),[], % 3.70/4.09 and(neg(and(X10,X11)),neg(and(X11,X10))) = neg(and(X10,X11))]. % 3.70/4.09 [702=param(534,693),[701], % 3.70/4.09 neg(and(X10,X11)) = neg(and(X11,X10))]. % 3.70/4.09 [705=param(537,693),[693,693], % 3.70/4.09 and(X10,X11) = and(X11,X10)]. % 3.70/4.09 [712=demod(626),[705], % 3.70/4.09 and(neg(X10),neg(and(and(X11,X10),X12))) = neg(X10)]. % 3.70/4.09 [721=demod(668),[705], % 3.70/4.09 and(X10,neg(and(and(X11,neg(X10)),X12))) = X10]. % 3.70/4.09 [730=demod(603),[705,705], % 3.70/4.09 and(and(and(X10,X11),X12),and(X10,neg(and(X13,neg(and(and(X10,X11),X12)))))) = and(and(X10,X11),X12)]. % 3.70/4.09 [741=param(528,702),[], % 3.70/4.09 and(neg(and(X10,X11)),neg(and(and(X11,X10),X12))) = neg(and(X11,X10))]. % 3.70/4.09 [747=param(610,702),[], % 3.70/4.09 and(and(X10,X11),neg(and(X12,neg(and(X11,X10))))) = and(X10,X11)]. % 3.70/4.09 [753=param(721,528),[], % 3.70/4.09 and(and(X10,X11),neg(and(neg(X10),X12))) = and(X10,X11)]. % 3.70/4.09 [828=param(609,712),[424,424,705,424], % 3.70/4.09 and(X10,and(and(X11,X10),X12)) = and(and(X11,X10),X12)]. % 3.70/4.09 [843=param(828,705),[594], % 3.70/4.09 and(and(X10,X11),X12) = and(and(X11,X10),X12)]. % 3.70/4.09 [859=param(843,705),[], % 3.70/4.09 and(and(X10,X11),X12) = and(X12,and(X11,X10))]. % 3.70/4.09 [909=param(702,859),[], % 3.70/4.09 neg(and(and(X10,X11),X12)) = neg(and(and(X11,X10),X12))]. % 3.70/4.09 [912=param(859,843),[], % 3.70/4.09 and(and(X10,X11),and(X12,X13)) = and(and(X13,X12),and(X11,X10))]. % 3.70/4.09 [925=param(635,702),[], % 3.70/4.09 and(neg(and(and(X10,X11),X12)),and(X13,neg(and(X11,X10)))) = and(X13,neg(and(X10,X11)))]. % 3.70/4.09 [927=param(635,843),[], % 3.70/4.09 and(neg(and(and(X10,X11),X12)),and(X13,neg(and(X11,X10)))) = and(X13,neg(and(X11,X10)))]. % 3.70/4.09 [928=demod(925),[927], % 3.70/4.09 and(X10,neg(and(X11,X12))) = and(X10,neg(and(X12,X11)))]. % 3.70/4.09 [1016=param(859,701),[701], % 3.70/4.09 and(neg(and(X10,X11)),X12) = and(X12,neg(and(X11,X10)))]. % 3.70/4.09 [1359=param(928,1016),[], % 3.70/4.10 and(neg(and(X10,X11)),neg(and(X12,X13))) = and(neg(and(X13,X12)),neg(and(X11,X10)))]. % 3.70/4.10 [1903=param(730,609),[424,705], % 3.70/4.10 and(and(X10,X11),and(and(X10,X12),X11)) = and(and(X10,X12),X11)]. % 3.70/4.10 [2136=param(1903,705),[], % 3.70/4.10 and(and(X10,X11),and(and(X11,X12),X10)) = and(and(X11,X12),X10)]. % 3.70/4.10 [2534=param(2136,597),[597], % 3.70/4.10 and(and(X10,X11),and(and(X12,X11),X10)) = and(and(X12,X11),X10)]. % 3.70/4.10 [2541=param(701,2136),[912,1359,912,2136,701,912], % 3.70/4.10 neg(and(and(X11,X10),and(X10,and(X11,X12)))) = neg(and(X10,and(X11,X12)))]. % 3.70/4.10 [2632=param(741,2534),[], % 3.70/4.10 and(neg(and(X10,X11)),neg(and(and(X12,X10),X11))) = neg(and(X11,X10))]. % 3.70/4.10 [2637=param(2534,753),[705,753], % 3.70/4.10 and(and(X10,X11),and(neg(and(neg(X10),X12)),X11)) = and(X10,X11)]. % 3.70/4.10 [3003=param(1903,2637),[705,2637], % 3.70/4.10 and(and(X10,X11),and(X10,and(neg(and(neg(X10),X12)),X11))) = and(X10,X11)]. % 3.70/4.10 [4771=param(747,2632),[424,705], % 3.70/4.10 and(and(X10,X11),and(X10,and(X12,X11))) = and(X10,and(X12,X11))]. % 3.70/4.10 [4773=demod(3003),[4771], % 3.70/4.10 and(X10,and(neg(and(neg(X10),X11)),X12)) = and(X10,X12)]. % 3.70/4.10 [4929=param(4773,1016),[], % 3.70/4.10 and(X10,and(X11,neg(and(X12,neg(X10))))) = and(X10,X11)]. % 3.70/4.10 [5008=param(4929,609),[424], % 3.70/4.10 and(and(X10,X11),and(X12,X11)) = and(and(X10,X11),X12)]. % 3.70/4.10 [5169=param(5008,705),[], % 3.70/4.10 and(and(X10,X11),and(X11,X12)) = and(and(X10,X11),X12)]. % 3.70/4.10 [5190=demod(2541),[5169], % 3.70/4.10 neg(and(and(X10,X11),and(X10,X12))) = neg(and(X11,and(X10,X12)))]. % 3.70/4.10 [5307=param(909,5169),[5190], % 3.70/4.10 neg(and(and(X10,X11),X12)) = neg(and(X10,and(X11,X12)))]. % 3.70/4.10 [5684=param(424,5307),[424], % 3.70/4.10 and(and(X10,X11),X12) = and(X10,and(X11,X12))]. % 3.70/4.10 [6272=demod(843),[5684,5684], % 3.70/4.10 and(X10,and(X11,X12)) = and(X11,and(X10,X12))]. % 3.70/4.10 [6778=param(526,6272),[705,705,5], % 3.70/4.10 thmtrue = thmfalse]. % 3.70/4.10 % SZS output end CNFRefutation % 3.70/4.10 Space: 18930 KB %------------------------------------------------------------------------------