%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n011.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:07:03 PM UTC 2026
% Result : Theorem 1.57s 6.49s
% Output : CNFRefutation 1.57s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f57ERROR: Could not build tree for root c_377ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f208,plain,
? [X0] :
( ( sP2(X0)
| sP4(X0)
| sP3(X0)
| ! [X43] :
( ~ p1(X43)
| ? [X44] :
( ~ p1(X44)
& r1(X43,X44) )
| ~ p1(X43)
| p2(X43)
| ~ r1(X0,X43) )
| ! [X41] :
( p1(X41)
| ? [X42] :
( ~ p2(X42)
& r1(X41,X42) )
| ~ p2(X41)
| ~ r1(X0,X41) ) )
& ( sP7(X0)
| sP9(X0)
| sP8(X0)
| ! [X39] :
( ~ p2(X39)
| ? [X40] :
( ~ p2(X40)
& r1(X39,X40) )
| ~ p2(X39)
| p3(X39)
| ~ r1(X0,X39) )
| ! [X37] :
( p2(X37)
| ? [X38] :
( ~ p3(X38)
& r1(X37,X38) )
| ~ p3(X37)
| ~ r1(X0,X37) ) )
& ( sP12(X0)
| sP14(X0)
| sP13(X0)
| ! [X35] :
( ~ p3(X35)
| ? [X36] :
( ~ p3(X36)
& r1(X35,X36) )
| ~ p3(X35)
| p4(X35)
| ~ r1(X0,X35) )
| ! [X33] :
( p3(X33)
| ? [X34] :
( ~ p4(X34)
& r1(X33,X34) )
| ~ p4(X33)
| ~ r1(X0,X33) ) )
& ? [X31] :
( p10(X31)
& ! [X32] :
( p10(X32)
| ~ r1(X31,X32) )
& ~ p10(X31)
& r1(X0,X31) )
& ? [X29] :
( p10(X29)
& ! [X30] :
( p10(X30)
| ~ r1(X29,X30) )
& ~ p10(X29)
& r1(X0,X29) )
& ( sP17(X0)
| sP19(X0)
| sP18(X0)
| ! [X27] :
( ~ p4(X27)
| ? [X28] :
( ~ p4(X28)
& r1(X27,X28) )
| ~ p4(X27)
| p5(X27)
| ~ r1(X0,X27) )
| ! [X25] :
( p4(X25)
| ? [X26] :
( ~ p5(X26)
& r1(X25,X26) )
| ~ p5(X25)
| ~ r1(X0,X25) ) )
& ( sP22(X0)
| sP24(X0)
| sP23(X0)
| ! [X23] :
( ~ p5(X23)
| ? [X24] :
( ~ p5(X24)
& r1(X23,X24) )
| ~ p5(X23)
| p6(X23)
| ~ r1(X0,X23) )
| ! [X21] :
( p5(X21)
| ? [X22] :
( ~ p6(X22)
& r1(X21,X22) )
| ~ p6(X21)
| ~ r1(X0,X21) ) )
& ( sP27(X0)
| sP29(X0)
| sP28(X0)
| ! [X19] :
( ~ p6(X19)
| ? [X20] :
( ~ p6(X20)
& r1(X19,X20) )
| ~ p6(X19)
| p7(X19)
| ~ r1(X0,X19) )
| ! [X17] :
( p6(X17)
| ? [X18] :
( ~ p7(X18)
& r1(X17,X18) )
| ~ p7(X17)
| ~ r1(X0,X17) ) )
& ( sP32(X0)
| sP34(X0)
| sP33(X0)
| ! [X15] :
( ~ p7(X15)
| ? [X16] :
( ~ p7(X16)
& r1(X15,X16) )
| ~ p7(X15)
| p8(X15)
| ~ r1(X0,X15) )
| ! [X13] :
( p7(X13)
| ? [X14] :
( ~ p8(X14)
& r1(X13,X14) )
| ~ p8(X13)
| ~ r1(X0,X13) ) )
& ( sP37(X0)
| sP39(X0)
| sP38(X0)
| ! [X11] :
( ~ p8(X11)
| ? [X12] :
( ~ p8(X12)
& r1(X11,X12) )
| ~ p8(X11)
| p9(X11)
| ~ r1(X0,X11) )
| ! [X9] :
( p8(X9)
| ? [X10] :
( ~ p9(X10)
& r1(X9,X10) )
| ~ p9(X9)
| ~ r1(X0,X9) ) )
& ( sP42(X0)
| sP44(X0)
| sP43(X0)
| ! [X7] :
( ~ p9(X7)
| ? [X8] :
( ~ p9(X8)
& r1(X7,X8) )
| ~ p9(X7)
| p10(X7)
| ~ r1(X0,X7) )
| ! [X5] :
( p9(X5)
| ? [X6] :
( ~ p10(X6)
& r1(X5,X6) )
| ~ p10(X5)
| ~ r1(X0,X5) ) )
& ( sP47(X0)
| sP49(X0)
| sP48(X0)
| ! [X3] :
( ~ p10(X3)
| ? [X4] :
( ~ p10(X4)
& r1(X3,X4) )
| ~ p10(X3)
| p11(X3)
| ~ r1(X0,X3) )
| ! [X1] :
( p10(X1)
| ? [X2] :
( ~ p11(X2)
& r1(X1,X2) )
| ~ p11(X1)
| ~ r1(X0,X1) ) ) ),
inference(rectify,[],[f57]) ).
fof(f209,plain,
( ( sP2(sK100)
| sP4(sK100)
| sP3(sK100)
| ! [X43] :
( ~ p1(X43)
| ( ~ p1(sK122(X43))
& r1(X43,sK122(X43)) )
| ~ p1(X43)
| p2(X43)
| ~ r1(sK100,X43) )
| ! [X41] :
( p1(X41)
| ( ~ p2(sK121(X41))
& r1(X41,sK121(X41)) )
| ~ p2(X41)
| ~ r1(sK100,X41) ) )
& ( sP7(sK100)
| sP9(sK100)
| sP8(sK100)
| ! [X39] :
( ~ p2(X39)
| ( ~ p2(sK120(X39))
& r1(X39,sK120(X39)) )
| ~ p2(X39)
| p3(X39)
| ~ r1(sK100,X39) )
| ! [X37] :
( p2(X37)
| ( ~ p3(sK119(X37))
& r1(X37,sK119(X37)) )
| ~ p3(X37)
| ~ r1(sK100,X37) ) )
& ( sP12(sK100)
| sP14(sK100)
| sP13(sK100)
| ! [X35] :
( ~ p3(X35)
| ( ~ p3(sK118(X35))
& r1(X35,sK118(X35)) )
| ~ p3(X35)
| p4(X35)
| ~ r1(sK100,X35) )
| ! [X33] :
( p3(X33)
| ( ~ p4(sK117(X33))
& r1(X33,sK117(X33)) )
| ~ p4(X33)
| ~ r1(sK100,X33) ) )
& p10(sK116)
& ! [X32] :
( p10(X32)
| ~ r1(sK116,X32) )
& ~ p10(sK116)
& r1(sK100,sK116)
& p10(sK115)
& ! [X30] :
( p10(X30)
| ~ r1(sK115,X30) )
& ~ p10(sK115)
& r1(sK100,sK115)
& ( sP17(sK100)
| sP19(sK100)
| sP18(sK100)
| ! [X27] :
( ~ p4(X27)
| ( ~ p4(sK114(X27))
& r1(X27,sK114(X27)) )
| ~ p4(X27)
| p5(X27)
| ~ r1(sK100,X27) )
| ! [X25] :
( p4(X25)
| ( ~ p5(sK113(X25))
& r1(X25,sK113(X25)) )
| ~ p5(X25)
| ~ r1(sK100,X25) ) )
& ( sP22(sK100)
| sP24(sK100)
| sP23(sK100)
| ! [X23] :
( ~ p5(X23)
| ( ~ p5(sK112(X23))
& r1(X23,sK112(X23)) )
| ~ p5(X23)
| p6(X23)
| ~ r1(sK100,X23) )
| ! [X21] :
( p5(X21)
| ( ~ p6(sK111(X21))
& r1(X21,sK111(X21)) )
| ~ p6(X21)
| ~ r1(sK100,X21) ) )
& ( sP27(sK100)
| sP29(sK100)
| sP28(sK100)
| ! [X19] :
( ~ p6(X19)
| ( ~ p6(sK110(X19))
& r1(X19,sK110(X19)) )
| ~ p6(X19)
| p7(X19)
| ~ r1(sK100,X19) )
| ! [X17] :
( p6(X17)
| ( ~ p7(sK109(X17))
& r1(X17,sK109(X17)) )
| ~ p7(X17)
| ~ r1(sK100,X17) ) )
& ( sP32(sK100)
| sP34(sK100)
| sP33(sK100)
| ! [X15] :
( ~ p7(X15)
| ( ~ p7(sK108(X15))
& r1(X15,sK108(X15)) )
| ~ p7(X15)
| p8(X15)
| ~ r1(sK100,X15) )
| ! [X13] :
( p7(X13)
| ( ~ p8(sK107(X13))
& r1(X13,sK107(X13)) )
| ~ p8(X13)
| ~ r1(sK100,X13) ) )
& ( sP37(sK100)
| sP39(sK100)
| sP38(sK100)
| ! [X11] :
( ~ p8(X11)
| ( ~ p8(sK106(X11))
& r1(X11,sK106(X11)) )
| ~ p8(X11)
| p9(X11)
| ~ r1(sK100,X11) )
| ! [X9] :
( p8(X9)
| ( ~ p9(sK105(X9))
& r1(X9,sK105(X9)) )
| ~ p9(X9)
| ~ r1(sK100,X9) ) )
& ( sP42(sK100)
| sP44(sK100)
| sP43(sK100)
| ! [X7] :
( ~ p9(X7)
| ( ~ p9(sK104(X7))
& r1(X7,sK104(X7)) )
| ~ p9(X7)
| p10(X7)
| ~ r1(sK100,X7) )
| ! [X5] :
( p9(X5)
| ( ~ p10(sK103(X5))
& r1(X5,sK103(X5)) )
| ~ p10(X5)
| ~ r1(sK100,X5) ) )
& ( sP47(sK100)
| sP49(sK100)
| sP48(sK100)
| ! [X3] :
( ~ p10(X3)
| ( ~ p10(sK102(X3))
& r1(X3,sK102(X3)) )
| ~ p10(X3)
| p11(X3)
| ~ r1(sK100,X3) )
| ! [X1] :
( p10(X1)
| ( ~ p11(sK101(X1))
& r1(X1,sK101(X1)) )
| ~ p11(X1)
| ~ r1(sK100,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK100,sK101,sK102,sK103,sK104,sK105,sK106,sK107,sK108,sK109,sK110,sK111,sK112,sK113,sK114,sK115,sK116,sK117,sK118,sK119,sK120,sK121,sK122]),skolemize(X0,sK100),skolemize(X2,sK101(X1)),skolemize(X4,sK102(X3)),skolemize(X6,sK103(X5)),skolemize(X8,sK104(X7)),skolemize(X10,sK105(X9)),skolemize(X12,sK106(X11)),skolemize(X14,sK107(X13)),skolemize(X16,sK108(X15)),skolemize(X18,sK109(X17)),skolemize(X20,sK110(X19)),skolemize(X22,sK111(X21)),skolemize(X24,sK112(X23)),skolemize(X26,sK113(X25)),skolemize(X28,sK114(X27)),skolemize(X29,sK115),skolemize(X31,sK116),skolemize(X34,sK117(X33)),skolemize(X36,sK118(X35)),skolemize(X38,sK119(X37)),skolemize(X40,sK120(X39)),skolemize(X42,sK121(X41)),skolemize(X44,sK122(X43))],[f208]) ).
fof(f502,plain,
p10(sK116),
inference(cnf_transformation,[],[f209]) ).
fof(f504,plain,
~ p10(sK116),
inference(cnf_transformation,[],[f209]) ).
tcf(c_362,negated_conjecture,
~ p10(sK116),
inference(cnf_transformation,[],[f504]) ).
tcf(c_364,negated_conjecture,
p10(sK116),
inference(cnf_transformation,[],[f502]) ).
tcf(c_377,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_362,c_364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.58 % Computer : n011.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.58 % CPULimit : 300
% 0.10/5.58 % WCLimit : 300
% 0.10/5.58 % DateTime : Wed Sep 23 23:54:20 UTC 2026
% 0.10/5.58 % CPUTime :
% 0.10/5.58 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/5.62 Running first-order theorem proving
% 0.13/5.62 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/5.63
% 0.13/5.63 % ======== iProver multi-core TPTP/SMT =========
% 0.13/5.63
% 0.13/5.63 % Detected problem language: tptp
% 0.13/5.64 % Proving...
% 1.57/6.49 % SZS status Started for theBenchmark.p
% 1.57/6.49 % SZS status Theorem for theBenchmark.p
% 1.57/6.49
% 1.57/6.49 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.57/6.49
% 1.57/6.49 % ------ iProver source info
% 1.57/6.49
% 1.57/6.49 % git: date: 2026-07-19 20:42:38 +0200
% 1.57/6.49 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.57/6.49 % git: non_committed_changes: false
% 1.57/6.49
% 1.57/6.49 % ------ Parsing...
% 1.57/6.49 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.57/6.49
% 1.57/6.49 % ------ Preprocessing...%
% 1.57/6.49
% 1.57/6.49 % SZS status Theorem for theBenchmark.p
% 1.57/6.49
% 1.57/6.49 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.57/6.49
% 1.57/6.49
%------------------------------------------------------------------------------