%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL875-1 : TPTP v9.3.1. Bugfixed v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:03:16 PM UTC 2026
% Result : Unsatisfiable 55.75s 7.49s
% Output : Proof 55.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 93
% Number of leaves : 52
% Syntax : Number of formulae : 633 ( 629 unt; 0 def)
% Number of atoms : 641 ( 608 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 68 ( 60 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 71 ( 71 usr; 69 con; 0-4 aty)
% Number of variables : 134 ( 2 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
sFlat0 = implies(y,y),
introduced(definition) ).
cnf(t120,plain,
implies(y,y) = sFlat0,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sFlat1 = implies(z,z),
introduced(definition) ).
cnf(t118,plain,
implies(z,z) = sFlat1,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sFlat2 = implies(u,u),
introduced(definition) ).
cnf(t106,plain,
implies(u,u) = sFlat2,
inference(orient,[status(thm)],[t8]) ).
cnf(t9,axiom,
sFlat3 = implies(v,v),
introduced(definition) ).
cnf(t102,plain,
implies(v,v) = sFlat3,
inference(orient,[status(thm)],[t9]) ).
cnf(t10,axiom,
sFlat4 = implies(x,w),
introduced(definition) ).
cnf(t123,plain,
implies(x,w) = sFlat4,
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
sFlat5 = implies(implies(v,v),implies(x,w)),
introduced(definition) ).
cnf(t75,plain,
implies(implies(v,v),implies(x,w)) = sFlat5,
inference(orient,[status(thm)],[t11]) ).
cnf(t22335,plain,
implies(sFlat3,implies(x,w)) = sFlat5,
inference(step,[status(thm)],[t75,t102]) ).
cnf(t103,plain,
implies(sFlat3,implies(x,w)) = sFlat5,
inference(rw,[status(thm)],[t22335]) ).
cnf(t22374,plain,
implies(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t103,t123]) ).
cnf(t449,plain,
implies(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t22374]) ).
cnf(t12,axiom,
sFlat6 = implies(implies(u,u),implies(implies(v,v),implies(x,w))),
introduced(definition) ).
cnf(t22302,plain,
sFlat6 = implies(implies(u,u),sFlat5),
inference(step,[status(thm)],[t12,t75]) ).
cnf(t78,plain,
implies(implies(u,u),sFlat5) = sFlat6,
inference(orient,[status(thm)],[t22302]) ).
cnf(t22337,plain,
implies(sFlat2,sFlat5) = sFlat6,
inference(step,[status(thm)],[t78,t106]) ).
cnf(t107,plain,
implies(sFlat2,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t22337]) ).
cnf(t377,plain,
implies(sFlat2,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t107]) ).
cnf(t13,axiom,
sFlat7 = implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w)))),
introduced(definition) ).
cnf(t22312,plain,
sFlat7 = implies(implies(z,z),implies(implies(u,u),sFlat5)),
inference(step,[status(thm)],[t13,t75]) ).
cnf(t22313,plain,
sFlat7 = implies(implies(z,z),sFlat6),
inference(step,[status(thm)],[t22312,t78]) ).
cnf(t86,plain,
implies(implies(z,z),sFlat6) = sFlat7,
inference(orient,[status(thm)],[t22313]) ).
cnf(t22345,plain,
implies(sFlat1,sFlat6) = sFlat7,
inference(step,[status(thm)],[t86,t118]) ).
cnf(t119,plain,
implies(sFlat1,sFlat6) = sFlat7,
inference(rw,[status(thm)],[t22345]) ).
cnf(t395,plain,
implies(sFlat1,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t119]) ).
cnf(t14,axiom,
sFlat8 = implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),
introduced(definition) ).
cnf(t22314,plain,
sFlat8 = implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),sFlat5))),
inference(step,[status(thm)],[t14,t75]) ).
cnf(t22315,plain,
sFlat8 = implies(implies(y,y),implies(implies(z,z),sFlat6)),
inference(step,[status(thm)],[t22314,t78]) ).
cnf(t22316,plain,
sFlat8 = implies(implies(y,y),sFlat7),
inference(step,[status(thm)],[t22315,t86]) ).
cnf(t87,plain,
implies(implies(y,y),sFlat7) = sFlat8,
inference(orient,[status(thm)],[t22316]) ).
cnf(t22346,plain,
implies(sFlat0,sFlat7) = sFlat8,
inference(step,[status(thm)],[t87,t120]) ).
cnf(t121,plain,
implies(sFlat0,sFlat7) = sFlat8,
inference(rw,[status(thm)],[t22346]) ).
cnf(t404,plain,
implies(sFlat0,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t121]) ).
cnf(t15,axiom,
sFlat9 = implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w),
introduced(definition) ).
cnf(t65,plain,
implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w) = sFlat9,
inference(orient,[status(thm)],[t15]) ).
cnf(t22299,plain,
implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),sFlat5))),w) = sFlat9,
inference(step,[status(thm)],[t65,t75]) ).
cnf(t76,plain,
implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),sFlat5))),w) = sFlat9,
inference(rw,[status(thm)],[t22299]) ).
cnf(t22529,plain,
implies(implies(sFlat0,implies(implies(z,z),implies(implies(u,u),sFlat5))),w) = sFlat9,
inference(step,[status(thm)],[t76,t120]) ).
cnf(t22530,plain,
implies(implies(sFlat0,implies(sFlat1,implies(implies(u,u),sFlat5))),w) = sFlat9,
inference(step,[status(thm)],[t22529,t118]) ).
cnf(t22531,plain,
implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,sFlat5))),w) = sFlat9,
inference(step,[status(thm)],[t22530,t106]) ).
cnf(t22532,plain,
implies(implies(sFlat0,implies(sFlat1,sFlat6)),w) = sFlat9,
inference(step,[status(thm)],[t22531,t377]) ).
cnf(t22533,plain,
implies(implies(sFlat0,sFlat7),w) = sFlat9,
inference(step,[status(thm)],[t22532,t395]) ).
cnf(t22534,plain,
implies(sFlat8,w) = sFlat9,
inference(step,[status(thm)],[t22533,t404]) ).
cnf(t1977,plain,
implies(sFlat8,w) = sFlat9,
inference(orient,[status(thm)],[t22534]) ).
cnf(t16,axiom,
sFlat10 = implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),
introduced(definition) ).
cnf(t22347,plain,
sFlat10 = implies(x,implies(implies(sFlat0,implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),
inference(step,[status(thm)],[t16,t120]) ).
cnf(t22348,plain,
sFlat10 = implies(x,implies(implies(sFlat0,implies(sFlat1,implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),
inference(step,[status(thm)],[t22347,t118]) ).
cnf(t22349,plain,
sFlat10 = implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(implies(v,v),implies(x,w))))),w)),
inference(step,[status(thm)],[t22348,t106]) ).
cnf(t22350,plain,
sFlat10 = implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(sFlat3,implies(x,w))))),w)),
inference(step,[status(thm)],[t22349,t102]) ).
cnf(t122,plain,
implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(sFlat3,implies(x,w))))),w)) = sFlat10,
inference(orient,[status(thm)],[t22350]) ).
cnf(t22351,plain,
implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(sFlat3,sFlat4)))),w)) = sFlat10,
inference(step,[status(thm)],[t122,t123]) ).
cnf(t124,plain,
implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(sFlat3,sFlat4)))),w)) = sFlat10,
inference(rw,[status(thm)],[t22351]) ).
cnf(t22580,plain,
implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,sFlat5))),w)) = sFlat10,
inference(step,[status(thm)],[t124,t449]) ).
cnf(t22581,plain,
implies(x,implies(implies(sFlat0,implies(sFlat1,sFlat6)),w)) = sFlat10,
inference(step,[status(thm)],[t22580,t377]) ).
cnf(t22582,plain,
implies(x,implies(implies(sFlat0,sFlat7),w)) = sFlat10,
inference(step,[status(thm)],[t22581,t395]) ).
cnf(t22583,plain,
implies(x,implies(sFlat8,w)) = sFlat10,
inference(step,[status(thm)],[t22582,t404]) ).
cnf(t22584,plain,
implies(x,sFlat9) = sFlat10,
inference(step,[status(thm)],[t22583,t1977]) ).
cnf(t3882,plain,
implies(x,sFlat9) = sFlat10,
inference(orient,[status(thm)],[t22584]) ).
cnf(t17,axiom,
sFlat11 = implies(v6,v7),
introduced(definition) ).
cnf(t115,plain,
implies(v6,v7) = sFlat11,
inference(orient,[status(thm)],[t17]) ).
cnf(t18,axiom,
sFlat12 = implies(v7,v8),
introduced(definition) ).
cnf(t117,plain,
implies(v7,v8) = sFlat12,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat13 = implies(v6,v8),
introduced(definition) ).
cnf(t113,plain,
implies(v6,v8) = sFlat13,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sFlat14 = implies(implies(v7,v8),implies(v6,v8)),
introduced(definition) ).
cnf(t84,plain,
implies(implies(v7,v8),implies(v6,v8)) = sFlat14,
inference(orient,[status(thm)],[t20]) ).
cnf(t22343,plain,
implies(implies(v7,v8),sFlat13) = sFlat14,
inference(step,[status(thm)],[t84,t113]) ).
cnf(t114,plain,
implies(implies(v7,v8),sFlat13) = sFlat14,
inference(rw,[status(thm)],[t22343]) ).
cnf(t22375,plain,
implies(sFlat12,sFlat13) = sFlat14,
inference(step,[status(thm)],[t114,t117]) ).
cnf(t458,plain,
implies(sFlat12,sFlat13) = sFlat14,
inference(orient,[status(thm)],[t22375]) ).
cnf(t21,axiom,
sFlat15 = implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),
introduced(definition) ).
cnf(t82,plain,
implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))) = sFlat15,
inference(orient,[status(thm)],[t21]) ).
cnf(t22311,plain,
implies(implies(v6,v7),sFlat14) = sFlat15,
inference(step,[status(thm)],[t82,t84]) ).
cnf(t85,plain,
implies(implies(v6,v7),sFlat14) = sFlat15,
inference(rw,[status(thm)],[t22311]) ).
cnf(t22370,plain,
implies(sFlat11,sFlat14) = sFlat15,
inference(step,[status(thm)],[t85,t115]) ).
cnf(t413,plain,
implies(sFlat11,sFlat14) = sFlat15,
inference(orient,[status(thm)],[t22370]) ).
cnf(t22,axiom,
sFlat16 = implies(v9,v10),
introduced(definition) ).
cnf(t91,plain,
implies(v9,v10) = sFlat16,
inference(orient,[status(thm)],[t22]) ).
cnf(t23,axiom,
sFlat17 = implies(v9,implies(v9,v10)),
introduced(definition) ).
cnf(t89,plain,
implies(v9,implies(v9,v10)) = sFlat17,
inference(orient,[status(thm)],[t23]) ).
cnf(t22330,plain,
implies(v9,sFlat16) = sFlat17,
inference(step,[status(thm)],[t89,t91]) ).
cnf(t92,plain,
implies(v9,sFlat16) = sFlat17,
inference(rw,[status(thm)],[t22330]) ).
cnf(t340,plain,
implies(v9,sFlat16) = sFlat17,
inference(orient,[status(thm)],[t92]) ).
cnf(t24,axiom,
sFlat18 = implies(implies(v9,implies(v9,v10)),implies(v9,v10)),
introduced(definition) ).
cnf(t67,plain,
implies(implies(v9,implies(v9,v10)),implies(v9,v10)) = sFlat18,
inference(orient,[status(thm)],[t24]) ).
cnf(t22329,plain,
implies(sFlat17,implies(v9,v10)) = sFlat18,
inference(step,[status(thm)],[t67,t89]) ).
cnf(t90,plain,
implies(sFlat17,implies(v9,v10)) = sFlat18,
inference(rw,[status(thm)],[t22329]) ).
cnf(t22371,plain,
implies(sFlat17,sFlat16) = sFlat18,
inference(step,[status(thm)],[t90,t91]) ).
cnf(t422,plain,
implies(sFlat17,sFlat16) = sFlat18,
inference(orient,[status(thm)],[t22371]) ).
cnf(t25,axiom,
sFlat19 = implies(v11,v12),
introduced(definition) ).
cnf(t96,plain,
implies(v11,v12) = sFlat19,
inference(orient,[status(thm)],[t25]) ).
cnf(t26,axiom,
sFlat20 = implies(v12,v13),
introduced(definition) ).
cnf(t93,plain,
implies(v12,v13) = sFlat20,
inference(orient,[status(thm)],[t26]) ).
cnf(t27,axiom,
sFlat21 = implies(v11,v13),
introduced(definition) ).
cnf(t95,plain,
implies(v11,v13) = sFlat21,
inference(orient,[status(thm)],[t27]) ).
cnf(t28,axiom,
sFlat22 = implies(implies(v12,v13),implies(v11,v13)),
introduced(definition) ).
cnf(t69,plain,
implies(implies(v12,v13),implies(v11,v13)) = sFlat22,
inference(orient,[status(thm)],[t28]) ).
cnf(t22331,plain,
implies(sFlat20,implies(v11,v13)) = sFlat22,
inference(step,[status(thm)],[t69,t93]) ).
cnf(t94,plain,
implies(sFlat20,implies(v11,v13)) = sFlat22,
inference(rw,[status(thm)],[t22331]) ).
cnf(t22372,plain,
implies(sFlat20,sFlat21) = sFlat22,
inference(step,[status(thm)],[t94,t95]) ).
cnf(t431,plain,
implies(sFlat20,sFlat21) = sFlat22,
inference(orient,[status(thm)],[t22372]) ).
cnf(t29,axiom,
sFlat23 = implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),
introduced(definition) ).
cnf(t22296,plain,
sFlat23 = implies(implies(v11,v12),sFlat22),
inference(step,[status(thm)],[t29,t69]) ).
cnf(t71,plain,
implies(implies(v11,v12),sFlat22) = sFlat23,
inference(orient,[status(thm)],[t22296]) ).
cnf(t22332,plain,
implies(sFlat19,sFlat22) = sFlat23,
inference(step,[status(thm)],[t71,t96]) ).
cnf(t97,plain,
implies(sFlat19,sFlat22) = sFlat23,
inference(rw,[status(thm)],[t22332]) ).
cnf(t350,plain,
implies(sFlat19,sFlat22) = sFlat23,
inference(orient,[status(thm)],[t97]) ).
cnf(t30,axiom,
sFlat24 = implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14),
introduced(definition) ).
cnf(t60,plain,
implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14) = sFlat24,
inference(orient,[status(thm)],[t30]) ).
cnf(t22295,plain,
implies(implies(implies(v11,v12),sFlat22),v14) = sFlat24,
inference(step,[status(thm)],[t60,t69]) ).
cnf(t70,plain,
implies(implies(implies(v11,v12),sFlat22),v14) = sFlat24,
inference(rw,[status(thm)],[t22295]) ).
cnf(t22416,plain,
implies(implies(sFlat19,sFlat22),v14) = sFlat24,
inference(step,[status(thm)],[t70,t96]) ).
cnf(t22417,plain,
implies(sFlat23,v14) = sFlat24,
inference(step,[status(thm)],[t22416,t350]) ).
cnf(t611,plain,
implies(sFlat23,v14) = sFlat24,
inference(orient,[status(thm)],[t22417]) ).
cnf(t31,axiom,
sFlat25 = implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),
introduced(definition) ).
cnf(t58,plain,
implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)) = sFlat25,
inference(orient,[status(thm)],[t31]) ).
cnf(t22287,plain,
implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),sFlat24) = sFlat25,
inference(step,[status(thm)],[t58,t60]) ).
cnf(t61,plain,
implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),sFlat24) = sFlat25,
inference(rw,[status(thm)],[t22287]) ).
cnf(t22404,plain,
implies(implies(implies(v9,sFlat16),implies(v9,v10)),sFlat24) = sFlat25,
inference(step,[status(thm)],[t61,t91]) ).
cnf(t22405,plain,
implies(implies(sFlat17,implies(v9,v10)),sFlat24) = sFlat25,
inference(step,[status(thm)],[t22404,t340]) ).
cnf(t22406,plain,
implies(implies(sFlat17,sFlat16),sFlat24) = sFlat25,
inference(step,[status(thm)],[t22405,t91]) ).
cnf(t22407,plain,
implies(sFlat18,sFlat24) = sFlat25,
inference(step,[status(thm)],[t22406,t422]) ).
cnf(t570,plain,
implies(sFlat18,sFlat24) = sFlat25,
inference(orient,[status(thm)],[t22407]) ).
cnf(t32,axiom,
sFlat26 = implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),
introduced(definition) ).
cnf(t55,plain,
implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14) = sFlat26,
inference(orient,[status(thm)],[t32]) ).
cnf(t22286,plain,
implies(sFlat25,v14) = sFlat26,
inference(step,[status(thm)],[t55,t58]) ).
cnf(t59,plain,
implies(sFlat25,v14) = sFlat26,
inference(rw,[status(thm)],[t22286]) ).
cnf(t331,plain,
implies(sFlat25,v14) = sFlat26,
inference(orient,[status(thm)],[t59]) ).
cnf(t33,axiom,
sFlat27 = implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15),
introduced(definition) ).
cnf(t53,plain,
implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15) = sFlat27,
inference(orient,[status(thm)],[t33]) ).
cnf(t22284,plain,
implies(sFlat26,v15) = sFlat27,
inference(step,[status(thm)],[t53,t55]) ).
cnf(t56,plain,
implies(sFlat26,v15) = sFlat27,
inference(rw,[status(thm)],[t22284]) ).
cnf(t322,plain,
implies(sFlat26,v15) = sFlat27,
inference(orient,[status(thm)],[t56]) ).
cnf(t34,axiom,
sFlat28 = implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),
introduced(definition) ).
cnf(t22289,plain,
sFlat28 = implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),sFlat24),v14),v15)),
inference(step,[status(thm)],[t34,t60]) ).
cnf(t64,plain,
implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),sFlat24),v14),v15)) = sFlat28,
inference(orient,[status(thm)],[t22289]) ).
cnf(t22294,plain,
implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(step,[status(thm)],[t64,t67]) ).
cnf(t68,plain,
implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(rw,[status(thm)],[t22294]) ).
cnf(t22472,plain,
implies(implies(sFlat11,implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(step,[status(thm)],[t68,t115]) ).
cnf(t22473,plain,
implies(implies(sFlat11,implies(sFlat12,implies(v6,v8))),implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(step,[status(thm)],[t22472,t117]) ).
cnf(t22474,plain,
implies(implies(sFlat11,implies(sFlat12,sFlat13)),implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(step,[status(thm)],[t22473,t113]) ).
cnf(t22475,plain,
implies(implies(sFlat11,sFlat14),implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(step,[status(thm)],[t22474,t458]) ).
cnf(t22476,plain,
implies(sFlat15,implies(implies(implies(sFlat18,sFlat24),v14),v15)) = sFlat28,
inference(step,[status(thm)],[t22475,t413]) ).
cnf(t22477,plain,
implies(sFlat15,implies(implies(sFlat25,v14),v15)) = sFlat28,
inference(step,[status(thm)],[t22476,t570]) ).
cnf(t22478,plain,
implies(sFlat15,implies(sFlat26,v15)) = sFlat28,
inference(step,[status(thm)],[t22477,t331]) ).
cnf(t22479,plain,
implies(sFlat15,sFlat27) = sFlat28,
inference(step,[status(thm)],[t22478,t322]) ).
cnf(t1099,plain,
implies(sFlat15,sFlat27) = sFlat28,
inference(orient,[status(thm)],[t22479]) ).
cnf(t35,axiom,
sFlat29 = implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),
introduced(definition) ).
cnf(t22285,plain,
sFlat29 = implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(sFlat26,v15)),v15),
inference(step,[status(thm)],[t35,t55]) ).
cnf(t57,plain,
implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(sFlat26,v15)),v15) = sFlat29,
inference(orient,[status(thm)],[t22285]) ).
cnf(t22310,plain,
implies(implies(sFlat15,implies(sFlat26,v15)),v15) = sFlat29,
inference(step,[status(thm)],[t57,t82]) ).
cnf(t83,plain,
implies(implies(sFlat15,implies(sFlat26,v15)),v15) = sFlat29,
inference(rw,[status(thm)],[t22310]) ).
cnf(t22419,plain,
implies(implies(sFlat15,sFlat27),v15) = sFlat29,
inference(step,[status(thm)],[t83,t322]) ).
cnf(t633,plain,
implies(implies(sFlat15,sFlat27),v15) = sFlat29,
inference(orient,[status(thm)],[t22419]) ).
cnf(t22480,plain,
implies(sFlat28,v15) = sFlat29,
inference(step,[status(thm)],[t633,t1099]) ).
cnf(t1108,plain,
implies(sFlat28,v15) = sFlat29,
inference(rw,[status(thm)],[t22480]) ).
cnf(t1110,plain,
implies(sFlat28,v15) = sFlat29,
inference(orient,[status(thm)],[t1108]) ).
cnf(t36,axiom,
sFlat30 = implies(v17,v17),
introduced(definition) ).
cnf(t111,plain,
implies(v17,v17) = sFlat30,
inference(orient,[status(thm)],[t36]) ).
cnf(t37,axiom,
sFlat31 = implies(v18,v18),
introduced(definition) ).
cnf(t104,plain,
implies(v18,v18) = sFlat31,
inference(orient,[status(thm)],[t37]) ).
cnf(t38,axiom,
sFlat32 = implies(v19,v19),
introduced(definition) ).
cnf(t100,plain,
implies(v19,v19) = sFlat32,
inference(orient,[status(thm)],[t38]) ).
cnf(t39,axiom,
sFlat33 = implies(v20,v20),
introduced(definition) ).
cnf(t98,plain,
implies(v20,v20) = sFlat33,
inference(orient,[status(thm)],[t39]) ).
cnf(t40,axiom,
sFlat34 = implies(v16,v21),
introduced(definition) ).
cnf(t109,plain,
implies(v16,v21) = sFlat34,
inference(orient,[status(thm)],[t40]) ).
cnf(t41,axiom,
sFlat35 = implies(implies(v20,v20),implies(v16,v21)),
introduced(definition) ).
cnf(t72,plain,
implies(implies(v20,v20),implies(v16,v21)) = sFlat35,
inference(orient,[status(thm)],[t41]) ).
cnf(t22333,plain,
implies(sFlat33,implies(v16,v21)) = sFlat35,
inference(step,[status(thm)],[t72,t98]) ).
cnf(t99,plain,
implies(sFlat33,implies(v16,v21)) = sFlat35,
inference(rw,[status(thm)],[t22333]) ).
cnf(t22373,plain,
implies(sFlat33,sFlat34) = sFlat35,
inference(step,[status(thm)],[t99,t109]) ).
cnf(t440,plain,
implies(sFlat33,sFlat34) = sFlat35,
inference(orient,[status(thm)],[t22373]) ).
cnf(t42,axiom,
sFlat36 = implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))),
introduced(definition) ).
cnf(t22298,plain,
sFlat36 = implies(implies(v19,v19),sFlat35),
inference(step,[status(thm)],[t42,t72]) ).
cnf(t74,plain,
implies(implies(v19,v19),sFlat35) = sFlat36,
inference(orient,[status(thm)],[t22298]) ).
cnf(t22334,plain,
implies(sFlat32,sFlat35) = sFlat36,
inference(step,[status(thm)],[t74,t100]) ).
cnf(t101,plain,
implies(sFlat32,sFlat35) = sFlat36,
inference(rw,[status(thm)],[t22334]) ).
cnf(t359,plain,
implies(sFlat32,sFlat35) = sFlat36,
inference(orient,[status(thm)],[t101]) ).
cnf(t43,axiom,
sFlat37 = implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21)))),
introduced(definition) ).
cnf(t22300,plain,
sFlat37 = implies(implies(v18,v18),implies(implies(v19,v19),sFlat35)),
inference(step,[status(thm)],[t43,t72]) ).
cnf(t22301,plain,
sFlat37 = implies(implies(v18,v18),sFlat36),
inference(step,[status(thm)],[t22300,t74]) ).
cnf(t77,plain,
implies(implies(v18,v18),sFlat36) = sFlat37,
inference(orient,[status(thm)],[t22301]) ).
cnf(t22336,plain,
implies(sFlat31,sFlat36) = sFlat37,
inference(step,[status(thm)],[t77,t104]) ).
cnf(t105,plain,
implies(sFlat31,sFlat36) = sFlat37,
inference(rw,[status(thm)],[t22336]) ).
cnf(t368,plain,
implies(sFlat31,sFlat36) = sFlat37,
inference(orient,[status(thm)],[t105]) ).
cnf(t44,axiom,
sFlat38 = implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),
introduced(definition) ).
cnf(t22306,plain,
sFlat38 = implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),sFlat35))),
inference(step,[status(thm)],[t44,t72]) ).
cnf(t22307,plain,
sFlat38 = implies(implies(v17,v17),implies(implies(v18,v18),sFlat36)),
inference(step,[status(thm)],[t22306,t74]) ).
cnf(t22308,plain,
sFlat38 = implies(implies(v17,v17),sFlat37),
inference(step,[status(thm)],[t22307,t77]) ).
cnf(t80,plain,
implies(implies(v17,v17),sFlat37) = sFlat38,
inference(orient,[status(thm)],[t22308]) ).
cnf(t22342,plain,
implies(sFlat30,sFlat37) = sFlat38,
inference(step,[status(thm)],[t80,t111]) ).
cnf(t112,plain,
implies(sFlat30,sFlat37) = sFlat38,
inference(rw,[status(thm)],[t22342]) ).
cnf(t386,plain,
implies(sFlat30,sFlat37) = sFlat38,
inference(orient,[status(thm)],[t112]) ).
cnf(t45,axiom,
sFlat39 = implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21),
introduced(definition) ).
cnf(t62,plain,
implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21) = sFlat39,
inference(orient,[status(thm)],[t45]) ).
cnf(t22297,plain,
implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),sFlat35))),v21) = sFlat39,
inference(step,[status(thm)],[t62,t72]) ).
cnf(t73,plain,
implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),sFlat35))),v21) = sFlat39,
inference(rw,[status(thm)],[t22297]) ).
cnf(t22507,plain,
implies(implies(sFlat30,implies(implies(v18,v18),implies(implies(v19,v19),sFlat35))),v21) = sFlat39,
inference(step,[status(thm)],[t73,t111]) ).
cnf(t22508,plain,
implies(implies(sFlat30,implies(sFlat31,implies(implies(v19,v19),sFlat35))),v21) = sFlat39,
inference(step,[status(thm)],[t22507,t104]) ).
cnf(t22509,plain,
implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,sFlat35))),v21) = sFlat39,
inference(step,[status(thm)],[t22508,t100]) ).
cnf(t22510,plain,
implies(implies(sFlat30,implies(sFlat31,sFlat36)),v21) = sFlat39,
inference(step,[status(thm)],[t22509,t359]) ).
cnf(t22511,plain,
implies(implies(sFlat30,sFlat37),v21) = sFlat39,
inference(step,[status(thm)],[t22510,t368]) ).
cnf(t22512,plain,
implies(sFlat38,v21) = sFlat39,
inference(step,[status(thm)],[t22511,t386]) ).
cnf(t1346,plain,
implies(sFlat38,v21) = sFlat39,
inference(orient,[status(thm)],[t22512]) ).
cnf(t46,axiom,
sFlat40 = implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),
introduced(definition) ).
cnf(t22338,plain,
sFlat40 = implies(v16,implies(implies(implies(v17,v17),implies(sFlat31,implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),
inference(step,[status(thm)],[t46,t104]) ).
cnf(t22339,plain,
sFlat40 = implies(v16,implies(implies(implies(v17,v17),implies(sFlat31,implies(sFlat32,implies(implies(v20,v20),implies(v16,v21))))),v21)),
inference(step,[status(thm)],[t22338,t100]) ).
cnf(t22340,plain,
sFlat40 = implies(v16,implies(implies(implies(v17,v17),implies(sFlat31,implies(sFlat32,implies(sFlat33,implies(v16,v21))))),v21)),
inference(step,[status(thm)],[t22339,t98]) ).
cnf(t108,plain,
implies(v16,implies(implies(implies(v17,v17),implies(sFlat31,implies(sFlat32,implies(sFlat33,implies(v16,v21))))),v21)) = sFlat40,
inference(orient,[status(thm)],[t22340]) ).
cnf(t22341,plain,
implies(v16,implies(implies(implies(v17,v17),implies(sFlat31,implies(sFlat32,implies(sFlat33,sFlat34)))),v21)) = sFlat40,
inference(step,[status(thm)],[t108,t109]) ).
cnf(t110,plain,
implies(v16,implies(implies(implies(v17,v17),implies(sFlat31,implies(sFlat32,implies(sFlat33,sFlat34)))),v21)) = sFlat40,
inference(rw,[status(thm)],[t22341]) ).
cnf(t22540,plain,
implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,implies(sFlat33,sFlat34)))),v21)) = sFlat40,
inference(step,[status(thm)],[t110,t111]) ).
cnf(t22541,plain,
implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,sFlat35))),v21)) = sFlat40,
inference(step,[status(thm)],[t22540,t440]) ).
cnf(t22542,plain,
implies(v16,implies(implies(sFlat30,implies(sFlat31,sFlat36)),v21)) = sFlat40,
inference(step,[status(thm)],[t22541,t359]) ).
cnf(t22543,plain,
implies(v16,implies(implies(sFlat30,sFlat37),v21)) = sFlat40,
inference(step,[status(thm)],[t22542,t368]) ).
cnf(t22544,plain,
implies(v16,implies(sFlat38,v21)) = sFlat40,
inference(step,[status(thm)],[t22543,t386]) ).
cnf(t22545,plain,
implies(v16,sFlat39) = sFlat40,
inference(step,[status(thm)],[t22544,t1346]) ).
cnf(t2620,plain,
implies(v16,sFlat39) = sFlat40,
inference(orient,[status(thm)],[t22545]) ).
cnf(t47,axiom,
sFlat41 = implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22),
introduced(definition) ).
cnf(t22303,plain,
sFlat41 = implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),sFlat35))),v21)),v22),
inference(step,[status(thm)],[t47,t72]) ).
cnf(t22304,plain,
sFlat41 = implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),sFlat36)),v21)),v22),
inference(step,[status(thm)],[t22303,t74]) ).
cnf(t22305,plain,
sFlat41 = implies(implies(v16,implies(implies(implies(v17,v17),sFlat37),v21)),v22),
inference(step,[status(thm)],[t22304,t77]) ).
cnf(t79,plain,
implies(implies(v16,implies(implies(implies(v17,v17),sFlat37),v21)),v22) = sFlat41,
inference(orient,[status(thm)],[t22305]) ).
cnf(t22309,plain,
implies(implies(v16,implies(sFlat38,v21)),v22) = sFlat41,
inference(step,[status(thm)],[t79,t80]) ).
cnf(t81,plain,
implies(implies(v16,implies(sFlat38,v21)),v22) = sFlat41,
inference(rw,[status(thm)],[t22309]) ).
cnf(t624,plain,
implies(implies(v16,implies(sFlat38,v21)),v22) = sFlat41,
inference(orient,[status(thm)],[t81]) ).
cnf(t22513,plain,
implies(implies(v16,sFlat39),v22) = sFlat41,
inference(step,[status(thm)],[t624,t1346]) ).
cnf(t1355,plain,
implies(implies(v16,sFlat39),v22) = sFlat41,
inference(rw,[status(thm)],[t22513]) ).
cnf(t1356,plain,
implies(implies(v16,sFlat39),v22) = sFlat41,
inference(orient,[status(thm)],[t1355]) ).
cnf(t22546,plain,
implies(sFlat40,v22) = sFlat41,
inference(step,[status(thm)],[t1356,t2620]) ).
cnf(t2631,plain,
implies(sFlat40,v22) = sFlat41,
inference(rw,[status(thm)],[t22546]) ).
cnf(t2633,plain,
implies(sFlat40,v22) = sFlat41,
inference(orient,[status(thm)],[t2631]) ).
cnf(t48,axiom,
sFlat42 = implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22)),
introduced(definition) ).
cnf(t22283,plain,
sFlat42 = implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),sFlat27),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22)),
inference(step,[status(thm)],[t48,t53]) ).
cnf(t54,plain,
implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),sFlat27),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22)) = sFlat42,
inference(orient,[status(thm)],[t22283]) ).
cnf(t22288,plain,
implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t54,t62]) ).
cnf(t63,plain,
implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(rw,[status(thm)],[t22288]) ).
cnf(t22459,plain,
implies(implies(implies(implies(sFlat11,implies(implies(v7,v8),implies(v6,v8))),sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t63,t115]) ).
cnf(t22460,plain,
implies(implies(implies(implies(sFlat11,implies(sFlat12,implies(v6,v8))),sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t22459,t117]) ).
cnf(t22461,plain,
implies(implies(implies(implies(sFlat11,implies(sFlat12,sFlat13)),sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t22460,t113]) ).
cnf(t22462,plain,
implies(implies(implies(implies(sFlat11,sFlat14),sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t22461,t458]) ).
cnf(t22463,plain,
implies(implies(implies(sFlat15,sFlat27),v15),implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t22462,t413]) ).
cnf(t22464,plain,
implies(sFlat29,implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(step,[status(thm)],[t22463,t633]) ).
cnf(t740,plain,
implies(sFlat29,implies(implies(v16,sFlat39),v22)) = sFlat42,
inference(orient,[status(thm)],[t22464]) ).
cnf(t22514,plain,
implies(sFlat29,sFlat41) = sFlat42,
inference(step,[status(thm)],[t740,t1356]) ).
cnf(t1365,plain,
implies(sFlat29,sFlat41) = sFlat42,
inference(rw,[status(thm)],[t22514]) ).
cnf(t1366,plain,
implies(sFlat29,sFlat41) = sFlat42,
inference(orient,[status(thm)],[t1365]) ).
cnf(t49,axiom,
sFlat43 = implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
introduced(definition) ).
cnf(t22317,plain,
sFlat43 = implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),sFlat5))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t49,t75]) ).
cnf(t22318,plain,
sFlat43 = implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),sFlat6)),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22317,t78]) ).
cnf(t22319,plain,
sFlat43 = implies(implies(x,implies(implies(implies(y,y),sFlat7),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22318,t86]) ).
cnf(t22320,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22319,t87]) ).
cnf(t22321,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22320,t84]) ).
cnf(t22322,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22321,t67]) ).
cnf(t22323,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(implies(implies(v11,v12),sFlat22),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22322,t69]) ).
cnf(t22324,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),
inference(step,[status(thm)],[t22323,t71]) ).
cnf(t22325,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),sFlat35))),v21)),v22))),
inference(step,[status(thm)],[t22324,t72]) ).
cnf(t22326,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),sFlat36)),v21)),v22))),
inference(step,[status(thm)],[t22325,t74]) ).
cnf(t22327,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),sFlat37),v21)),v22))),
inference(step,[status(thm)],[t22326,t77]) ).
cnf(t22328,plain,
sFlat43 = implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))),
inference(step,[status(thm)],[t22327,t80]) ).
cnf(t88,plain,
implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(orient,[status(thm)],[t22328]) ).
cnf(t22344,plain,
implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(sFlat11,sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t88,t115]) ).
cnf(t116,plain,
implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(sFlat11,sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(rw,[status(thm)],[t22344]) ).
cnf(t22559,plain,
implies(implies(x,sFlat9),implies(implies(implies(implies(sFlat11,sFlat14),implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t116,t1977]) ).
cnf(t22560,plain,
implies(implies(x,sFlat9),implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22559,t413]) ).
cnf(t22561,plain,
implies(implies(x,sFlat9),implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,sFlat24),v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22560,t611]) ).
cnf(t22562,plain,
implies(implies(x,sFlat9),implies(implies(implies(sFlat15,implies(implies(sFlat25,v14),v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22561,t570]) ).
cnf(t22563,plain,
implies(implies(x,sFlat9),implies(implies(implies(sFlat15,implies(sFlat26,v15)),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22562,t331]) ).
cnf(t22564,plain,
implies(implies(x,sFlat9),implies(implies(implies(sFlat15,sFlat27),v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22563,t322]) ).
cnf(t22565,plain,
implies(implies(x,sFlat9),implies(implies(sFlat28,v15),implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22564,t1099]) ).
cnf(t22566,plain,
implies(implies(x,sFlat9),implies(sFlat29,implies(implies(v16,implies(sFlat38,v21)),v22))) = sFlat43,
inference(step,[status(thm)],[t22565,t1110]) ).
cnf(t22567,plain,
implies(implies(x,sFlat9),implies(sFlat29,implies(implies(v16,sFlat39),v22))) = sFlat43,
inference(step,[status(thm)],[t22566,t1346]) ).
cnf(t22568,plain,
implies(implies(x,sFlat9),implies(sFlat29,implies(sFlat40,v22))) = sFlat43,
inference(step,[status(thm)],[t22567,t2620]) ).
cnf(t22569,plain,
implies(implies(x,sFlat9),implies(sFlat29,sFlat41)) = sFlat43,
inference(step,[status(thm)],[t22568,t2633]) ).
cnf(t22570,plain,
implies(implies(x,sFlat9),sFlat42) = sFlat43,
inference(step,[status(thm)],[t22569,t1366]) ).
cnf(t3233,plain,
implies(implies(x,sFlat9),sFlat42) = sFlat43,
inference(orient,[status(thm)],[t22570]) ).
cnf(t22585,plain,
implies(sFlat10,sFlat42) = sFlat43,
inference(step,[status(thm)],[t3233,t3882]) ).
cnf(t3893,plain,
implies(sFlat10,sFlat42) = sFlat43,
inference(rw,[status(thm)],[t22585]) ).
cnf(t3897,plain,
implies(sFlat10,sFlat42) = sFlat43,
inference(orient,[status(thm)],[t3893]) ).
cnf(t50,axiom,
sFlat44 = implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22),
introduced(definition) ).
cnf(t22290,plain,
sFlat44 = implies(implies(implies(x,sFlat9),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22),
inference(step,[status(thm)],[t50,t65]) ).
cnf(t22291,plain,
sFlat44 = implies(implies(implies(x,sFlat9),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),sFlat24),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22),
inference(step,[status(thm)],[t22290,t60]) ).
cnf(t22292,plain,
sFlat44 = implies(implies(implies(x,sFlat9),implies(implies(sFlat28,v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22),
inference(step,[status(thm)],[t22291,t64]) ).
cnf(t22293,plain,
sFlat44 = implies(implies(implies(x,sFlat9),implies(implies(sFlat28,v15),implies(implies(v16,sFlat39),v22))),v22),
inference(step,[status(thm)],[t22292,t62]) ).
cnf(t66,plain,
implies(implies(implies(x,sFlat9),implies(implies(sFlat28,v15),implies(implies(v16,sFlat39),v22))),v22) = sFlat44,
inference(orient,[status(thm)],[t22293]) ).
cnf(t22482,plain,
implies(implies(implies(x,sFlat9),implies(sFlat29,implies(implies(v16,sFlat39),v22))),v22) = sFlat44,
inference(step,[status(thm)],[t66,t1110]) ).
cnf(t22483,plain,
implies(implies(implies(x,sFlat9),sFlat42),v22) = sFlat44,
inference(step,[status(thm)],[t22482,t740]) ).
cnf(t1119,plain,
implies(implies(implies(x,sFlat9),sFlat42),v22) = sFlat44,
inference(rw,[status(thm)],[t22483]) ).
cnf(t1142,plain,
implies(implies(implies(x,sFlat9),sFlat42),v22) = sFlat44,
inference(orient,[status(thm)],[t1119]) ).
cnf(t22571,plain,
implies(sFlat43,v22) = sFlat44,
inference(step,[status(thm)],[t1142,t3233]) ).
cnf(t3242,plain,
implies(sFlat43,v22) = sFlat44,
inference(rw,[status(thm)],[t22571]) ).
cnf(t3243,plain,
implies(sFlat43,v22) = sFlat44,
inference(orient,[status(thm)],[t3242]) ).
cnf(f0,axiom,
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f0_nnf,plain,
! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t5,plain,
ifeq(is_a_theorem(implies(X1,X2)),true,ifeq(is_a_theorem(X1),true,is_a_theorem(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t263,plain,
ifeq(is_a_theorem(implies(X1,X2)),true,ifeq(is_a_theorem(X1),true,is_a_theorem(X2),true),true) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(f2,axiom,
is_a_theorem(implies(implies(A,implies(B,C)),implies(B,implies(A,C)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c) ).
fof(f2_nnf,plain,
! [A,B,C] : is_a_theorem(implies(implies(A,implies(B,C)),implies(B,implies(A,C)))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B,C] : is_a_theorem(implies(implies(A,implies(B,C)),implies(B,implies(A,C)))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2)))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t4,plain,
is_a_theorem(implies(implies(X1,implies(X2,X3)),implies(X2,implies(X1,X3)))) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t189,plain,
is_a_theorem(implies(implies(X1,implies(X2,X3)),implies(X2,implies(X1,X3)))) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t266,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(X1,implies(X2,X3))),true,is_a_theorem(implies(X2,implies(X1,X3))),true),true),
inference(cp,[status(thm)],[t263,t189]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t52,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t22604,plain,
true = ifeq(is_a_theorem(implies(X1,implies(X2,X3))),true,is_a_theorem(implies(X2,implies(X1,X3))),true),
inference(step,[status(thm)],[t266,t52]) ).
cnf(t5531,plain,
ifeq(is_a_theorem(implies(X1,implies(X2,X3))),true,is_a_theorem(implies(X2,implies(X1,X3))),true) = true,
inference(orient,[status(thm)],[t22604]) ).
cnf(f1,axiom,
is_a_theorem(implies(implies(A,B),implies(implies(C,A),implies(C,B)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b) ).
fof(f1_nnf,plain,
! [A,B,C] : is_a_theorem(implies(implies(A,B),implies(implies(C,A),implies(C,B)))),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] : is_a_theorem(implies(implies(A,B),implies(implies(C,A),implies(C,B)))),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t3,plain,
is_a_theorem(implies(implies(X1,X2),implies(implies(X3,X1),implies(X3,X2)))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t134,plain,
is_a_theorem(implies(implies(X1,X2),implies(implies(X3,X1),implies(X3,X2)))) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t265,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(X1,X2)),true,is_a_theorem(implies(implies(X3,X1),implies(X3,X2))),true),true),
inference(cp,[status(thm)],[t263,t134]) ).
cnf(t22594,plain,
true = ifeq(is_a_theorem(implies(X1,X2)),true,is_a_theorem(implies(implies(X3,X1),implies(X3,X2))),true),
inference(step,[status(thm)],[t265,t52]) ).
cnf(t4505,plain,
ifeq(is_a_theorem(implies(X1,X2)),true,is_a_theorem(implies(implies(X3,X1),implies(X3,X2))),true) = true,
inference(orient,[status(thm)],[t22594]) ).
cnf(f3,axiom,
is_a_theorem(implies(A,A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',i) ).
fof(f3_nnf,plain,
! [A] : is_a_theorem(implies(A,A)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A] : is_a_theorem(implies(A,A)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
is_a_theorem(implies(X0,X0)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t0,plain,
is_a_theorem(implies(X1,X1)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t125,plain,
is_a_theorem(implies(X1,X1)) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t5532,plain,
true = ifeq(true,true,is_a_theorem(implies(X1,implies(implies(X1,X2),X2))),true),
inference(cp,[status(thm)],[t5531,t125]) ).
cnf(t22611,plain,
true = is_a_theorem(implies(X1,implies(implies(X1,X2),X2))),
inference(step,[status(thm)],[t5532,t52]) ).
cnf(t6152,plain,
is_a_theorem(implies(X1,implies(implies(X1,X2),X2))) = true,
inference(orient,[status(thm)],[t22611]) ).
cnf(t6155,plain,
true = is_a_theorem(implies(sFlat40,implies(sFlat41,v22))),
inference(cp,[status(thm)],[t6152,t2633]) ).
cnf(t6247,plain,
is_a_theorem(implies(sFlat40,implies(sFlat41,v22))) = true,
inference(orient,[status(thm)],[t6155]) ).
cnf(t6248,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat40),true,is_a_theorem(implies(sFlat41,v22)),true),true),
inference(cp,[status(thm)],[t263,t6247]) ).
cnf(t23294,plain,
true = ifeq(is_a_theorem(sFlat40),true,is_a_theorem(implies(sFlat41,v22)),true),
inference(step,[status(thm)],[t6248,t52]) ).
cnf(t197,plain,
true = is_a_theorem(implies(implies(X1,sFlat34),implies(v16,implies(X1,v21)))),
inference(cp,[status(thm)],[t189,t109]) ).
cnf(t2790,plain,
is_a_theorem(implies(implies(X1,sFlat34),implies(v16,implies(X1,v21)))) = true,
inference(orient,[status(thm)],[t197]) ).
cnf(t2792,plain,
true = is_a_theorem(implies(implies(sFlat38,sFlat34),implies(v16,sFlat39))),
inference(cp,[status(thm)],[t2790,t1346]) ).
cnf(t22551,plain,
true = is_a_theorem(implies(implies(sFlat38,sFlat34),sFlat40)),
inference(step,[status(thm)],[t2792,t2620]) ).
cnf(t2805,plain,
is_a_theorem(implies(implies(sFlat38,sFlat34),sFlat40)) = true,
inference(orient,[status(thm)],[t22551]) ).
cnf(t2806,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat38,sFlat34)),true,is_a_theorem(sFlat40),true),true),
inference(cp,[status(thm)],[t263,t2805]) ).
cnf(t22552,plain,
true = ifeq(is_a_theorem(implies(sFlat38,sFlat34)),true,is_a_theorem(sFlat40),true),
inference(step,[status(thm)],[t2806,t52]) ).
cnf(t2831,plain,
ifeq(is_a_theorem(implies(sFlat38,sFlat34)),true,is_a_theorem(sFlat40),true) = true,
inference(orient,[status(thm)],[t22552]) ).
cnf(t6165,plain,
true = is_a_theorem(implies(sFlat33,implies(sFlat35,sFlat34))),
inference(cp,[status(thm)],[t6152,t440]) ).
cnf(t6441,plain,
is_a_theorem(implies(sFlat33,implies(sFlat35,sFlat34))) = true,
inference(orient,[status(thm)],[t6165]) ).
cnf(t6442,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat33),true,is_a_theorem(implies(sFlat35,sFlat34)),true),true),
inference(cp,[status(thm)],[t263,t6441]) ).
cnf(t22624,plain,
true = ifeq(is_a_theorem(sFlat33),true,is_a_theorem(implies(sFlat35,sFlat34)),true),
inference(step,[status(thm)],[t6442,t52]) ).
cnf(t133,plain,
true = is_a_theorem(sFlat33),
inference(cp,[status(thm)],[t125,t98]) ).
cnf(t319,plain,
is_a_theorem(sFlat33) = true,
inference(orient,[status(thm)],[t133]) ).
cnf(t22625,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat35,sFlat34)),true),
inference(step,[status(thm)],[t22624,t319]) ).
cnf(t22626,plain,
true = is_a_theorem(implies(sFlat35,sFlat34)),
inference(step,[status(thm)],[t22625,t52]) ).
cnf(t6456,plain,
is_a_theorem(implies(sFlat35,sFlat34)) = true,
inference(orient,[status(thm)],[t22626]) ).
cnf(t6467,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat35),implies(X1,sFlat34))),true),
inference(cp,[status(thm)],[t4505,t6456]) ).
cnf(t22836,plain,
true = is_a_theorem(implies(implies(X1,sFlat35),implies(X1,sFlat34))),
inference(step,[status(thm)],[t6467,t52]) ).
cnf(t9513,plain,
is_a_theorem(implies(implies(X1,sFlat35),implies(X1,sFlat34))) = true,
inference(orient,[status(thm)],[t22836]) ).
cnf(t9514,plain,
true = is_a_theorem(implies(sFlat36,implies(sFlat32,sFlat34))),
inference(cp,[status(thm)],[t9513,t359]) ).
cnf(t9531,plain,
is_a_theorem(implies(sFlat36,implies(sFlat32,sFlat34))) = true,
inference(orient,[status(thm)],[t9514]) ).
cnf(t9545,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat32,implies(sFlat36,sFlat34))),true),
inference(cp,[status(thm)],[t5531,t9531]) ).
cnf(t22837,plain,
true = is_a_theorem(implies(sFlat32,implies(sFlat36,sFlat34))),
inference(step,[status(thm)],[t9545,t52]) ).
cnf(t9548,plain,
is_a_theorem(implies(sFlat32,implies(sFlat36,sFlat34))) = true,
inference(orient,[status(thm)],[t22837]) ).
cnf(t9549,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat32),true,is_a_theorem(implies(sFlat36,sFlat34)),true),true),
inference(cp,[status(thm)],[t263,t9548]) ).
cnf(t22838,plain,
true = ifeq(is_a_theorem(sFlat32),true,is_a_theorem(implies(sFlat36,sFlat34)),true),
inference(step,[status(thm)],[t9549,t52]) ).
cnf(t132,plain,
true = is_a_theorem(sFlat32),
inference(cp,[status(thm)],[t125,t100]) ).
cnf(t316,plain,
is_a_theorem(sFlat32) = true,
inference(orient,[status(thm)],[t132]) ).
cnf(t22839,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat36,sFlat34)),true),
inference(step,[status(thm)],[t22838,t316]) ).
cnf(t22840,plain,
true = is_a_theorem(implies(sFlat36,sFlat34)),
inference(step,[status(thm)],[t22839,t52]) ).
cnf(t9564,plain,
is_a_theorem(implies(sFlat36,sFlat34)) = true,
inference(orient,[status(thm)],[t22840]) ).
cnf(t9577,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat36),implies(X1,sFlat34))),true),
inference(cp,[status(thm)],[t4505,t9564]) ).
cnf(t22935,plain,
true = is_a_theorem(implies(implies(X1,sFlat36),implies(X1,sFlat34))),
inference(step,[status(thm)],[t9577,t52]) ).
cnf(t10762,plain,
is_a_theorem(implies(implies(X1,sFlat36),implies(X1,sFlat34))) = true,
inference(orient,[status(thm)],[t22935]) ).
cnf(t10763,plain,
true = is_a_theorem(implies(sFlat37,implies(sFlat31,sFlat34))),
inference(cp,[status(thm)],[t10762,t368]) ).
cnf(t10781,plain,
is_a_theorem(implies(sFlat37,implies(sFlat31,sFlat34))) = true,
inference(orient,[status(thm)],[t10763]) ).
cnf(t10795,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat31,implies(sFlat37,sFlat34))),true),
inference(cp,[status(thm)],[t5531,t10781]) ).
cnf(t22936,plain,
true = is_a_theorem(implies(sFlat31,implies(sFlat37,sFlat34))),
inference(step,[status(thm)],[t10795,t52]) ).
cnf(t10813,plain,
is_a_theorem(implies(sFlat31,implies(sFlat37,sFlat34))) = true,
inference(orient,[status(thm)],[t22936]) ).
cnf(t10814,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat31),true,is_a_theorem(implies(sFlat37,sFlat34)),true),true),
inference(cp,[status(thm)],[t263,t10813]) ).
cnf(t22937,plain,
true = ifeq(is_a_theorem(sFlat31),true,is_a_theorem(implies(sFlat37,sFlat34)),true),
inference(step,[status(thm)],[t10814,t52]) ).
cnf(t130,plain,
true = is_a_theorem(sFlat31),
inference(cp,[status(thm)],[t125,t104]) ).
cnf(t310,plain,
is_a_theorem(sFlat31) = true,
inference(orient,[status(thm)],[t130]) ).
cnf(t22938,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat37,sFlat34)),true),
inference(step,[status(thm)],[t22937,t310]) ).
cnf(t22939,plain,
true = is_a_theorem(implies(sFlat37,sFlat34)),
inference(step,[status(thm)],[t22938,t52]) ).
cnf(t10829,plain,
is_a_theorem(implies(sFlat37,sFlat34)) = true,
inference(orient,[status(thm)],[t22939]) ).
cnf(t10842,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat37),implies(X1,sFlat34))),true),
inference(cp,[status(thm)],[t4505,t10829]) ).
cnf(t23079,plain,
true = is_a_theorem(implies(implies(X1,sFlat37),implies(X1,sFlat34))),
inference(step,[status(thm)],[t10842,t52]) ).
cnf(t12834,plain,
is_a_theorem(implies(implies(X1,sFlat37),implies(X1,sFlat34))) = true,
inference(orient,[status(thm)],[t23079]) ).
cnf(t12835,plain,
true = is_a_theorem(implies(sFlat38,implies(sFlat30,sFlat34))),
inference(cp,[status(thm)],[t12834,t386]) ).
cnf(t12852,plain,
is_a_theorem(implies(sFlat38,implies(sFlat30,sFlat34))) = true,
inference(orient,[status(thm)],[t12835]) ).
cnf(t12866,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat30,implies(sFlat38,sFlat34))),true),
inference(cp,[status(thm)],[t5531,t12852]) ).
cnf(t23080,plain,
true = is_a_theorem(implies(sFlat30,implies(sFlat38,sFlat34))),
inference(step,[status(thm)],[t12866,t52]) ).
cnf(t12869,plain,
is_a_theorem(implies(sFlat30,implies(sFlat38,sFlat34))) = true,
inference(orient,[status(thm)],[t23080]) ).
cnf(t12870,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat30),true,is_a_theorem(implies(sFlat38,sFlat34)),true),true),
inference(cp,[status(thm)],[t263,t12869]) ).
cnf(t23081,plain,
true = ifeq(is_a_theorem(sFlat30),true,is_a_theorem(implies(sFlat38,sFlat34)),true),
inference(step,[status(thm)],[t12870,t52]) ).
cnf(t128,plain,
true = is_a_theorem(sFlat30),
inference(cp,[status(thm)],[t125,t111]) ).
cnf(t304,plain,
is_a_theorem(sFlat30) = true,
inference(orient,[status(thm)],[t128]) ).
cnf(t23082,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat38,sFlat34)),true),
inference(step,[status(thm)],[t23081,t304]) ).
cnf(t23083,plain,
true = is_a_theorem(implies(sFlat38,sFlat34)),
inference(step,[status(thm)],[t23082,t52]) ).
cnf(t12885,plain,
is_a_theorem(implies(sFlat38,sFlat34)) = true,
inference(orient,[status(thm)],[t23083]) ).
cnf(t23085,plain,
ifeq(true,true,is_a_theorem(sFlat40),true) = true,
inference(step,[status(thm)],[t2831,t12885]) ).
cnf(t23086,plain,
is_a_theorem(sFlat40) = true,
inference(step,[status(thm)],[t23085,t52]) ).
cnf(t12900,plain,
is_a_theorem(sFlat40) = true,
inference(rw,[status(thm)],[t23086]) ).
cnf(t12901,plain,
is_a_theorem(sFlat40) = true,
inference(orient,[status(thm)],[t12900]) ).
cnf(t23295,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat41,v22)),true),
inference(step,[status(thm)],[t23294,t12901]) ).
cnf(t23296,plain,
true = is_a_theorem(implies(sFlat41,v22)),
inference(step,[status(thm)],[t23295,t52]) ).
cnf(t21804,plain,
is_a_theorem(implies(sFlat41,v22)) = true,
inference(orient,[status(thm)],[t23296]) ).
cnf(t21821,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat41),implies(X1,v22))),true),
inference(cp,[status(thm)],[t4505,t21804]) ).
cnf(t23298,plain,
true = is_a_theorem(implies(implies(X1,sFlat41),implies(X1,v22))),
inference(step,[status(thm)],[t21821,t52]) ).
cnf(t21826,plain,
is_a_theorem(implies(implies(X1,sFlat41),implies(X1,v22))) = true,
inference(orient,[status(thm)],[t23298]) ).
cnf(t21827,plain,
true = is_a_theorem(implies(sFlat42,implies(sFlat29,v22))),
inference(cp,[status(thm)],[t21826,t1366]) ).
cnf(t21851,plain,
is_a_theorem(implies(sFlat42,implies(sFlat29,v22))) = true,
inference(orient,[status(thm)],[t21827]) ).
cnf(t21868,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat29,implies(sFlat42,v22))),true),
inference(cp,[status(thm)],[t5531,t21851]) ).
cnf(t23299,plain,
true = is_a_theorem(implies(sFlat29,implies(sFlat42,v22))),
inference(step,[status(thm)],[t21868,t52]) ).
cnf(t21895,plain,
is_a_theorem(implies(sFlat29,implies(sFlat42,v22))) = true,
inference(orient,[status(thm)],[t23299]) ).
cnf(t21896,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat29),true,is_a_theorem(implies(sFlat42,v22)),true),true),
inference(cp,[status(thm)],[t263,t21895]) ).
cnf(t23300,plain,
true = ifeq(is_a_theorem(sFlat29),true,is_a_theorem(implies(sFlat42,v22)),true),
inference(step,[status(thm)],[t21896,t52]) ).
cnf(t329,plain,
true = is_a_theorem(implies(implies(X1,sFlat27),implies(sFlat26,implies(X1,v15)))),
inference(cp,[status(thm)],[t189,t322]) ).
cnf(t3478,plain,
is_a_theorem(implies(implies(X1,sFlat27),implies(sFlat26,implies(X1,v15)))) = true,
inference(orient,[status(thm)],[t329]) ).
cnf(t3479,plain,
true = is_a_theorem(implies(sFlat28,implies(sFlat26,implies(sFlat15,v15)))),
inference(cp,[status(thm)],[t3478,t1099]) ).
cnf(t3493,plain,
is_a_theorem(implies(sFlat28,implies(sFlat26,implies(sFlat15,v15)))) = true,
inference(orient,[status(thm)],[t3479]) ).
cnf(t5612,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat26,implies(sFlat28,implies(sFlat15,v15)))),true),
inference(cp,[status(thm)],[t5531,t3493]) ).
cnf(t22764,plain,
true = is_a_theorem(implies(sFlat26,implies(sFlat28,implies(sFlat15,v15)))),
inference(step,[status(thm)],[t5612,t52]) ).
cnf(t8572,plain,
is_a_theorem(implies(sFlat26,implies(sFlat28,implies(sFlat15,v15)))) = true,
inference(orient,[status(thm)],[t22764]) ).
cnf(t8573,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat26),true,is_a_theorem(implies(sFlat28,implies(sFlat15,v15))),true),true),
inference(cp,[status(thm)],[t263,t8572]) ).
cnf(t22765,plain,
true = ifeq(is_a_theorem(sFlat26),true,is_a_theorem(implies(sFlat28,implies(sFlat15,v15))),true),
inference(step,[status(thm)],[t8573,t52]) ).
cnf(t339,plain,
true = is_a_theorem(implies(implies(sFlat25,implies(X1,v14)),implies(X1,sFlat26))),
inference(cp,[status(thm)],[t189,t331]) ).
cnf(t3681,plain,
is_a_theorem(implies(implies(sFlat25,implies(X1,v14)),implies(X1,sFlat26))) = true,
inference(orient,[status(thm)],[t339]) ).
cnf(t3682,plain,
true = is_a_theorem(implies(implies(sFlat25,sFlat24),implies(sFlat23,sFlat26))),
inference(cp,[status(thm)],[t3681,t611]) ).
cnf(t3695,plain,
is_a_theorem(implies(implies(sFlat25,sFlat24),implies(sFlat23,sFlat26))) = true,
inference(orient,[status(thm)],[t3682]) ).
cnf(t5602,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat23,implies(implies(sFlat25,sFlat24),sFlat26))),true),
inference(cp,[status(thm)],[t5531,t3695]) ).
cnf(t22748,plain,
true = is_a_theorem(implies(sFlat23,implies(implies(sFlat25,sFlat24),sFlat26))),
inference(step,[status(thm)],[t5602,t52]) ).
cnf(t8440,plain,
is_a_theorem(implies(sFlat23,implies(implies(sFlat25,sFlat24),sFlat26))) = true,
inference(orient,[status(thm)],[t22748]) ).
cnf(t8441,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat23),true,is_a_theorem(implies(implies(sFlat25,sFlat24),sFlat26)),true),true),
inference(cp,[status(thm)],[t263,t8440]) ).
cnf(t22749,plain,
true = ifeq(is_a_theorem(sFlat23),true,is_a_theorem(implies(implies(sFlat25,sFlat24),sFlat26)),true),
inference(step,[status(thm)],[t8441,t52]) ).
cnf(t439,plain,
true = is_a_theorem(implies(implies(sFlat20,implies(X1,sFlat21)),implies(X1,sFlat22))),
inference(cp,[status(thm)],[t189,t431]) ).
cnf(t5484,plain,
is_a_theorem(implies(implies(sFlat20,implies(X1,sFlat21)),implies(X1,sFlat22))) = true,
inference(orient,[status(thm)],[t439]) ).
cnf(t5485,plain,
true = is_a_theorem(implies(implies(sFlat20,implies(sFlat19,sFlat21)),sFlat23)),
inference(cp,[status(thm)],[t5484,t350]) ).
cnf(t5499,plain,
is_a_theorem(implies(implies(sFlat20,implies(sFlat19,sFlat21)),sFlat23)) = true,
inference(orient,[status(thm)],[t5485]) ).
cnf(t5500,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat20,implies(sFlat19,sFlat21))),true,is_a_theorem(sFlat23),true),true),
inference(cp,[status(thm)],[t263,t5499]) ).
cnf(t22600,plain,
true = ifeq(is_a_theorem(implies(sFlat20,implies(sFlat19,sFlat21))),true,is_a_theorem(sFlat23),true),
inference(step,[status(thm)],[t5500,t52]) ).
cnf(t150,plain,
true = is_a_theorem(implies(sFlat20,implies(implies(X1,v12),implies(X1,v13)))),
inference(cp,[status(thm)],[t134,t93]) ).
cnf(t1802,plain,
is_a_theorem(implies(sFlat20,implies(implies(X1,v12),implies(X1,v13)))) = true,
inference(orient,[status(thm)],[t150]) ).
cnf(t1803,plain,
true = is_a_theorem(implies(sFlat20,implies(sFlat19,implies(v11,v13)))),
inference(cp,[status(thm)],[t1802,t96]) ).
cnf(t22527,plain,
true = is_a_theorem(implies(sFlat20,implies(sFlat19,sFlat21))),
inference(step,[status(thm)],[t1803,t95]) ).
cnf(t1818,plain,
is_a_theorem(implies(sFlat20,implies(sFlat19,sFlat21))) = true,
inference(orient,[status(thm)],[t22527]) ).
cnf(t22601,plain,
true = ifeq(true,true,is_a_theorem(sFlat23),true),
inference(step,[status(thm)],[t22600,t1818]) ).
cnf(t22602,plain,
true = is_a_theorem(sFlat23),
inference(step,[status(thm)],[t22601,t52]) ).
cnf(t5513,plain,
is_a_theorem(sFlat23) = true,
inference(orient,[status(thm)],[t22602]) ).
cnf(t22750,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(sFlat25,sFlat24),sFlat26)),true),
inference(step,[status(thm)],[t22749,t5513]) ).
cnf(t22751,plain,
true = is_a_theorem(implies(implies(sFlat25,sFlat24),sFlat26)),
inference(step,[status(thm)],[t22750,t52]) ).
cnf(t8455,plain,
is_a_theorem(implies(implies(sFlat25,sFlat24),sFlat26)) = true,
inference(orient,[status(thm)],[t22751]) ).
cnf(t8456,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat25,sFlat24)),true,is_a_theorem(sFlat26),true),true),
inference(cp,[status(thm)],[t263,t8455]) ).
cnf(t22752,plain,
true = ifeq(is_a_theorem(implies(sFlat25,sFlat24)),true,is_a_theorem(sFlat26),true),
inference(step,[status(thm)],[t8456,t52]) ).
cnf(t6162,plain,
true = is_a_theorem(implies(sFlat18,implies(sFlat25,sFlat24))),
inference(cp,[status(thm)],[t6152,t570]) ).
cnf(t6373,plain,
is_a_theorem(implies(sFlat18,implies(sFlat25,sFlat24))) = true,
inference(orient,[status(thm)],[t6162]) ).
cnf(t6374,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat18),true,is_a_theorem(implies(sFlat25,sFlat24)),true),true),
inference(cp,[status(thm)],[t263,t6373]) ).
cnf(t22618,plain,
true = ifeq(is_a_theorem(sFlat18),true,is_a_theorem(implies(sFlat25,sFlat24)),true),
inference(step,[status(thm)],[t6374,t52]) ).
cnf(f4,axiom,
is_a_theorem(implies(implies(U,implies(U,V)),implies(U,V))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',w) ).
fof(f4_nnf,plain,
! [U,V] : is_a_theorem(implies(implies(U,implies(U,V)),implies(U,V))),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [U,V] : is_a_theorem(implies(implies(U,implies(U,V)),implies(U,V))),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t2,plain,
is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2))) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t226,plain,
is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2))) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t243,plain,
true = is_a_theorem(implies(implies(v9,sFlat16),implies(v9,v10))),
inference(cp,[status(thm)],[t226,t91]) ).
cnf(t22392,plain,
true = is_a_theorem(implies(sFlat17,implies(v9,v10))),
inference(step,[status(thm)],[t243,t340]) ).
cnf(t22393,plain,
true = is_a_theorem(implies(sFlat17,sFlat16)),
inference(step,[status(thm)],[t22392,t91]) ).
cnf(t22394,plain,
true = is_a_theorem(sFlat18),
inference(step,[status(thm)],[t22393,t422]) ).
cnf(t531,plain,
is_a_theorem(sFlat18) = true,
inference(orient,[status(thm)],[t22394]) ).
cnf(t22619,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat25,sFlat24)),true),
inference(step,[status(thm)],[t22618,t531]) ).
cnf(t22620,plain,
true = is_a_theorem(implies(sFlat25,sFlat24)),
inference(step,[status(thm)],[t22619,t52]) ).
cnf(t6388,plain,
is_a_theorem(implies(sFlat25,sFlat24)) = true,
inference(orient,[status(thm)],[t22620]) ).
cnf(t22753,plain,
true = ifeq(true,true,is_a_theorem(sFlat26),true),
inference(step,[status(thm)],[t22752,t6388]) ).
cnf(t22754,plain,
true = is_a_theorem(sFlat26),
inference(step,[status(thm)],[t22753,t52]) ).
cnf(t8470,plain,
is_a_theorem(sFlat26) = true,
inference(orient,[status(thm)],[t22754]) ).
cnf(t22766,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat28,implies(sFlat15,v15))),true),
inference(step,[status(thm)],[t22765,t8470]) ).
cnf(t22767,plain,
true = is_a_theorem(implies(sFlat28,implies(sFlat15,v15))),
inference(step,[status(thm)],[t22766,t52]) ).
cnf(t8587,plain,
is_a_theorem(implies(sFlat28,implies(sFlat15,v15))) = true,
inference(orient,[status(thm)],[t22767]) ).
cnf(t8601,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat15,implies(sFlat28,v15))),true),
inference(cp,[status(thm)],[t5531,t8587]) ).
cnf(t22768,plain,
true = is_a_theorem(implies(sFlat15,implies(sFlat28,v15))),
inference(step,[status(thm)],[t8601,t52]) ).
cnf(t22769,plain,
true = is_a_theorem(implies(sFlat15,sFlat29)),
inference(step,[status(thm)],[t22768,t1110]) ).
cnf(t8604,plain,
is_a_theorem(implies(sFlat15,sFlat29)) = true,
inference(orient,[status(thm)],[t22769]) ).
cnf(t8605,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat15),true,is_a_theorem(sFlat29),true),true),
inference(cp,[status(thm)],[t263,t8604]) ).
cnf(t22770,plain,
true = ifeq(is_a_theorem(sFlat15),true,is_a_theorem(sFlat29),true),
inference(step,[status(thm)],[t8605,t52]) ).
cnf(t138,plain,
true = is_a_theorem(implies(sFlat12,implies(implies(X1,v7),implies(X1,v8)))),
inference(cp,[status(thm)],[t134,t117]) ).
cnf(t1426,plain,
is_a_theorem(implies(sFlat12,implies(implies(X1,v7),implies(X1,v8)))) = true,
inference(orient,[status(thm)],[t138]) ).
cnf(t1427,plain,
true = is_a_theorem(implies(sFlat12,implies(sFlat11,implies(v6,v8)))),
inference(cp,[status(thm)],[t1426,t115]) ).
cnf(t22519,plain,
true = is_a_theorem(implies(sFlat12,implies(sFlat11,sFlat13))),
inference(step,[status(thm)],[t1427,t113]) ).
cnf(t1442,plain,
is_a_theorem(implies(sFlat12,implies(sFlat11,sFlat13))) = true,
inference(orient,[status(thm)],[t22519]) ).
cnf(t5738,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat11,implies(sFlat12,sFlat13))),true),
inference(cp,[status(thm)],[t5531,t1442]) ).
cnf(t22605,plain,
true = is_a_theorem(implies(sFlat11,implies(sFlat12,sFlat13))),
inference(step,[status(thm)],[t5738,t52]) ).
cnf(t22606,plain,
true = is_a_theorem(implies(sFlat11,sFlat14)),
inference(step,[status(thm)],[t22605,t458]) ).
cnf(t22607,plain,
true = is_a_theorem(sFlat15),
inference(step,[status(thm)],[t22606,t413]) ).
cnf(t6106,plain,
is_a_theorem(sFlat15) = true,
inference(orient,[status(thm)],[t22607]) ).
cnf(t22771,plain,
true = ifeq(true,true,is_a_theorem(sFlat29),true),
inference(step,[status(thm)],[t22770,t6106]) ).
cnf(t22772,plain,
true = is_a_theorem(sFlat29),
inference(step,[status(thm)],[t22771,t52]) ).
cnf(t8619,plain,
is_a_theorem(sFlat29) = true,
inference(orient,[status(thm)],[t22772]) ).
cnf(t23301,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat42,v22)),true),
inference(step,[status(thm)],[t23300,t8619]) ).
cnf(t23302,plain,
true = is_a_theorem(implies(sFlat42,v22)),
inference(step,[status(thm)],[t23301,t52]) ).
cnf(t21916,plain,
is_a_theorem(implies(sFlat42,v22)) = true,
inference(orient,[status(thm)],[t23302]) ).
cnf(t21933,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat42),implies(X1,v22))),true),
inference(cp,[status(thm)],[t4505,t21916]) ).
cnf(t23316,plain,
true = is_a_theorem(implies(implies(X1,sFlat42),implies(X1,v22))),
inference(step,[status(thm)],[t21933,t52]) ).
cnf(t22194,plain,
is_a_theorem(implies(implies(X1,sFlat42),implies(X1,v22))) = true,
inference(orient,[status(thm)],[t23316]) ).
cnf(t22195,plain,
true = is_a_theorem(implies(sFlat43,implies(sFlat10,v22))),
inference(cp,[status(thm)],[t22194,t3897]) ).
cnf(t22220,plain,
is_a_theorem(implies(sFlat43,implies(sFlat10,v22))) = true,
inference(orient,[status(thm)],[t22195]) ).
cnf(t22237,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat10,implies(sFlat43,v22))),true),
inference(cp,[status(thm)],[t5531,t22220]) ).
cnf(t23317,plain,
true = is_a_theorem(implies(sFlat10,implies(sFlat43,v22))),
inference(step,[status(thm)],[t22237,t52]) ).
cnf(t23318,plain,
true = is_a_theorem(implies(sFlat10,sFlat44)),
inference(step,[status(thm)],[t23317,t3243]) ).
cnf(t22243,plain,
is_a_theorem(implies(sFlat10,sFlat44)) = true,
inference(orient,[status(thm)],[t23318]) ).
cnf(t22244,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat10),true,is_a_theorem(sFlat44),true),true),
inference(cp,[status(thm)],[t263,t22243]) ).
cnf(t23319,plain,
true = ifeq(is_a_theorem(sFlat10),true,is_a_theorem(sFlat44),true),
inference(step,[status(thm)],[t22244,t52]) ).
cnf(t190,plain,
true = is_a_theorem(implies(implies(X1,sFlat4),implies(x,implies(X1,w)))),
inference(cp,[status(thm)],[t189,t123]) ).
cnf(t2553,plain,
is_a_theorem(implies(implies(X1,sFlat4),implies(x,implies(X1,w)))) = true,
inference(orient,[status(thm)],[t190]) ).
cnf(t2555,plain,
true = is_a_theorem(implies(implies(sFlat8,sFlat4),implies(x,sFlat9))),
inference(cp,[status(thm)],[t2553,t1977]) ).
cnf(t2581,plain,
is_a_theorem(implies(implies(sFlat8,sFlat4),implies(x,sFlat9))) = true,
inference(orient,[status(thm)],[t2555]) ).
cnf(t22587,plain,
is_a_theorem(implies(implies(sFlat8,sFlat4),sFlat10)) = true,
inference(step,[status(thm)],[t2581,t3882]) ).
cnf(t3895,plain,
is_a_theorem(implies(implies(sFlat8,sFlat4),sFlat10)) = true,
inference(rw,[status(thm)],[t22587]) ).
cnf(t3932,plain,
is_a_theorem(implies(implies(sFlat8,sFlat4),sFlat10)) = true,
inference(orient,[status(thm)],[t3895]) ).
cnf(t3933,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat8,sFlat4)),true,is_a_theorem(sFlat10),true),true),
inference(cp,[status(thm)],[t263,t3932]) ).
cnf(t22592,plain,
true = ifeq(is_a_theorem(implies(sFlat8,sFlat4)),true,is_a_theorem(sFlat10),true),
inference(step,[status(thm)],[t3933,t52]) ).
cnf(t3999,plain,
ifeq(is_a_theorem(implies(sFlat8,sFlat4)),true,is_a_theorem(sFlat10),true) = true,
inference(orient,[status(thm)],[t22592]) ).
cnf(t6164,plain,
true = is_a_theorem(implies(sFlat3,implies(sFlat5,sFlat4))),
inference(cp,[status(thm)],[t6152,t449]) ).
cnf(t6414,plain,
is_a_theorem(implies(sFlat3,implies(sFlat5,sFlat4))) = true,
inference(orient,[status(thm)],[t6164]) ).
cnf(t6415,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat3),true,is_a_theorem(implies(sFlat5,sFlat4)),true),true),
inference(cp,[status(thm)],[t263,t6414]) ).
cnf(t22621,plain,
true = ifeq(is_a_theorem(sFlat3),true,is_a_theorem(implies(sFlat5,sFlat4)),true),
inference(step,[status(thm)],[t6415,t52]) ).
cnf(t131,plain,
true = is_a_theorem(sFlat3),
inference(cp,[status(thm)],[t125,t102]) ).
cnf(t313,plain,
is_a_theorem(sFlat3) = true,
inference(orient,[status(thm)],[t131]) ).
cnf(t22622,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat5,sFlat4)),true),
inference(step,[status(thm)],[t22621,t313]) ).
cnf(t22623,plain,
true = is_a_theorem(implies(sFlat5,sFlat4)),
inference(step,[status(thm)],[t22622,t52]) ).
cnf(t6429,plain,
is_a_theorem(implies(sFlat5,sFlat4)) = true,
inference(orient,[status(thm)],[t22623]) ).
cnf(t6440,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat5),implies(X1,sFlat4))),true),
inference(cp,[status(thm)],[t4505,t6429]) ).
cnf(t22830,plain,
true = is_a_theorem(implies(implies(X1,sFlat5),implies(X1,sFlat4))),
inference(step,[status(thm)],[t6440,t52]) ).
cnf(t9447,plain,
is_a_theorem(implies(implies(X1,sFlat5),implies(X1,sFlat4))) = true,
inference(orient,[status(thm)],[t22830]) ).
cnf(t9448,plain,
true = is_a_theorem(implies(sFlat6,implies(sFlat2,sFlat4))),
inference(cp,[status(thm)],[t9447,t377]) ).
cnf(t9465,plain,
is_a_theorem(implies(sFlat6,implies(sFlat2,sFlat4))) = true,
inference(orient,[status(thm)],[t9448]) ).
cnf(t9479,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat2,implies(sFlat6,sFlat4))),true),
inference(cp,[status(thm)],[t5531,t9465]) ).
cnf(t22831,plain,
true = is_a_theorem(implies(sFlat2,implies(sFlat6,sFlat4))),
inference(step,[status(thm)],[t9479,t52]) ).
cnf(t9482,plain,
is_a_theorem(implies(sFlat2,implies(sFlat6,sFlat4))) = true,
inference(orient,[status(thm)],[t22831]) ).
cnf(t9483,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat2),true,is_a_theorem(implies(sFlat6,sFlat4)),true),true),
inference(cp,[status(thm)],[t263,t9482]) ).
cnf(t22832,plain,
true = ifeq(is_a_theorem(sFlat2),true,is_a_theorem(implies(sFlat6,sFlat4)),true),
inference(step,[status(thm)],[t9483,t52]) ).
cnf(t129,plain,
true = is_a_theorem(sFlat2),
inference(cp,[status(thm)],[t125,t106]) ).
cnf(t307,plain,
is_a_theorem(sFlat2) = true,
inference(orient,[status(thm)],[t129]) ).
cnf(t22833,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat6,sFlat4)),true),
inference(step,[status(thm)],[t22832,t307]) ).
cnf(t22834,plain,
true = is_a_theorem(implies(sFlat6,sFlat4)),
inference(step,[status(thm)],[t22833,t52]) ).
cnf(t9498,plain,
is_a_theorem(implies(sFlat6,sFlat4)) = true,
inference(orient,[status(thm)],[t22834]) ).
cnf(t9511,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat6),implies(X1,sFlat4))),true),
inference(cp,[status(thm)],[t4505,t9498]) ).
cnf(t22920,plain,
true = is_a_theorem(implies(implies(X1,sFlat6),implies(X1,sFlat4))),
inference(step,[status(thm)],[t9511,t52]) ).
cnf(t10545,plain,
is_a_theorem(implies(implies(X1,sFlat6),implies(X1,sFlat4))) = true,
inference(orient,[status(thm)],[t22920]) ).
cnf(t10546,plain,
true = is_a_theorem(implies(sFlat7,implies(sFlat1,sFlat4))),
inference(cp,[status(thm)],[t10545,t395]) ).
cnf(t10564,plain,
is_a_theorem(implies(sFlat7,implies(sFlat1,sFlat4))) = true,
inference(orient,[status(thm)],[t10546]) ).
cnf(t10578,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat1,implies(sFlat7,sFlat4))),true),
inference(cp,[status(thm)],[t5531,t10564]) ).
cnf(t22921,plain,
true = is_a_theorem(implies(sFlat1,implies(sFlat7,sFlat4))),
inference(step,[status(thm)],[t10578,t52]) ).
cnf(t10596,plain,
is_a_theorem(implies(sFlat1,implies(sFlat7,sFlat4))) = true,
inference(orient,[status(thm)],[t22921]) ).
cnf(t10597,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat1),true,is_a_theorem(implies(sFlat7,sFlat4)),true),true),
inference(cp,[status(thm)],[t263,t10596]) ).
cnf(t22922,plain,
true = ifeq(is_a_theorem(sFlat1),true,is_a_theorem(implies(sFlat7,sFlat4)),true),
inference(step,[status(thm)],[t10597,t52]) ).
cnf(t127,plain,
true = is_a_theorem(sFlat1),
inference(cp,[status(thm)],[t125,t118]) ).
cnf(t301,plain,
is_a_theorem(sFlat1) = true,
inference(orient,[status(thm)],[t127]) ).
cnf(t22923,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat7,sFlat4)),true),
inference(step,[status(thm)],[t22922,t301]) ).
cnf(t22924,plain,
true = is_a_theorem(implies(sFlat7,sFlat4)),
inference(step,[status(thm)],[t22923,t52]) ).
cnf(t10612,plain,
is_a_theorem(implies(sFlat7,sFlat4)) = true,
inference(orient,[status(thm)],[t22924]) ).
cnf(t10625,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat7),implies(X1,sFlat4))),true),
inference(cp,[status(thm)],[t4505,t10612]) ).
cnf(t23060,plain,
true = is_a_theorem(implies(implies(X1,sFlat7),implies(X1,sFlat4))),
inference(step,[status(thm)],[t10625,t52]) ).
cnf(t12618,plain,
is_a_theorem(implies(implies(X1,sFlat7),implies(X1,sFlat4))) = true,
inference(orient,[status(thm)],[t23060]) ).
cnf(t12619,plain,
true = is_a_theorem(implies(sFlat8,implies(sFlat0,sFlat4))),
inference(cp,[status(thm)],[t12618,t404]) ).
cnf(t12636,plain,
is_a_theorem(implies(sFlat8,implies(sFlat0,sFlat4))) = true,
inference(orient,[status(thm)],[t12619]) ).
cnf(t12650,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat0,implies(sFlat8,sFlat4))),true),
inference(cp,[status(thm)],[t5531,t12636]) ).
cnf(t23061,plain,
true = is_a_theorem(implies(sFlat0,implies(sFlat8,sFlat4))),
inference(step,[status(thm)],[t12650,t52]) ).
cnf(t12653,plain,
is_a_theorem(implies(sFlat0,implies(sFlat8,sFlat4))) = true,
inference(orient,[status(thm)],[t23061]) ).
cnf(t12654,plain,
true = ifeq(true,true,ifeq(is_a_theorem(sFlat0),true,is_a_theorem(implies(sFlat8,sFlat4)),true),true),
inference(cp,[status(thm)],[t263,t12653]) ).
cnf(t23062,plain,
true = ifeq(is_a_theorem(sFlat0),true,is_a_theorem(implies(sFlat8,sFlat4)),true),
inference(step,[status(thm)],[t12654,t52]) ).
cnf(t126,plain,
true = is_a_theorem(sFlat0),
inference(cp,[status(thm)],[t125,t120]) ).
cnf(t298,plain,
is_a_theorem(sFlat0) = true,
inference(orient,[status(thm)],[t126]) ).
cnf(t23063,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat8,sFlat4)),true),
inference(step,[status(thm)],[t23062,t298]) ).
cnf(t23064,plain,
true = is_a_theorem(implies(sFlat8,sFlat4)),
inference(step,[status(thm)],[t23063,t52]) ).
cnf(t12669,plain,
is_a_theorem(implies(sFlat8,sFlat4)) = true,
inference(orient,[status(thm)],[t23064]) ).
cnf(t23065,plain,
ifeq(true,true,is_a_theorem(sFlat10),true) = true,
inference(step,[status(thm)],[t3999,t12669]) ).
cnf(t23066,plain,
is_a_theorem(sFlat10) = true,
inference(step,[status(thm)],[t23065,t52]) ).
cnf(t12683,plain,
is_a_theorem(sFlat10) = true,
inference(rw,[status(thm)],[t23066]) ).
cnf(t12685,plain,
is_a_theorem(sFlat10) = true,
inference(orient,[status(thm)],[t12683]) ).
cnf(t23320,plain,
true = ifeq(true,true,is_a_theorem(sFlat44),true),
inference(step,[status(thm)],[t23319,t12685]) ).
cnf(t23321,plain,
true = is_a_theorem(sFlat44),
inference(step,[status(thm)],[t23320,t52]) ).
cnf(t22264,plain,
is_a_theorem(sFlat44) = true,
inference(orient,[status(thm)],[t23321]) ).
cnf(f5,negated_conjecture,
~ is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_rezus) ).
fof(f5_nnf,plain,
~ is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
~ is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
~ is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(goal_0,negated_conjecture,
is_a_theorem(implies(implies(implies(x,implies(implies(implies(y,y),implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(g0_0,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(implies(z,z),implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[goal_0,t120]) ).
cnf(g0_1,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(sFlat1,implies(implies(u,u),implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_0,t118]) ).
cnf(g0_2,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(implies(v,v),implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_1,t106]) ).
cnf(g0_3,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(sFlat3,implies(x,w))))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_2,t102]) ).
cnf(g0_4,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,implies(sFlat3,sFlat4)))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_3,t123]) ).
cnf(g0_5,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(sFlat1,implies(sFlat2,sFlat5))),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_4,t449]) ).
cnf(g0_6,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,implies(sFlat1,sFlat6)),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_5,t377]) ).
cnf(g0_7,plain,
is_a_theorem(implies(implies(implies(x,implies(implies(sFlat0,sFlat7),w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_6,t395]) ).
cnf(g0_8,plain,
is_a_theorem(implies(implies(implies(x,implies(sFlat8,w)),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_7,t404]) ).
cnf(g0_9,plain,
is_a_theorem(implies(implies(implies(x,sFlat9),implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_8,t1977]) ).
cnf(g0_10,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(implies(implies(v6,v7),implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_9,t3882]) ).
cnf(g0_11,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(implies(sFlat11,implies(implies(v7,v8),implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_10,t115]) ).
cnf(g0_12,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(implies(sFlat11,implies(sFlat12,implies(v6,v8))),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_11,t117]) ).
cnf(g0_13,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(implies(sFlat11,implies(sFlat12,sFlat13)),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_12,t113]) ).
cnf(g0_14,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(implies(sFlat11,sFlat14),implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_13,t458]) ).
cnf(g0_15,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(implies(implies(v9,implies(v9,v10)),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_14,t413]) ).
cnf(g0_16,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(implies(implies(v9,sFlat16),implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_15,t91]) ).
cnf(g0_17,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(implies(sFlat17,implies(v9,v10)),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_16,t340]) ).
cnf(g0_18,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(implies(sFlat17,sFlat16),implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_17,t91]) ).
cnf(g0_19,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(implies(implies(v11,v12),implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_18,t422]) ).
cnf(g0_20,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(implies(sFlat19,implies(implies(v12,v13),implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_19,t96]) ).
cnf(g0_21,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(implies(sFlat19,implies(sFlat20,implies(v11,v13))),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_20,t93]) ).
cnf(g0_22,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(implies(sFlat19,implies(sFlat20,sFlat21)),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_21,t95]) ).
cnf(g0_23,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(implies(sFlat19,sFlat22),v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_22,t431]) ).
cnf(g0_24,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,implies(sFlat23,v14)),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_23,t350]) ).
cnf(g0_25,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(implies(sFlat18,sFlat24),v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_24,t611]) ).
cnf(g0_26,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(implies(sFlat25,v14),v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_25,t570]) ).
cnf(g0_27,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,implies(sFlat26,v15)),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_26,t331]) ).
cnf(g0_28,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(implies(sFlat15,sFlat27),v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_27,t322]) ).
cnf(g0_29,plain,
is_a_theorem(implies(implies(sFlat10,implies(implies(sFlat28,v15),implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_28,t1099]) ).
cnf(g0_30,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(implies(v17,v17),implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_29,t1110]) ).
cnf(g0_31,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(implies(v18,v18),implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_30,t111]) ).
cnf(g0_32,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(implies(v19,v19),implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_31,t104]) ).
cnf(g0_33,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,implies(implies(v20,v20),implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_32,t100]) ).
cnf(g0_34,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,implies(sFlat33,implies(v16,v21))))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_33,t98]) ).
cnf(g0_35,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,implies(sFlat33,sFlat34)))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_34,t109]) ).
cnf(g0_36,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(sFlat31,implies(sFlat32,sFlat35))),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_35,t440]) ).
cnf(g0_37,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,implies(sFlat31,sFlat36)),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_36,t359]) ).
cnf(g0_38,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(implies(sFlat30,sFlat37),v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_37,t368]) ).
cnf(g0_39,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,implies(sFlat38,v21)),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_38,t386]) ).
cnf(g0_40,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(implies(v16,sFlat39),v22))),v22)) != true,
inference(rw,[status(thm)],[g0_39,t1346]) ).
cnf(g0_41,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,implies(sFlat40,v22))),v22)) != true,
inference(rw,[status(thm)],[g0_40,t2620]) ).
cnf(g0_42,plain,
is_a_theorem(implies(implies(sFlat10,implies(sFlat29,sFlat41)),v22)) != true,
inference(rw,[status(thm)],[g0_41,t2633]) ).
cnf(g0_43,plain,
is_a_theorem(implies(implies(sFlat10,sFlat42),v22)) != true,
inference(rw,[status(thm)],[g0_42,t1366]) ).
cnf(g0_44,plain,
is_a_theorem(implies(sFlat43,v22)) != true,
inference(rw,[status(thm)],[g0_43,t3897]) ).
cnf(g0_45,plain,
is_a_theorem(sFlat44) != true,
inference(rw,[status(thm)],[g0_44,t3243]) ).
cnf(g0_46,plain,
true != true,
inference(rw,[status(thm)],[g0_45,t22264]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL875-1 : TPTP v9.3.1. Bugfixed v5.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 00:38:02 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 55.75/7.49 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 55.75/7.49 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------