%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : BOO076-1 : TPTP v8.1.0. Released v2.6.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n019.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 : Thu Jul 14 23:38:54 EDT 2022 % Result : Unsatisfiable 52.45s 52.92s % Output : CNFRefutation 52.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : BOO076-1 : TPTP v8.1.0. Released v2.6.0. % 0.11/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 1 19:19:55 EDT 2022 % 0.12/0.33 % CPUTime : % 52.45/52.92 Theorem Proved. % 52.45/52.92 % SZS status Unsatisfiable % 52.45/52.92 % SZS output start CNFRefutation % 52.45/52.92 [1=axiom,[], % 52.45/52.92 nand(nand(X10,nand(nand(X11,X10),X10)),nand(X11,nand(X12,X10))) = X11]. % 52.45/52.92 [2=axiom,[], % 52.45/52.92 thtop(X10,X10) = thmfalse]. % 52.45/52.92 [3=axiom,[], % 52.45/52.92 thtop(nand(a,nand(b,nand(a,c))),nand(nand(nand(c,b),b),a)) = thmtrue]. % 52.45/52.92 [4=param(1,1),[], % 52.45/52.92 nand(nand(nand(X10,nand(X11,X12)),nand(nand(X13,nand(X10,nand(X11,X12))),nand(X10,nand(X11,X12)))),nand(X13,X10)) = X13]. % 52.45/52.92 [5=param(1,4),[], % 52.45/52.92 nand(nand(nand(X10,X11),nand(nand(X12,nand(X10,X11)),nand(X10,X11))),nand(X12,X10)) = X12]. % 52.45/52.92 [6=param(1,1),[], % 52.45/52.92 nand(nand(nand(X10,X11),nand(nand(nand(X11,nand(nand(X12,X11),X11)),nand(X10,X11)),nand(X10,X11))),X12) = nand(X11,nand(nand(X12,X11),X11))]. % 52.45/52.92 [7=param(5,1),[1,1], % 52.45/52.92 nand(nand(X10,nand(nand(X11,X10),X10)),nand(X11,nand(X12,nand(nand(X10,X12),X12)))) = X11]. % 52.45/52.92 [8=param(7,1),[], % 52.45/52.92 nand(nand(X10,nand(nand(nand(X11,nand(nand(X11,X11),X11)),X10),X10)),X11) = nand(X11,nand(nand(X11,X11),X11))]. % 52.45/52.92 [9=param(8,1),[], % 52.45/52.92 nand(nand(nand(X10,nand(X11,X10)),nand(X10,nand(X10,nand(X11,X10)))),X10) = nand(X10,nand(nand(X10,X10),X10))]. % 52.45/52.92 [10=param(9,7),[], % 52.45/52.92 nand(X10,nand(nand(X10,X10),X10)) = nand(X10,X10)]. % 52.45/52.92 [12=demod(8),[10,10], % 52.45/52.92 nand(nand(X10,nand(nand(nand(X11,X11),X10),X10)),X11) = nand(X11,X11)]. % 52.45/52.92 [13=param(10,1),[10,10,10,10], % 52.45/52.92 nand(nand(X10,X10),nand(X10,nand(X10,X10))) = nand(nand(X10,X10),nand(X10,X10))]. % 52.45/52.92 [14=param(1,10),[], % 52.45/52.92 nand(nand(X10,X10),nand(X10,nand(X11,X10))) = X10]. % 52.45/52.92 [15=demod(13),[14], % 52.45/52.92 nand(nand(X10,X10),nand(X10,X10)) = X10]. % 52.45/52.92 [20=param(1,15),[14], % 52.45/52.92 nand(X10,nand(nand(X10,X10),nand(X11,nand(X10,X10)))) = nand(X10,X10)]. % 52.45/52.92 [25=param(7,20),[], % 52.45/52.92 nand(nand(X10,nand(nand(X11,X10),X10)),nand(X11,X11)) = X11]. % 52.45/52.92 [26=param(1,25),[14], % 52.45/52.92 nand(X10,nand(nand(X11,nand(nand(X10,X11),X11)),nand(X12,nand(X10,X10)))) = nand(X11,nand(nand(X10,X11),X11))]. % 52.45/52.92 [27=param(1,25),[], % 52.45/52.92 nand(nand(X10,nand(nand(nand(X11,nand(nand(X10,X11),X11)),X10),X10)),X10) = nand(X11,nand(nand(X10,X11),X11))]. % 52.45/52.92 [29=param(7,25),[14], % 52.45/52.92 nand(X10,nand(nand(X11,nand(nand(X10,X11),X11)),nand(X12,nand(nand(nand(X10,X10),X12),X12)))) = nand(X11,nand(nand(X10,X11),X11))]. % 52.45/52.92 [33=param(6,12),[10,15], % 52.45/52.92 nand(X11,nand(nand(nand(nand(X10,X11),nand(X10,X11)),X11),X11)) = nand(X10,X11)]. % 52.45/52.92 [36=param(1,33),[10], % 52.45/52.92 nand(nand(X10,X10),nand(X11,X10)) = X10]. % 52.45/52.92 [40=param(5,33),[33,33], % 52.45/52.92 nand(nand(nand(X10,X11),nand(nand(X12,nand(X10,X11)),nand(X10,X11))),nand(X12,X11)) = X12]. % 52.45/52.92 [42=param(20,33),[], % 52.45/52.92 nand(X10,nand(X11,nand(X10,X10))) = nand(X10,X10)]. % 52.45/52.92 [48=param(36,6),[], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(nand(X10,X11),X11))) = X10]. % 52.45/52.92 [52=param(36,36),[], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),X11) = nand(X10,X11)]. % 52.45/52.92 [53=demod(33),[52], % 52.45/52.92 nand(X10,nand(nand(X11,X10),X10)) = nand(X11,X10)]. % 52.45/52.92 [54=demod(40),[53], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),nand(X10,X12)) = X10]. % 52.45/52.92 [55=demod(5),[53], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),nand(X10,X11)) = X10]. % 52.45/52.92 [56=demod(25),[53], % 52.45/52.92 nand(nand(X10,X11),nand(X10,X10)) = X10]. % 52.45/52.92 [57=demod(1),[53], % 52.45/52.92 nand(nand(X10,X11),nand(X10,nand(X12,X11))) = X10]. % 52.45/52.92 [59=demod(12),[53], % 52.45/52.92 nand(nand(nand(X10,X10),X11),X10) = nand(X10,X10)]. % 52.45/52.92 [62=demod(48),[53], % 52.45/52.92 nand(nand(X10,X10),nand(X10,X11)) = X10]. % 52.45/52.92 [65=demod(27),[53,53,53], % 52.45/52.92 nand(nand(nand(X10,X11),X10),X10) = nand(X10,X11)]. % 52.45/52.92 [66=demod(26),[53,53], % 52.45/52.92 nand(X10,nand(nand(X10,X11),nand(X12,nand(X10,X10)))) = nand(X10,X11)]. % 52.45/52.92 [69=demod(7),[53,53], % 52.45/52.92 nand(nand(X10,X11),nand(X10,nand(X11,X12))) = X10]. % 52.45/52.92 [70=demod(29),[53,53,53], % 52.45/52.92 nand(X10,nand(nand(X10,X11),nand(nand(X10,X10),X12))) = nand(X10,X11)]. % 52.45/52.92 [73=param(62,36),[], % 52.45/52.92 nand(X10,nand(nand(X10,X10),X11)) = nand(X10,X10)]. % 52.45/52.92 [82=param(53,36),[36], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(X10,X11))) = X11]. % 52.45/52.92 [84=param(56,53),[], % 52.45/52.92 nand(nand(X10,X11),nand(X11,X11)) = X11]. % 52.45/52.92 [85=param(59,53),[], % 52.45/52.92 nand(nand(X10,nand(X11,X11)),X11) = nand(X11,X11)]. % 52.45/52.92 [86=param(53,65),[], % 52.45/52.92 nand(nand(X10,X11),X10) = nand(X10,nand(X10,X11))]. % 52.45/52.92 [88=demod(65),[86,86], % 52.45/52.92 nand(X10,nand(X10,nand(X10,X11))) = nand(X10,X11)]. % 52.45/52.92 [89=param(86,53),[53], % 52.45/52.92 nand(nand(X10,X11),X11) = nand(X11,nand(X10,X11))]. % 52.45/52.92 [90=demod(53),[89], % 52.45/52.92 nand(X10,nand(X10,nand(X11,X10))) = nand(X11,X10)]. % 52.45/52.92 [105=param(54,85),[], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),nand(nand(X12,nand(nand(X10,X11),nand(X10,X11))),X11)) = nand(X12,nand(nand(X10,X11),nand(X10,X11)))]. % 52.45/52.92 [125=param(69,54),[], % 52.45/52.92 nand(X10,nand(nand(X10,nand(X11,X12)),nand(nand(X10,X12),X13))) = nand(X10,nand(X11,X12))]. % 52.45/52.92 [130=param(69,59),[], % 52.45/52.92 nand(nand(X10,X10),nand(nand(nand(X10,X10),X11),nand(X10,X12))) = nand(nand(X10,X10),X11)]. % 52.45/52.92 [132=param(69,69),[], % 52.45/52.92 nand(X10,nand(nand(X10,X11),nand(nand(X10,nand(X11,X12)),X13))) = nand(X10,X11)]. % 52.45/52.92 [134=param(69,84),[], % 52.45/52.92 nand(X10,nand(nand(X11,X10),nand(nand(X10,X10),X12))) = nand(X11,X10)]. % 52.45/52.92 [144=param(57,54),[], % 52.45/52.92 nand(nand(nand(X10,nand(X11,X12)),X12),X10) = nand(X10,nand(X11,X12))]. % 52.45/52.92 [147=param(57,55),[], % 52.45/52.92 nand(X10,nand(nand(X10,nand(X11,X12)),nand(X13,nand(X10,X11)))) = nand(X10,nand(X11,X12))]. % 52.45/52.92 [148=param(57,55),[], % 52.45/52.92 nand(nand(nand(X10,nand(X11,X12)),X11),X10) = nand(X10,nand(X11,X12))]. % 52.45/52.92 [153=param(57,69),[], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X11,X12)),X10) = nand(X10,X11)]. % 52.45/52.92 [156=param(57,84),[], % 52.45/52.92 nand(X10,nand(nand(X11,X10),nand(X12,nand(X10,X10)))) = nand(X11,X10)]. % 52.45/52.92 [173=param(153,82),[], % 52.45/52.92 nand(X10,X11) = nand(X11,X10)]. % 52.45/52.92 [182=demod(148),[173,173], % 52.45/52.92 nand(X10,nand(X11,nand(X10,nand(X11,X12)))) = nand(X10,nand(X11,X12))]. % 52.45/52.92 [184=demod(105),[173], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),nand(X11,nand(X12,nand(nand(X10,X11),nand(X10,X11))))) = nand(X12,nand(nand(X10,X11),nand(X10,X11)))]. % 52.45/52.92 [185=demod(144),[173,173], % 52.45/52.92 nand(X10,nand(X11,nand(X10,nand(X12,X11)))) = nand(X10,nand(X12,X11))]. % 52.45/52.92 [187=param(57,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(X12,X10))) = X11]. % 52.45/52.92 [188=param(57,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,X11),X10)) = X10]. % 52.45/52.92 [189=param(69,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(X10,X12))) = X11]. % 52.45/52.92 [190=param(69,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X11,X12),X10)) = X10]. % 52.45/52.92 [194=param(190,84),[], % 52.45/52.92 nand(X10,nand(nand(nand(X10,X10),X11),nand(X12,X10))) = nand(X12,X10)]. % 52.45/52.92 [197=param(190,173),[], % 52.45/52.92 nand(nand(nand(X11,X12),X10),nand(X10,X11)) = X10]. % 52.45/52.92 [198=param(190,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X10,X12),X11)) = X11]. % 52.45/52.92 [199=param(198,42),[], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X10,X11),nand(X12,nand(X10,X10)))) = nand(X12,nand(X10,X10))]. % 52.45/52.92 [200=param(198,57),[], % 52.45/52.92 nand(X10,nand(nand(nand(X10,X11),X12),nand(X10,nand(X13,X11)))) = nand(X10,nand(X13,X11))]. % 52.45/52.92 [203=param(69,198),[], % 52.45/52.92 nand(X10,nand(nand(X11,X10),nand(nand(nand(X11,X12),X10),X13))) = nand(X11,X10)]. % 52.45/52.92 [204=param(69,198),[173], % 52.45/52.92 nand(X10,nand(nand(X11,X10),nand(X11,X12))) = nand(X11,X10)]. % 52.45/52.92 [205=param(198,73),[], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X10,X11),nand(nand(X10,X10),X12))) = nand(nand(X10,X10),X12)]. % 52.45/52.92 [206=param(198,84),[173], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,X10),X11)) = X11]. % 52.45/52.92 [210=param(190,198),[173,173], % 52.45/52.92 nand(X10,nand(X11,nand(nand(X11,X12),X10))) = nand(nand(X11,X12),X10)]. % 52.45/52.92 [232=param(190,206),[173,173], % 52.45/52.92 nand(X10,nand(X11,nand(nand(X12,X11),X10))) = nand(nand(X12,X11),X10)]. % 52.45/52.92 [245=param(189,84),[], % 52.45/52.92 nand(nand(nand(X10,X11),X12),nand(X12,X11)) = X12]. % 52.45/52.92 [246=param(189,173),[], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),nand(X11,X10)) = X10]. % 52.45/52.92 [249=param(189,198),[173], % 52.45/52.92 nand(X10,nand(nand(X11,X12),nand(X11,X10))) = nand(X11,X10)]. % 52.45/52.92 [252=param(189,206),[173], % 52.45/52.92 nand(X10,nand(nand(X11,X12),nand(X12,X10))) = nand(X12,X10)]. % 52.45/52.92 [258=param(69,70),[], % 52.45/52.92 nand(nand(X10,X11),nand(X10,nand(nand(nand(X10,X11),nand(nand(X10,X10),X12)),X13))) = X10]. % 52.45/52.92 [264=param(69,245),[], % 52.45/52.92 nand(X10,nand(nand(nand(X11,X12),X10),nand(nand(X10,X12),X13))) = nand(nand(X11,X12),X10)]. % 52.45/52.92 [274=param(125,246),[173], % 52.45/52.92 nand(X10,nand(X11,nand(X10,X11))) = nand(X10,X10)]. % 52.45/52.92 [282=param(206,274),[], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X11,X10),nand(X12,nand(X10,X12)))) = nand(X12,nand(X10,X12))]. % 52.45/52.92 [322=param(252,125),[125], % 52.45/52.92 nand(nand(nand(X10,nand(X11,X12)),nand(nand(X10,X12),X13)),nand(nand(X14,X10),nand(X10,nand(X11,X12)))) = nand(X10,nand(X11,X12))]. % 52.45/52.92 [356=param(187,249),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(nand(X10,X12),nand(X10,X11)),nand(X13,X11))) = nand(nand(X10,X12),nand(X10,X11))]. % 52.45/52.92 [363=param(249,197),[173,197], % 52.45/52.92 nand(nand(X10,X11),nand(X10,nand(nand(nand(X11,X12),X10),X13))) = X10]. % 52.45/52.92 [367=param(206,249),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,X11),nand(nand(X10,X13),nand(X10,X11)))) = nand(nand(X10,X13),nand(X10,X11))]. % 52.45/52.92 [374=param(252,249),[249], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X12)),nand(nand(X13,X12),nand(X10,X12))) = nand(X10,X12)]. % 52.45/52.92 [406=param(57,204),[], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(X12,nand(nand(X10,X11),nand(X10,X13))))) = X11]. % 52.45/52.92 [480=param(232,173),[210], % 52.45/52.92 nand(nand(X10,X11),X12) = nand(nand(X11,X10),X12)]. % 52.45/52.92 [485=param(232,198),[173], % 52.45/52.92 nand(X10,nand(X11,nand(X11,X10))) = nand(X10,X10)]. % 52.45/52.92 [508=param(190,485),[173], % 52.45/52.92 nand(nand(X10,nand(X11,nand(X11,nand(X10,X12)))),nand(nand(X10,X12),nand(X10,X12))) = nand(X11,nand(X11,nand(X10,X12)))]. % 52.45/52.92 [542=param(90,480),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X11,X10),nand(X12,nand(X10,X11)))) = nand(X12,nand(X10,X11))]. % 52.45/52.92 [549=param(480,173),[], % 52.45/52.92 nand(nand(X10,X11),X12) = nand(X12,nand(X11,X10))]. % 52.45/52.92 [557=param(480,204),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,nand(X11,X10)),nand(X12,X13))) = nand(X12,nand(X11,X10))]. % 52.45/52.92 [565=param(480,249),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,X13),nand(X12,nand(X11,X10)))) = nand(X12,nand(X11,X10))]. % 52.45/52.92 [573=param(485,480),[], % 52.45/52.92 nand(X10,nand(nand(X11,X12),nand(nand(X12,X11),X10))) = nand(X10,X10)]. % 52.45/52.92 [586=param(549,173),[], % 52.45/52.92 nand(X10,nand(X11,X12)) = nand(X10,nand(X12,X11))]. % 52.45/52.92 [599=param(549,549),[], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),X13) = nand(X13,nand(X10,nand(X12,X11)))]. % 52.45/52.92 [602=param(232,549),[], % 52.45/52.92 nand(nand(X10,X11),nand(X12,nand(nand(X11,X10),nand(X13,X12)))) = nand(nand(X13,X12),nand(X10,X11))]. % 52.45/52.92 [604=param(549,480),[], % 52.45/52.92 nand(nand(X10,X11),nand(X12,X13)) = nand(nand(X13,X12),nand(X11,X10))]. % 52.45/52.92 [605=param(549,480),[], % 52.45/52.92 nand(X10,nand(nand(X11,X12),X13)) = nand(nand(X13,nand(X12,X11)),X10)]. % 52.45/52.92 [630=param(210,134),[-602,573], % 52.45/52.92 nand(nand(X10,X10),nand(X11,X11)) = nand(nand(X10,X10),nand(nand(X10,X10),X11))]. % 52.45/52.92 [680=param(185,130),[-599], % 52.45/52.92 nand(nand(nand(X10,X10),X11),nand(nand(X10,X10),X11)) = nand(nand(X10,nand(X10,X10)),nand(nand(X10,X10),X11))]. % 52.45/52.92 [695=param(185,480),[], % 52.45/52.92 nand(nand(X11,X10),nand(X13,nand(nand(X10,X11),nand(X12,X13)))) = nand(nand(X10,X11),nand(X12,X13))]. % 52.45/52.92 [698=param(185,485),[], % 52.45/52.92 nand(X10,nand(X11,X11)) = nand(X10,nand(X10,X11))]. % 52.45/52.92 [699=param(698,36),[], % 52.45/52.92 nand(X10,nand(X10,nand(X11,X11))) = nand(X10,X11)]. % 52.45/52.92 [706=param(698,173),[], % 52.45/52.92 nand(X10,nand(X10,X11)) = nand(nand(X11,X11),X10)]. % 52.45/52.92 [725=param(698,480),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X10,X11),X12)) = nand(nand(X11,X10),nand(X12,X12))]. % 52.45/52.92 [733=param(36,698),[-706,-605,188,-605], % 52.45/52.92 nand(X10,nand(nand(X11,X11),X10)) = nand(X10,X11)]. % 52.45/52.92 [755=param(698,549),[173], % 52.45/52.92 nand(X10,nand(X11,X11)) = nand(X10,nand(X11,X10))]. % 52.45/52.92 [757=param(586,698),[173], % 52.45/52.92 nand(X10,nand(X11,nand(X12,X12))) = nand(X10,nand(X11,nand(X11,X12)))]. % 52.45/52.92 [809=param(733,549),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X11,X10),nand(X12,X12))) = nand(nand(X10,X11),X12)]. % 52.45/52.92 [838=param(755,173),[], % 52.45/52.92 nand(X10,nand(X11,X10)) = nand(nand(X11,X11),X10)]. % 52.45/52.92 [859=param(480,755),[], % 52.45/52.92 nand(nand(X10,nand(X11,X10)),X12) = nand(nand(nand(X11,X11),X10),X12)]. % 52.45/52.92 [863=param(549,755),[], % 52.45/52.92 nand(X10,nand(X11,nand(X12,X11))) = nand(nand(nand(X12,X12),X11),X10)]. % 52.45/52.92 [867=param(755,56),[-706], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X10,X11),nand(X10,X11))) = nand(X10,nand(X10,X10))]. % 52.45/52.92 [870=param(755,66),[-602,573,-602,199,565], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,nand(X10,X10)),nand(X12,nand(X10,X10)))) = nand(X12,nand(X10,X10))]. % 52.45/52.92 [872=param(755,70),[-602,573,680,-602,205,680,205], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X10,nand(X10,X10)),nand(nand(X10,X10),X12))) = nand(nand(X10,X10),X12)]. % 52.45/52.92 [873=param(755,84),[-706], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X11,X10),nand(X11,X10))) = nand(X10,nand(X10,X10))]. % 52.45/52.92 [916=param(586,755),[173], % 52.45/52.92 nand(X10,nand(X11,nand(X12,X12))) = nand(X10,nand(X11,nand(X12,X11)))]. % 52.45/52.92 [917=param(755,698),[], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(X11,X10))) = nand(nand(X10,X10),nand(X11,X11))]. % 52.45/52.92 [919=param(838,69),[173], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),nand(X10,nand(X11,X12))) = nand(X10,nand(X10,nand(X11,X12)))]. % 52.45/52.92 [953=param(838,66),[36,36,194,-602,542], % 52.45/52.92 nand(nand(X10,X11),nand(nand(nand(X11,X11),X12),nand(X10,X11))) = nand(nand(X11,X11),X12)]. % 52.45/52.92 [974=param(706,66),[36,36,-605,70,-602,953], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X11,X10),nand(nand(X10,X10),X12))) = nand(nand(X10,X10),X12)]. % 52.45/52.92 [1025=param(917,88),[-602,542,-602,867,199], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X10,X11),nand(X10,X11))) = nand(X10,nand(X10,X10))]. % 52.45/52.92 [1027=param(917,90),[-602,542,1025,-602,873,282], % 52.45/52.92 nand(X10,nand(X10,X10)) = nand(X11,nand(X11,X11))]. % 52.45/52.92 [1066=param(36,1027),[36], % 52.45/52.92 nand(X10,nand(X11,nand(X11,X11))) = nand(X10,X10)]. % 52.45/52.92 [1068=param(57,1027),[], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(X11,X11))) = X10]. % 52.45/52.92 [1116=param(206,1068),[], % 52.45/52.92 nand(nand(nand(X10,nand(X10,X10)),X11),nand(X12,X11)) = X11]. % 52.45/52.92 [1142=param(156,698),[], % 52.45/52.92 nand(X10,nand(nand(X11,X10),nand(X12,nand(X12,X10)))) = nand(X11,X10)]. % 52.45/52.92 [1203=param(733,1066),[], % 52.45/52.92 nand(X10,nand(nand(X11,nand(X12,nand(X12,X12))),X10)) = nand(X10,X11)]. % 52.45/52.92 [1204=param(755,1066),[], % 52.45/52.92 nand(X10,nand(X11,nand(X12,nand(X12,X12)))) = nand(X10,nand(X11,X10))]. % 52.45/52.92 [1318=param(90,1203),[], % 52.45/52.92 nand(X10,nand(X10,X11)) = nand(nand(X11,nand(X12,nand(X12,X12))),X10)]. % 52.45/52.92 [1450=param(733,184),[-599,-755,-602,695,-602,249,406], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(nand(X12,X10),nand(X12,X10)))) = X10]. % 52.45/52.92 [1561=param(1142,62),[62], % 52.45/52.92 nand(nand(X10,X11),nand(X10,nand(X12,nand(X12,nand(X10,X11))))) = X10]. % 52.45/52.92 [1964=param(1561,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(X12,nand(X12,nand(X11,X10))))) = X11]. % 52.45/52.92 [1993=param(755,1561),[173,508], % 52.45/52.92 nand(X10,nand(X10,nand(X11,nand(X11,nand(X10,X12))))) = nand(X11,nand(X11,nand(X10,X12)))]. % 52.45/52.92 [2151=param(57,203),[-602,363,173], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(nand(nand(X10,X12),X11),X13))) = X11]. % 52.45/52.92 [2186=param(200,2151),[173,173], % 52.45/52.92 nand(X10,nand(X11,nand(X10,nand(nand(X10,X11),X12)))) = nand(X10,X10)]. % 52.45/52.92 [2228=param(182,2186),[], % 52.45/52.92 nand(X10,nand(X11,nand(nand(X11,X10),X12))) = nand(X10,nand(X11,X11))]. % 52.45/52.92 [2238=param(2228,56),[867], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X10,X11),nand(X10,X12))) = nand(X10,nand(X10,X10))]. % 52.45/52.92 [2259=param(2228,173),[], % 52.45/52.92 nand(X10,nand(X11,nand(nand(X10,X11),X12))) = nand(X10,nand(X11,X11))]. % 52.45/52.92 [2299=param(2228,549),[], % 52.45/52.92 nand(X10,nand(X11,nand(X12,nand(X10,X11)))) = nand(X10,nand(X11,X11))]. % 52.45/52.92 [2475=param(2259,189),[-725,69,173], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X11,nand(X10,X12)),nand(X11,X13))) = nand(X11,nand(X11,X10))]. % 52.45/52.92 [3837=param(90,1964),[173,1993,173,-755,1964], % 52.45/52.92 nand(nand(X10,nand(X10,nand(X11,X12))),nand(X11,X11)) = X11]. % 52.45/52.92 [3869=param(3837,90),[], % 52.45/52.92 nand(nand(X10,nand(X10,nand(X11,X12))),nand(X12,X12)) = X12]. % 52.45/52.92 [3871=param(3837,173),[], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(X11,nand(X10,X12)))) = X10]. % 52.45/52.92 [3872=param(3837,173),[-602,695], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(nand(X10,X12),X11))) = X10]. % 52.45/52.92 [3891=param(3837,232),[-602,695], % 52.45/52.92 nand(nand(X10,X10),nand(X11,nand(nand(X12,X10),X11))) = X10]. % 52.45/52.92 [3902=param(3837,838),[36,173], % 52.45/52.92 nand(X10,nand(X11,nand(X11,nand(X12,nand(X10,X12))))) = nand(X10,X10)]. % 52.45/52.92 [4154=param(187,3872),[604], % 52.45/52.92 nand(nand(X10,X11),nand(X11,nand(X12,nand(nand(X10,X13),X12)))) = X11]. % 52.45/52.92 [4211=param(57,3871),[173], % 52.45/52.92 nand(nand(X10,X11),nand(X10,nand(X12,nand(X12,nand(X11,X13))))) = X10]. % 52.45/52.92 [4737=param(3902,190),[173,173,-755], % 52.45/52.92 nand(X10,nand(nand(X10,nand(X11,X12)),nand(X11,X11))) = nand(X10,X10)]. % 52.45/52.92 [4827=param(4737,480),[-602,695], % 52.45/52.92 nand(X10,nand(nand(X11,X11),nand(nand(X11,X12),X10))) = nand(X10,X10)]. % 52.45/52.92 [4852=param(4827,56),[], % 52.45/52.92 nand(X10,nand(nand(nand(X11,X12),nand(X11,X12)),nand(X11,X10))) = nand(X10,X10)]. % 52.45/52.92 [4856=param(4827,90),[], % 52.45/52.92 nand(X10,nand(nand(X11,X11),nand(nand(X12,X11),X10))) = nand(X10,X10)]. % 52.45/52.92 [4892=param(4827,838),[36], % 52.45/52.92 nand(X10,nand(X11,nand(nand(X12,nand(X11,X12)),X10))) = nand(X10,X10)]. % 52.45/52.92 [4902=param(2299,4827),[84,630], % 52.45/52.92 nand(nand(X10,X10),nand(nand(X10,X10),nand(nand(X10,X12),X11))) = nand(nand(X10,X10),X11)]. % 52.45/52.92 [5016=param(2299,4892),[84,698], % 52.45/52.92 nand(X10,nand(X10,nand(nand(X12,nand(X10,X12)),X11))) = nand(X10,X11)]. % 52.45/52.92 [5047=param(88,5016),[], % 52.45/52.92 nand(X10,nand(nand(X12,nand(X10,X12)),X11)) = nand(X10,nand(X10,X11))]. % 52.45/52.92 [5148=param(5047,66),[-602,573,870], % 52.45/52.92 nand(X10,nand(nand(X11,nand(X10,X10)),X12)) = nand(X10,nand(X10,X12))]. % 52.45/52.92 [5157=param(5047,70),[-602,573,680,872], % 52.45/52.92 nand(X10,nand(nand(nand(X10,X10),X11),X12)) = nand(X10,nand(X10,X12))]. % 52.45/52.92 [5182=param(5047,173),[], % 52.45/52.92 nand(X10,nand(nand(X11,nand(X11,X10)),X12)) = nand(X10,nand(X10,X12))]. % 52.45/52.92 [5353=param(5182,755),[5182,699], % 52.45/52.92 nand(X10,nand(X10,nand(X11,nand(X12,nand(X12,X10))))) = nand(X10,X11)]. % 52.45/52.92 [5364=param(5182,2238),[187], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X12)),nand(nand(nand(X10,X11),nand(X10,X12)),X13)) = nand(nand(nand(X10,X11),nand(X10,X12)),nand(X10,X13))]. % 52.45/52.92 [5903=param(36,5353),[-602,2475,-599,557], % 52.45/52.92 nand(X10,nand(X11,nand(X12,nand(X12,X10)))) = nand(X10,nand(X11,X10))]. % 52.45/52.92 [5967=param(5903,549),[], % 52.45/52.92 nand(nand(X10,X11),nand(X12,nand(X13,nand(nand(X11,X10),X13)))) = nand(nand(X10,X11),nand(X12,nand(X10,X11)))]. % 52.45/52.92 [6753=param(755,258),[173,-602,4852,630,4902], % 52.45/52.92 nand(X10,nand(X10,nand(nand(nand(X10,X11),nand(nand(X10,X10),X12)),X13))) = nand(nand(nand(X10,X11),nand(X10,X11)),X13)]. % 52.45/52.92 [7258=param(4211,5182),[88], % 52.45/52.92 nand(nand(X10,nand(X11,nand(X11,X12))),nand(X10,nand(X12,X13))) = X10]. % 52.45/52.92 [7388=param(7258,549),[], % 52.45/52.92 nand(nand(nand(X11,X12),X10),nand(X10,nand(X13,nand(X13,X11)))) = X10]. % 52.45/52.92 [7610=param(7388,838),[699], % 52.45/52.92 nand(nand(nand(X10,nand(X11,X10)),X12),nand(X12,nand(X13,X11))) = X12]. % 52.45/52.92 [7713=param(7610,173),[], % 52.45/52.92 nand(nand(X10,nand(X11,nand(X12,X11))),nand(X10,nand(X13,X12))) = X10]. % 52.45/52.92 [7810=param(7610,755),[733], % 52.45/52.92 nand(nand(nand(X10,X11),X12),nand(X12,nand(X13,nand(X11,X13)))) = X12]. % 52.45/52.92 [8065=param(7810,838),[], % 52.45/52.92 nand(nand(nand(X10,X11),X12),nand(X12,nand(nand(X11,X11),X13))) = X12]. % 52.45/52.92 [8176=param(8065,549),[], % 52.45/52.92 nand(nand(nand(nand(X11,X11),X12),X10),nand(nand(X13,X11),X10)) = X10]. % 52.45/52.92 [8279=param(755,264),[-602,573,-602,4856,630,4902], % 52.45/52.92 nand(nand(nand(X10,X11),X12),nand(nand(nand(X12,X11),X13),nand(nand(X12,X11),X13))) = nand(nand(X12,X12),X13)]. % 52.45/52.92 [8372=param(8176,755),[36], % 52.45/52.92 nand(nand(nand(X10,X11),X12),nand(nand(X13,nand(X10,X13)),X12)) = X12]. % 52.45/52.92 [8546=param(8372,549),[], % 52.45/52.92 nand(nand(X10,nand(X11,nand(X12,X11))),nand(nand(X12,X13),X10)) = X10]. % 52.45/52.92 [8682=param(8546,84),[604], % 52.45/52.92 nand(nand(X10,X11),nand(nand(X12,nand(nand(X13,X11),X12)),X10)) = X10]. % 52.45/52.92 [16637=param(4154,3871),[], % 52.45/52.92 nand(X10,nand(nand(X11,nand(X11,nand(X10,X12))),nand(X13,nand(nand(nand(X10,X10),X14),X13)))) = nand(X11,nand(X11,nand(X10,X12)))]. % 52.45/52.92 [16638=param(4154,3872),[], % 52.45/52.92 nand(X10,nand(nand(X11,nand(nand(X10,X12),X11)),nand(X13,nand(nand(nand(X10,X10),X14),X13)))) = nand(X11,nand(nand(X10,X12),X11))]. % 52.45/52.92 [18523=param(7713,322),[-602,5967,-602,485,8279,5047,974], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),nand(nand(X10,X10),X13)) = nand(nand(X10,nand(X11,X12)),nand(nand(X10,X12),X13))]. % 52.45/52.92 [18550=param(5148,1450),[18523,173], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),nand(nand(X11,nand(X10,X11)),X12)) = nand(nand(nand(X10,X11),nand(X10,X11)),nand(X11,X12))]. % 52.45/52.92 [19695=param(809,549),[], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),nand(nand(X10,nand(X12,X11)),nand(X13,X13))) = nand(nand(X10,nand(X11,X12)),X13)]. % 52.45/52.92 [22809=param(549,1318),[], % 52.45/52.92 nand(X10,nand(X11,nand(X11,X12))) = nand(nand(X11,nand(X12,nand(X13,nand(X13,X13)))),X10)]. % 52.45/52.92 [23280=param(1204,187),[173], % 52.45/52.92 nand(nand(X10,nand(X11,X12)),nand(nand(X12,X10),nand(X13,nand(X13,X13)))) = nand(X10,nand(X10,nand(X11,X12)))]. % 52.45/52.92 [24161=param(356,173),[], % 52.45/52.92 nand(nand(X10,X11),nand(nand(nand(X11,X12),nand(X11,X10)),nand(X13,X10))) = nand(nand(X11,X12),nand(X11,X10))]. % 52.45/52.92 [24175=param(573,356),[-602,24161,367,5364], % 52.45/52.92 nand(X10,nand(nand(nand(X11,X12),nand(X11,X13)),nand(X11,X10))) = nand(X10,X10)]. % 52.45/52.92 [26734=param(916,549),[], % 52.45/52.92 nand(nand(X10,X11),nand(X12,nand(X13,X13))) = nand(nand(X12,nand(X13,X12)),nand(X11,X10))]. % 52.45/52.92 [28709=param(863,3891),[-605,173,36], % 52.45/52.92 nand(X10,nand(X11,nand(X12,nand(X12,nand(X13,X11))))) = nand(nand(X11,nand(X12,nand(nand(X13,X11),X12))),X10)]. % 52.45/52.92 [28998=param(5148,374),[18523,173,18550], % 52.45/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),nand(nand(X12,nand(X10,X11)),X13)) = nand(nand(nand(X10,X11),nand(X10,X11)),nand(X11,X13))]. % 52.56/52.92 [29003=param(5157,374),[18523,173,28998], % 52.56/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),nand(nand(nand(X10,X11),X12),X13)) = nand(nand(nand(X10,X11),nand(X10,X11)),nand(X11,X13))]. % 52.56/52.92 [29501=param(859,480),[], % 52.56/52.92 nand(nand(X10,nand(nand(X11,X12),X10)),X13) = nand(nand(nand(nand(X12,X11),nand(X12,X11)),X10),X13)]. % 52.56/52.92 [30469=param(755,757),[], % 52.56/52.92 nand(nand(X10,nand(X10,X11)),nand(X12,nand(X10,nand(X11,X11)))) = nand(nand(X10,nand(X10,X11)),nand(X12,X12))]. % 52.56/52.92 [32388=param(5182,204),[5364], % 52.56/52.92 nand(nand(nand(X10,X11),nand(X10,X12)),nand(nand(X11,nand(X10,X11)),X13)) = nand(nand(nand(X10,X11),nand(X10,X12)),nand(X10,X13))]. % 52.56/52.92 [32559=param(3869,132),[-30469,26734], % 52.56/52.92 nand(nand(X10,nand(X10,X11)),nand(nand(X10,nand(X11,X10)),nand(X12,nand(X10,nand(X11,X13))))) = nand(nand(X10,nand(X11,X13)),X12)]. % 52.56/52.92 [33348=param(8682,1116),[-22809], % 52.56/52.92 nand(nand(X10,nand(X11,nand(X11,nand(X12,X10)))),nand(nand(X12,X10),nand(X13,nand(X13,X13)))) = nand(X11,nand(nand(X12,X10),nand(X13,nand(X13,X13))))]. % 52.56/52.92 [33706=param(755,258),[173,-602,24175,630,29003,18523,173,32388,919], % 52.56/52.92 nand(X10,nand(X10,nand(nand(nand(X10,X11),nand(nand(X10,X10),X12)),X13))) = nand(X10,nand(X10,nand(X11,X13)))]. % 52.56/52.92 [33707=demod(6753),[33706], % 52.56/52.92 nand(nand(nand(X10,X11),nand(X10,X11)),X12) = nand(X10,nand(X10,nand(X11,X12)))]. % 52.56/52.92 [34336=demod(29501),[33707], % 52.56/52.92 nand(nand(X10,nand(nand(X11,X12),X10)),X13) = nand(nand(X12,nand(X12,nand(X11,X10))),X13)]. % 52.56/52.92 [34366=demod(16638),[34336,16637], % 52.56/52.92 nand(X12,nand(nand(X11,X10),X12)) = nand(X10,nand(X10,nand(X11,X12)))]. % 52.56/52.92 [34470=demod(23280),[], % 52.56/52.92 nand(nand(X10,nand(X11,X12)),nand(nand(X12,X10),nand(X13,nand(X13,X13)))) = nand(X10,nand(X10,nand(X11,X12)))]. % 52.56/52.92 [34477=demod(33348),[], % 52.56/52.92 nand(nand(X10,nand(X11,nand(X11,nand(X12,X10)))),nand(nand(X12,X10),nand(X13,nand(X13,X13)))) = nand(X11,nand(nand(X12,X10),nand(X13,nand(X13,X13))))]. % 52.56/52.92 [35707=demod(34470),[], % 52.56/52.92 nand(nand(X10,nand(X11,X12)),nand(nand(X12,X10),nand(X13,nand(X13,X13)))) = nand(X10,nand(X10,nand(X11,X12)))]. % 52.56/52.92 [35712=demod(34477),[], % 52.56/52.92 nand(nand(X10,nand(X11,nand(X11,nand(X12,X10)))),nand(nand(X12,X10),nand(X13,nand(X13,X13)))) = nand(X11,nand(nand(X12,X10),nand(X13,nand(X13,X13))))]. % 52.56/52.92 [36676=demod(28709),[34366,88], % 52.56/52.92 nand(X10,nand(X11,nand(X12,nand(X12,nand(X13,X11))))) = nand(nand(X11,nand(X13,X12)),X10)]. % 52.56/52.92 [37853=param(198,198),[-36676,173], % 52.56/52.92 nand(X10,nand(X11,nand(X10,nand(X10,nand(X11,nand(X11,X12)))))) = nand(nand(X11,X12),X10)]. % 52.56/52.92 [37912=param(3,549),[173,-37853,-32559,173,-755,-755,-37853,485,1066,-605,-706,173,-755], % 52.56/52.92 thtop(nand(nand(b,nand(c,c)),nand(nand(b,nand(c,c)),nand(a,nand(b,nand(c,nand(b,nand(b,nand(c,nand(c,a))))))))),nand(a,nand(b,nand(c,c)))) = thmtrue]. % 52.56/52.92 [37913=param(88,549),[34366], % 52.56/52.92 nand(X10,nand(X11,nand(X11,nand(X12,X10)))) = nand(X10,nand(X11,X12))]. % 52.56/52.92 [37918=demod(35712),[37913,35707], % 52.56/52.92 nand(X10,nand(X10,nand(X11,X12))) = nand(X11,nand(nand(X12,X10),nand(X13,nand(X13,X13))))]. % 52.56/52.92 [37957=param(147,1066),[-37918,-36676,37913,37913], % 52.56/52.92 nand(X10,nand(X11,nand(X11,nand(X10,X12)))) = nand(X10,nand(X11,X12))]. % 52.56/52.92 [38499=param(37957,755),[37957], % 52.56/52.92 nand(X10,nand(X11,nand(X12,X10))) = nand(X10,nand(X11,nand(X12,X12)))]. % 52.56/52.92 [38628=param(37912,37957),[182,38499,-755,19695,-605,-706,173,-755,2], % 52.56/52.92 thmtrue = thmfalse]. % 52.56/52.92 % SZS output end CNFRefutation % 52.56/52.92 Space: 85748 KB %------------------------------------------------------------------------------