%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LCL038-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n008.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 10:33:03 EDT 2022 % Result : Unsatisfiable 40.97s 41.38s % Output : CNFRefutation 41.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LCL038-10 : TPTP v8.1.0. Released v7.5.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jul 3 09:06:38 EDT 2022 % 0.12/0.34 % CPUTime : % 40.97/41.38 Theorem Proved. % 40.97/41.38 % SZS status Unsatisfiable % 40.97/41.38 % SZS output start CNFRefutation % 40.97/41.38 [1=axiom,[], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(X12,X10),implies(X13,X10)))) = true]. % 40.97/41.38 [2=axiom,[], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,X11)),true,ifeq(is_a_theorem(X10),true,is_a_theorem(X11),true),true) = true]. % 40.97/41.38 [3=axiom,[], % 40.97/41.38 ifeq(X10,X10,X11,X12) = X11]. % 40.97/41.38 [4=axiom,[], % 40.97/41.38 thtop(X10,X10) = thmfalse]. % 40.97/41.38 [5=axiom,[], % 40.97/41.38 thtop(is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),true) = thmtrue]. % 40.97/41.38 [6=param(2,1),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,X11),X12)),true,is_a_theorem(implies(implies(X12,X10),implies(X13,X10))),true) = true]. % 40.97/41.38 [8=param(6,1),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X12,X11)),implies(X11,X13)),implies(X14,implies(X11,X13)))) = true]. % 40.97/41.38 [10=param(2,1),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(X10,X11),X12),implies(implies(X12,X10),implies(X13,X10))),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [11=param(2,8),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,X11),implies(X12,X11)),implies(X11,X13))),true,is_a_theorem(implies(X14,implies(X11,X13))),true) = true]. % 40.97/41.38 [12=param(11,8),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(X11,X12),implies(X12,implies(X11,X12))))) = true]. % 40.97/41.38 [15=param(6,12),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X11,implies(X10,X11))),X12),implies(X13,X12))) = true]. % 40.97/41.38 [23=param(10,15),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(X11,implies(X12,X11)),X12),implies(X13,X12)))) = true]. % 40.97/41.38 [30=param(6,23),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(X10,implies(X11,X10)),X11),implies(X12,X11)),X13),implies(X14,X13))) = true]. % 40.97/41.38 [72=param(11,30),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(X11,X12),implies(X13,implies(X11,X12))))) = true]. % 40.97/41.38 [93=param(10,72),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,X11),implies(X12,implies(X10,X11)))) = true]. % 40.97/41.38 [95=param(2,93),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,X11),implies(X12,implies(X10,X11))),X13)),true,is_a_theorem(X13),true) = true]. % 40.97/41.38 [96=param(6,93),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),X11),implies(X13,X11))) = true]. % 40.97/41.38 [111=param(2,96),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(X10,implies(X11,X12)),X11),implies(X13,X11)),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [112=param(6,96),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(X12,implies(X11,X13))),implies(X14,implies(X12,implies(X11,X13))))) = true]. % 40.97/41.38 [185=param(95,112),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,implies(X12,X12)))) = true]. % 40.97/41.38 [190=param(10,185),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,X11))) = true]. % 40.97/41.38 [197=param(10,190),[3], % 40.97/41.38 is_a_theorem(implies(X10,X10)) = true]. % 40.97/41.38 [200=param(6,197),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X10),implies(X12,X10))) = true]. % 40.97/41.38 [202=param(2,200),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(X10,X11),X10),implies(X12,X10)),X13)),true,is_a_theorem(X13),true) = true]. % 40.97/41.38 [203=param(6,200),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(X11,X12)),implies(X13,implies(X11,X12)))) = true]. % 40.97/41.38 [274=param(6,203),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X13,X11)),implies(X14,implies(X13,X11)))) = true]. % 40.97/41.38 [282=param(6,274),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),implies(X13,implies(X12,X14))),implies(X15,implies(X13,implies(X12,X14))))) = true]. % 40.97/41.38 [283=param(10,274),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(implies(X11,X12),X13),X12),implies(X11,X12)))) = true]. % 40.97/41.38 [288=param(10,283),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X12),X11),implies(X10,X11))) = true]. % 40.97/41.38 [290=param(2,288),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,X11),X12),X11)),true,is_a_theorem(implies(X10,X11)),true) = true]. % 40.97/41.38 [292=param(6,288),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(implies(X10,X11),X12)),implies(X13,implies(implies(X10,X11),X12)))) = true]. % 40.97/41.38 [344=param(111,292),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(X11,implies(X12,X13)),X12),X12))) = true]. % 40.97/41.38 [345=param(202,292),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(X11,X12),X11),X11))) = true]. % 40.97/41.38 [358=param(10,345),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X10),X10)) = true]. % 40.97/41.38 [362=param(6,358),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X10,X11)),implies(X12,implies(X10,X11)))) = true]. % 40.97/41.38 [363=param(2,362),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,implies(X10,X11))),true,is_a_theorem(implies(X12,implies(X10,X11))),true) = true]. % 40.97/41.38 [364=param(2,362),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,implies(X10,X11)),implies(X12,implies(X10,X11))),X13)),true,is_a_theorem(X13),true) = true]. % 40.97/41.38 [390=param(10,344),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),X11),X11)) = true]. % 40.97/41.38 [394=param(6,390),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X11,implies(X10,X12))),implies(X13,implies(X11,implies(X10,X12))))) = true]. % 40.97/41.38 [443=param(363,362),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(X11,implies(X11,X12)),implies(X11,X12)))) = true]. % 40.97/41.38 [450=param(10,443),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X10,X11)),implies(X10,X11))) = true]. % 40.97/41.38 [452=param(2,450),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,implies(X10,X11))),true,is_a_theorem(implies(X10,X11)),true) = true]. % 40.97/41.38 [464=param(452,203),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(X11,X12)),implies(X11,X12))) = true]. % 40.97/41.38 [487=param(6,464),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(X12,X10)),implies(X13,implies(X12,X10)))) = true]. % 40.97/41.38 [496=param(290,487),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,implies(X12,X10)))) = true]. % 40.97/41.38 [500=param(2,496),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,implies(X11,implies(X12,X10))),X13)),true,is_a_theorem(X13),true) = true]. % 40.97/41.38 [501=param(6,496),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,implies(X12,X13))),X12),implies(X14,X12))) = true]. % 40.97/41.38 [565=param(452,501),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,implies(X12,X13))),X12),X12)) = true]. % 40.97/41.38 [569=param(6,565),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X11,implies(X12,implies(X10,X13)))),implies(X14,implies(X11,implies(X12,implies(X10,X13)))))) = true]. % 40.97/41.38 [586=param(10,282),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(X11,X12),X13),implies(X12,X13)))) = true]. % 40.97/41.38 [592=param(10,586),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(X11,X12))) = true]. % 40.97/41.38 [595=param(2,592),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,X11),X12)),true,is_a_theorem(implies(X11,X12)),true) = true]. % 40.97/41.38 [597=param(10,592),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(X10,X11),implies(X12,X11)))) = true]. % 40.97/41.38 [599=param(2,597),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,implies(implies(X10,X11),implies(X12,X11))),X13)),true,is_a_theorem(X13),true) = true]. % 40.97/41.38 [600=param(6,597),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(X10,X11),X12),implies(X13,X12)),X10),implies(X14,X10))) = true]. % 40.97/41.38 [839=param(452,600),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(X10,X11),X12),implies(X13,X12)),X10),X10)) = true]. % 40.97/41.38 [842=param(2,839),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(implies(implies(X10,X11),X12),implies(X13,X12)),X10),X10),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [944=param(452,394),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X11,implies(X10,X12))),implies(X11,implies(X10,X12)))) = true]. % 40.97/41.38 [946=param(2,944),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,implies(X11,implies(X10,X12)))),true,is_a_theorem(implies(X11,implies(X10,X12))),true) = true]. % 40.97/41.38 [948=param(10,944),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,X11),implies(implies(implies(X11,X12),X10),X11))) = true]. % 40.97/41.38 [952=param(2,948),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,X11)),true,is_a_theorem(implies(implies(implies(X11,X12),X10),X11)),true) = true]. % 40.97/41.38 [956=param(202,948),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X12),implies(implies(X11,X13),X11)),implies(X10,X11))) = true]. % 40.97/41.38 [969=param(364,948),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,implies(X11,X12)),X13),implies(X11,implies(X11,X12))),implies(X10,implies(X11,X12)))) = true]. % 40.97/41.38 [975=param(500,948),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,implies(X11,X12)),X13),X12),implies(X10,implies(X11,X12)))) = true]. % 40.97/41.38 [1068=param(952,597),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(X10,X11),implies(X12,X11)),X13),X10),implies(implies(X10,X11),implies(X12,X11)))) = true]. % 40.97/41.38 [1163=param(2,975),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,implies(X11,X12)),X13),X12)),true,is_a_theorem(implies(X10,implies(X11,X12))),true) = true]. % 40.97/41.38 [1168=param(2,956),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(X11,X13),X11))),true,is_a_theorem(implies(X10,X11)),true) = true]. % 40.97/41.38 [1258=param(452,569),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X11,implies(X12,implies(X10,X13)))),implies(X11,implies(X12,implies(X10,X13))))) = true]. % 40.97/41.38 [1259=param(2,1258),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,implies(X11,implies(X12,implies(X10,X13))))),true,is_a_theorem(implies(X11,implies(X12,implies(X10,X13)))),true) = true]. % 40.97/41.38 [1420=param(1168,839),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(implies(X10,X11),X12),implies(X10,X11)),X13),X11),implies(X10,X11))) = true]. % 40.97/41.38 [1424=param(1168,1420),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(X10,X11),X10),X12),implies(implies(X10,X11),X10)),X10)) = true]. % 40.97/41.38 [1426=param(6,1424),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(implies(implies(X10,X11),X10),X12)),implies(X13,implies(implies(implies(X10,X11),X10),X12)))) = true]. % 40.97/41.38 [1932=param(6,1426),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(implies(implies(X11,X12),X11),X13)),X11),implies(X14,X11))) = true]. % 40.97/41.38 [1961=param(452,1932),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(implies(implies(X11,X12),X11),X13)),X11),X11)) = true]. % 40.97/41.38 [1964=param(2,1961),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(X10,implies(implies(implies(X11,X12),X11),X13)),X11),X11),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [2147=param(1964,1068),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,X11),implies(implies(implies(X10,X12),X10),X11))) = true]. % 40.97/41.38 [2148=param(2,2147),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,X11)),true,is_a_theorem(implies(implies(implies(X10,X12),X10),X11)),true) = true]. % 40.97/41.38 [2155=param(599,2147),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X10),implies(implies(X10,X12),implies(X13,X12)))) = true]. % 40.97/41.38 [2167=param(2,2155),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(X10,X11),X10),implies(implies(X10,X12),implies(X13,X12))),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [2168=param(6,2155),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X12,X11)),implies(X10,X13)),implies(X14,implies(X10,X13)))) = true]. % 40.97/41.38 [2172=param(1163,2155),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,implies(implies(X10,X12),implies(X13,X12))))) = true]. % 40.97/41.38 [2174=param(2,2172),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,implies(X11,implies(implies(X10,X12),implies(X13,X12)))),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [2199=param(2148,2172),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X10),implies(X12,implies(implies(X10,X13),implies(X14,X13))))) = true]. % 40.97/41.38 [2205=param(1163,2199),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,implies(X12,implies(implies(X10,X13),implies(X14,X13)))))) = true]. % 40.97/41.38 [2209=param(2,2205),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,implies(X11,implies(X12,implies(implies(X10,X13),implies(X14,X13))))),X15)),true,is_a_theorem(X15),true) = true]. % 40.97/41.38 [2671=param(2167,969),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(X10,X11),X11))) = true]. % 40.97/41.38 [2677=param(595,2671),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(X11,X10),X12),X12))) = true]. % 40.97/41.38 [2688=param(952,2671),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(implies(X10,X11),X11),X12),X10),implies(implies(X10,X11),X11))) = true]. % 40.97/41.38 [2691=param(2148,2671),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X10),implies(implies(X10,X12),X12))) = true]. % 40.97/41.38 [2702=param(2,2677),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,implies(implies(implies(X11,X10),X12),X12)),X13)),true,is_a_theorem(X13),true) = true]. % 40.97/41.38 [2817=param(452,2168),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X12,X11)),implies(X10,X13)),implies(X10,X13))) = true]. % 40.97/41.38 [3041=param(6,2691),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X11),implies(X10,X12)),implies(X13,implies(X10,X12)))) = true]. % 40.97/41.38 [3049=param(1163,2691),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,implies(implies(X10,X12),X12)))) = true]. % 40.97/41.38 [3059=param(595,3049),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(X11,implies(implies(implies(X12,X10),X13),X13)))) = true]. % 40.97/41.38 [3068=param(952,3049),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,implies(implies(X11,X12),X12)),X13),X11),implies(X10,implies(implies(X11,X12),X12)))) = true]. % 40.97/41.38 [3082=param(2,3059),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,implies(X11,implies(implies(implies(X12,X10),X13),X13))),X14)),true,is_a_theorem(X14),true) = true]. % 40.97/41.38 [3569=param(452,3041),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X11),implies(X10,X12)),implies(X10,X12))) = true]. % 40.97/41.38 [3582=param(6,3569),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(implies(X10,X12),X12)),implies(X13,implies(implies(X10,X12),X12)))) = true]. % 40.97/41.38 [3586=param(2174,3569),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(implies(X10,X11),X11),X12),implies(X13,X12)))) = true]. % 40.97/41.38 [3609=param(946,3586),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X11),X12),implies(X10,X12))) = true]. % 40.97/41.38 [3619=param(2,3609),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(X10,X11),X11),X12)),true,is_a_theorem(implies(X10,X12)),true) = true]. % 40.97/41.38 [4691=param(2174,2817),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(implies(X10,X11),implies(X12,X11)),X13),implies(X14,X13)))) = true]. % 40.97/41.38 [4705=param(946,4691),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X12,X11)),X13),implies(X10,X13))) = true]. % 40.97/41.38 [4730=param(3619,4705),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,X11),implies(X10,implies(X12,X11)))) = true]. % 40.97/41.38 [4731=param(2,4730),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(X10,X11)),true,is_a_theorem(implies(X10,implies(X12,X11))),true) = true]. % 40.97/41.38 [4742=param(2148,4730),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X12),implies(X10,X11)),implies(X10,implies(X13,X11)))) = true]. % 40.97/41.38 [5648=param(2,2688),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(implies(implies(X10,X11),X11),X12),X10)),true,is_a_theorem(implies(implies(X10,X11),X11)),true) = true]. % 40.97/41.38 [7197=param(452,3582),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),implies(implies(X10,X12),X12)),implies(implies(X10,X12),X12))) = true]. % 40.97/41.38 [7202=param(2,7197),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,X11),implies(implies(X10,X12),X12))),true,is_a_theorem(implies(implies(X10,X12),X12)),true) = true]. % 40.97/41.38 [8024=param(842,3068),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(X10,X12),X12))) = true]. % 40.97/41.38 [8026=param(2,8024),[3], % 40.97/41.38 ifeq(is_a_theorem(implies(implies(X10,X11),X12)),true,is_a_theorem(implies(implies(X10,X12),X12)),true) = true]. % 40.97/41.38 [8103=param(8026,4742),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(implies(X10,X11),X12),implies(X10,implies(X13,X11))),implies(X10,implies(X13,X11)))) = true]. % 40.97/41.38 [8165=param(3082,8103),[3], % 40.97/41.38 is_a_theorem(implies(X10,implies(implies(implies(X11,implies(implies(X10,X12),X13)),X12),X12))) = true]. % 40.97/41.38 [8207=param(2148,8165),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,X11),X10),implies(implies(implies(X12,implies(implies(X10,X13),X14)),X13),X13))) = true]. % 40.97/41.38 [8607=param(7202,8207),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(implies(X10,X11),X12)),X11),X11)) = true]. % 40.97/41.38 [8632=param(4731,8607),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(implies(X10,X11),X12)),X11),implies(X13,X11))) = true]. % 40.97/41.38 [8654=param(8026,8632),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(implies(X10,X11),X12)),implies(X13,X11)),implies(X13,X11))) = true]. % 40.97/41.38 [8666=param(2702,8654),[3], % 40.97/41.38 is_a_theorem(implies(implies(implies(X10,implies(X11,implies(implies(X11,X12),X13))),X12),X12)) = true]. % 40.97/41.38 [11944=param(5648,8666),[3], % 40.97/41.38 is_a_theorem(implies(implies(X10,implies(X11,implies(implies(X11,X10),X12))),implies(X11,implies(implies(X11,X10),X12)))) = true]. % 41.06/41.45 [11954=param(2209,11944),[3], % 41.06/41.45 is_a_theorem(implies(X10,implies(implies(X10,X11),implies(implies(X11,X12),implies(X13,X12))))) = true]. % 41.06/41.45 [13342=param(1259,11954),[3], % 41.06/41.45 is_a_theorem(implies(implies(X10,X11),implies(implies(X11,X12),implies(X10,X12)))) = true]. % 41.06/41.45 [13391=param(5,13342),[4], % 41.06/41.45 thmtrue = thmfalse]. % 41.06/41.45 % SZS output end CNFRefutation % 41.06/41.45 Space: 1197938 KB %------------------------------------------------------------------------------