%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LCL400-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n016.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:35:18 EDT 2022 % Result : Unsatisfiable 4.27s 4.68s % Output : CNFRefutation 4.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : LCL400-10 : TPTP v8.1.0. Released v7.5.0. % 0.11/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n016.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 : Mon Jul 4 13:10:47 EDT 2022 % 0.12/0.34 % CPUTime : % 4.27/4.68 Theorem Proved. % 4.27/4.68 % SZS status Unsatisfiable % 4.27/4.68 % SZS output start CNFRefutation % 4.27/4.68 [1=axiom,[], % 4.27/4.68 is_a_theorem(implies(X10,implies(not(X10),X11))) = true]. % 4.27/4.68 [2=axiom,[], % 4.27/4.68 is_a_theorem(implies(implies(not(X10),X10),X10)) = true]. % 4.27/4.68 [3=axiom,[], % 4.27/4.68 is_a_theorem(implies(implies(X10,X11),implies(implies(X11,X12),implies(X10,X12)))) = true]. % 4.27/4.68 [4=axiom,[], % 4.27/4.68 ifeq(is_a_theorem(implies(X10,X11)),true,ifeq(is_a_theorem(X10),true,is_a_theorem(X11),true),true) = true]. % 4.27/4.68 [5=axiom,[], % 4.27/4.68 ifeq(X10,X10,X11,X12) = X11]. % 4.27/4.68 [6=axiom,[], % 4.27/4.68 thtop(X10,X10) = thmfalse]. % 4.27/4.68 [7=axiom,[], % 4.27/4.68 thtop(is_a_theorem(implies(not(implies(x,y)),x)),true) = thmtrue]. % 4.27/4.68 [8=param(4,1),[5], % 4.27/4.68 ifeq(is_a_theorem(X10),true,is_a_theorem(implies(not(X10),X11)),true) = true]. % 4.27/4.68 [17=param(4,1),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(X10,implies(not(X10),X11)),X12)),true,is_a_theorem(X12),true) = true]. % 4.27/4.68 [18=param(4,2),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(implies(not(X10),X10),X10),X11)),true,is_a_theorem(X11),true) = true]. % 4.27/4.68 [19=param(4,3),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(X10,X11)),true,is_a_theorem(implies(implies(X11,X12),implies(X10,X12))),true) = true]. % 4.27/4.68 [21=param(17,3),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(not(X10),X11),X12),implies(X10,X12))) = true]. % 4.27/4.68 [22=param(4,21),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(not(X10),X11),X12)),true,is_a_theorem(implies(X10,X12)),true) = true]. % 4.27/4.68 [27=param(18,3),[5], % 4.27/4.68 is_a_theorem(implies(implies(X10,X11),implies(implies(not(X10),X10),X11))) = true]. % 4.27/4.68 [28=param(18,21),[5], % 4.27/4.68 is_a_theorem(implies(X10,X10)) = true]. % 4.27/4.68 [31=param(8,28),[5], % 4.27/4.68 is_a_theorem(implies(not(implies(X10,X10)),X11)) = true]. % 4.27/4.68 [37=param(19,21),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(implies(not(X10),X13),X11),X12))) = true]. % 4.27/4.68 [39=param(19,31),[5], % 4.27/4.68 is_a_theorem(implies(implies(X10,X11),implies(not(implies(X12,X12)),X11))) = true]. % 4.27/4.68 [45=param(22,3),[5], % 4.27/4.68 is_a_theorem(implies(X10,implies(implies(X11,X12),implies(not(X10),X12)))) = true]. % 4.27/4.68 [47=param(22,39),[5], % 4.27/4.68 is_a_theorem(implies(X10,implies(not(implies(X11,X11)),X12))) = true]. % 4.27/4.68 [49=param(19,47),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(not(implies(X10,X10)),X11),X12),implies(X13,X12))) = true]. % 4.27/4.68 [52=param(19,45),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(not(X12),X11)),X13),implies(X12,X13))) = true]. % 4.27/4.68 [74=param(18,49),[5], % 4.27/4.68 is_a_theorem(implies(X10,implies(X11,X11))) = true]. % 4.27/4.68 [76=param(18,37),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(not(not(X10)),X11),X10),X10)) = true]. % 4.27/4.68 [79=param(19,74),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(X10,X10),X11),implies(X12,X11))) = true]. % 4.27/4.68 [84=param(4,79),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(X10,X10),X11)),true,is_a_theorem(implies(X12,X11)),true) = true]. % 4.27/4.68 [93=param(84,27),[5], % 4.27/4.68 is_a_theorem(implies(X10,implies(implies(not(X11),X11),X11))) = true]. % 4.27/4.68 [107=param(19,93),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(implies(not(X10),X10),X10),X11),implies(X12,X11))) = true]. % 4.27/4.68 [240=param(4,79),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(implies(implies(X10,X10),X11),implies(X12,X11)),X13)),true,is_a_theorem(X13),true) = true]. % 4.27/4.68 [242=param(4,76),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(implies(implies(not(not(X10)),X11),X10),X10),X12)),true,is_a_theorem(X12),true) = true]. % 4.27/4.68 [251=param(19,3),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(implies(X10,X11),implies(X12,X11)),X13),implies(implies(X12,X10),X13))) = true]. % 4.27/4.68 [369=param(19,107),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(implies(implies(not(X13),X13),X13),X11),X12))) = true]. % 4.27/4.68 [493=param(240,52),[5], % 4.27/4.68 is_a_theorem(implies(X10,implies(X11,implies(not(X10),X12)))) = true]. % 4.27/4.68 [498=param(19,493),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(X10,implies(not(X11),X12)),X13),implies(X11,X13))) = true]. % 4.27/4.68 [570=param(4,498),[5], % 4.27/4.68 ifeq(is_a_theorem(implies(implies(X10,implies(not(X11),X12)),X13)),true,is_a_theorem(implies(X11,X13)),true) = true]. % 4.27/4.68 [573=param(19,498),[5], % 4.27/4.68 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(implies(X13,implies(not(X10),X14)),X11),X12))) = true]. % 4.27/4.68 [604=param(242,251),[5], % 4.27/4.69 is_a_theorem(implies(implies(X10,not(not(implies(X10,X11)))),implies(X10,X11))) = true]. % 4.27/4.69 [615=param(19,604),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(implies(X10,not(not(implies(X10,X11)))),X12))) = true]. % 4.27/4.69 [883=param(18,615),[5], % 4.27/4.69 is_a_theorem(implies(implies(not(X10),not(not(implies(not(X10),X10)))),X10)) = true]. % 4.27/4.69 [901=param(570,3),[5], % 4.27/4.69 is_a_theorem(implies(X10,implies(implies(implies(not(X10),X11),X12),implies(X13,X12)))) = true]. % 4.27/4.69 [926=param(19,901),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(implies(implies(not(X10),X11),X12),implies(X13,X12)),X14),implies(X10,X14))) = true]. % 4.27/4.69 [966=param(18,369),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(implies(not(X10),X10),X10),X11),X11)) = true]. % 4.27/4.69 [1121=param(17,573),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(X10,implies(not(X11),X12)),X13),implies(not(implies(X11,X13)),X14))) = true]. % 4.27/4.69 [1285=param(4,966),[5], % 4.27/4.69 ifeq(is_a_theorem(implies(implies(implies(implies(implies(not(X10),X10),X10),X11),X11),X12)),true,is_a_theorem(X12),true) = true]. % 4.27/4.69 [1300=param(4,21),[5], % 4.27/4.69 ifeq(is_a_theorem(implies(implies(implies(implies(not(X10),X11),X12),implies(X10,X12)),X13)),true,is_a_theorem(X13),true) = true]. % 4.27/4.69 [3343=param(1285,251),[5], % 4.27/4.69 is_a_theorem(implies(implies(X10,implies(not(X11),X11)),implies(X10,X11))) = true]. % 4.27/4.69 [3345=param(1285,926),[5], % 4.27/4.69 is_a_theorem(implies(X10,implies(X11,X10))) = true]. % 4.27/4.69 [3351=param(19,3345),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(X11,X12))) = true]. % 4.27/4.69 [3493=param(4,3351),[5], % 4.27/4.69 ifeq(is_a_theorem(implies(implies(X10,X11),X12)),true,is_a_theorem(implies(X11,X12)),true) = true]. % 4.27/4.69 [3698=param(4,3343),[5], % 4.27/4.69 ifeq(is_a_theorem(implies(X10,implies(not(X11),X11))),true,is_a_theorem(implies(X10,X11)),true) = true]. % 4.27/4.69 [3818=param(1300,251),[5], % 4.27/4.69 is_a_theorem(implies(implies(X10,not(X11)),implies(X11,implies(X10,X12)))) = true]. % 4.27/4.69 [3822=param(4,3818),[5], % 4.27/4.69 ifeq(is_a_theorem(implies(X10,not(X11))),true,is_a_theorem(implies(X11,implies(X10,X12))),true) = true]. % 4.27/4.69 [4065=param(3493,883),[5], % 4.27/4.69 is_a_theorem(implies(not(not(implies(not(X10),X10))),X10)) = true]. % 4.27/4.69 [4196=param(19,4065),[5], % 4.27/4.69 is_a_theorem(implies(implies(X10,X11),implies(not(not(implies(not(X10),X10))),X11))) = true]. % 4.27/4.69 [4654=param(22,4196),[5], % 4.27/4.69 is_a_theorem(implies(X10,implies(not(not(implies(not(not(X10)),not(X10)))),X11))) = true]. % 4.27/4.69 [5770=param(3698,4654),[5], % 4.27/4.69 is_a_theorem(implies(X10,not(implies(not(not(X10)),not(X10))))) = true]. % 4.27/4.69 [5968=param(3822,5770),[5], % 4.27/4.69 is_a_theorem(implies(implies(not(not(X10)),not(X10)),implies(X10,X11))) = true]. % 4.27/4.69 [6095=param(22,5968),[5], % 4.27/4.69 is_a_theorem(implies(not(X10),implies(X10,X11))) = true]. % 4.27/4.69 [6119=param(19,6095),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(X10,X11),X12),implies(not(X10),X12))) = true]. % 4.27/4.69 [11342=param(3698,6119),[5], % 4.27/4.69 is_a_theorem(implies(implies(implies(X10,X11),X10),X10)) = true]. % 4.27/4.69 [11349=param(4,11342),[5], % 4.27/4.69 ifeq(is_a_theorem(implies(implies(X10,X11),X10)),true,is_a_theorem(X10),true) = true]. % 4.27/4.69 [11561=param(11349,1121),[5], % 4.27/4.69 is_a_theorem(implies(not(implies(X10,X11)),implies(not(X10),X12))) = true]. % 4.27/4.69 [11588=param(3698,11561),[5], % 4.27/4.69 is_a_theorem(implies(not(implies(X10,X11)),X10)) = true]. % 4.27/4.69 [11597=param(7,11588),[6], % 4.27/4.69 thmtrue = thmfalse]. % 4.27/4.69 % SZS output end CNFRefutation % 4.27/4.69 Space: 95165 KB %------------------------------------------------------------------------------