%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL644+1.015 : 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 : 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:07:03 PM UTC 2026
% Result : Theorem 2.06s 6.31s
% Output : CNFRefutation 2.06s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f82ERROR: Could not build tree for root c_537ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f308,plain,
? [X0] :
( ( sP2(X0)
| sP4(X0)
| sP3(X0)
| ! [X63] :
( ~ p1(X63)
| ? [X64] :
( ~ p1(X64)
& r1(X63,X64) )
| ~ p1(X63)
| p2(X63)
| ~ r1(X0,X63) )
| ! [X61] :
( p1(X61)
| ? [X62] :
( ~ p2(X62)
& r1(X61,X62) )
| ~ p2(X61)
| ~ r1(X0,X61) ) )
& ( sP7(X0)
| sP9(X0)
| sP8(X0)
| ! [X59] :
( ~ p2(X59)
| ? [X60] :
( ~ p2(X60)
& r1(X59,X60) )
| ~ p2(X59)
| p3(X59)
| ~ r1(X0,X59) )
| ! [X57] :
( p2(X57)
| ? [X58] :
( ~ p3(X58)
& r1(X57,X58) )
| ~ p3(X57)
| ~ r1(X0,X57) ) )
& ( sP12(X0)
| sP14(X0)
| sP13(X0)
| ! [X55] :
( ~ p3(X55)
| ? [X56] :
( ~ p3(X56)
& r1(X55,X56) )
| ~ p3(X55)
| p4(X55)
| ~ r1(X0,X55) )
| ! [X53] :
( p3(X53)
| ? [X54] :
( ~ p4(X54)
& r1(X53,X54) )
| ~ p4(X53)
| ~ r1(X0,X53) ) )
& ( sP17(X0)
| sP19(X0)
| sP18(X0)
| ! [X51] :
( ~ p4(X51)
| ? [X52] :
( ~ p4(X52)
& r1(X51,X52) )
| ~ p4(X51)
| p5(X51)
| ~ r1(X0,X51) )
| ! [X49] :
( p4(X49)
| ? [X50] :
( ~ p5(X50)
& r1(X49,X50) )
| ~ p5(X49)
| ~ r1(X0,X49) ) )
& ( sP22(X0)
| sP24(X0)
| sP23(X0)
| ! [X47] :
( ~ p5(X47)
| ? [X48] :
( ~ p5(X48)
& r1(X47,X48) )
| ~ p5(X47)
| p6(X47)
| ~ r1(X0,X47) )
| ! [X45] :
( p5(X45)
| ? [X46] :
( ~ p6(X46)
& r1(X45,X46) )
| ~ p6(X45)
| ~ r1(X0,X45) ) )
& ? [X43] :
( p15(X43)
& ! [X44] :
( p15(X44)
| ~ r1(X43,X44) )
& ~ p15(X43)
& r1(X0,X43) )
& ? [X41] :
( p15(X41)
& ! [X42] :
( p15(X42)
| ~ r1(X41,X42) )
& ~ p15(X41)
& r1(X0,X41) )
& ( sP27(X0)
| sP29(X0)
| sP28(X0)
| ! [X39] :
( ~ p6(X39)
| ? [X40] :
( ~ p6(X40)
& r1(X39,X40) )
| ~ p6(X39)
| p7(X39)
| ~ r1(X0,X39) )
| ! [X37] :
( p6(X37)
| ? [X38] :
( ~ p7(X38)
& r1(X37,X38) )
| ~ p7(X37)
| ~ r1(X0,X37) ) )
& ( sP32(X0)
| sP34(X0)
| sP33(X0)
| ! [X35] :
( ~ p7(X35)
| ? [X36] :
( ~ p7(X36)
& r1(X35,X36) )
| ~ p7(X35)
| p8(X35)
| ~ r1(X0,X35) )
| ! [X33] :
( p7(X33)
| ? [X34] :
( ~ p8(X34)
& r1(X33,X34) )
| ~ p8(X33)
| ~ r1(X0,X33) ) )
& ( sP37(X0)
| sP39(X0)
| sP38(X0)
| ! [X31] :
( ~ p8(X31)
| ? [X32] :
( ~ p8(X32)
& r1(X31,X32) )
| ~ p8(X31)
| p9(X31)
| ~ r1(X0,X31) )
| ! [X29] :
( p8(X29)
| ? [X30] :
( ~ p9(X30)
& r1(X29,X30) )
| ~ p9(X29)
| ~ r1(X0,X29) ) )
& ( sP42(X0)
| sP44(X0)
| sP43(X0)
| ! [X27] :
( ~ p9(X27)
| ? [X28] :
( ~ p9(X28)
& r1(X27,X28) )
| ~ p9(X27)
| p10(X27)
| ~ r1(X0,X27) )
| ! [X25] :
( p9(X25)
| ? [X26] :
( ~ p10(X26)
& r1(X25,X26) )
| ~ p10(X25)
| ~ r1(X0,X25) ) )
& ( sP47(X0)
| sP49(X0)
| sP48(X0)
| ! [X23] :
( ~ p10(X23)
| ? [X24] :
( ~ p10(X24)
& r1(X23,X24) )
| ~ p10(X23)
| p11(X23)
| ~ r1(X0,X23) )
| ! [X21] :
( p10(X21)
| ? [X22] :
( ~ p11(X22)
& r1(X21,X22) )
| ~ p11(X21)
| ~ r1(X0,X21) ) )
& ( sP52(X0)
| sP54(X0)
| sP53(X0)
| ! [X19] :
( ~ p11(X19)
| ? [X20] :
( ~ p11(X20)
& r1(X19,X20) )
| ~ p11(X19)
| p12(X19)
| ~ r1(X0,X19) )
| ! [X17] :
( p11(X17)
| ? [X18] :
( ~ p12(X18)
& r1(X17,X18) )
| ~ p12(X17)
| ~ r1(X0,X17) ) )
& ( sP57(X0)
| sP59(X0)
| sP58(X0)
| ! [X15] :
( ~ p12(X15)
| ? [X16] :
( ~ p12(X16)
& r1(X15,X16) )
| ~ p12(X15)
| p13(X15)
| ~ r1(X0,X15) )
| ! [X13] :
( p12(X13)
| ? [X14] :
( ~ p13(X14)
& r1(X13,X14) )
| ~ p13(X13)
| ~ r1(X0,X13) ) )
& ( sP62(X0)
| sP64(X0)
| sP63(X0)
| ! [X11] :
( ~ p13(X11)
| ? [X12] :
( ~ p13(X12)
& r1(X11,X12) )
| ~ p13(X11)
| p14(X11)
| ~ r1(X0,X11) )
| ! [X9] :
( p13(X9)
| ? [X10] :
( ~ p14(X10)
& r1(X9,X10) )
| ~ p14(X9)
| ~ r1(X0,X9) ) )
& ( sP67(X0)
| sP69(X0)
| sP68(X0)
| ! [X7] :
( ~ p14(X7)
| ? [X8] :
( ~ p14(X8)
& r1(X7,X8) )
| ~ p14(X7)
| p15(X7)
| ~ r1(X0,X7) )
| ! [X5] :
( p14(X5)
| ? [X6] :
( ~ p15(X6)
& r1(X5,X6) )
| ~ p15(X5)
| ~ r1(X0,X5) ) )
& ( sP72(X0)
| sP74(X0)
| sP73(X0)
| ! [X3] :
( ~ p15(X3)
| ? [X4] :
( ~ p15(X4)
& r1(X3,X4) )
| ~ p15(X3)
| p16(X3)
| ~ r1(X0,X3) )
| ! [X1] :
( p15(X1)
| ? [X2] :
( ~ p16(X2)
& r1(X1,X2) )
| ~ p16(X1)
| ~ r1(X0,X1) ) ) ),
inference(rectify,[],[f82]) ).
fof(f309,plain,
( ( sP2(sK150)
| sP4(sK150)
| sP3(sK150)
| ! [X63] :
( ~ p1(X63)
| ( ~ p1(sK182(X63))
& r1(X63,sK182(X63)) )
| ~ p1(X63)
| p2(X63)
| ~ r1(sK150,X63) )
| ! [X61] :
( p1(X61)
| ( ~ p2(sK181(X61))
& r1(X61,sK181(X61)) )
| ~ p2(X61)
| ~ r1(sK150,X61) ) )
& ( sP7(sK150)
| sP9(sK150)
| sP8(sK150)
| ! [X59] :
( ~ p2(X59)
| ( ~ p2(sK180(X59))
& r1(X59,sK180(X59)) )
| ~ p2(X59)
| p3(X59)
| ~ r1(sK150,X59) )
| ! [X57] :
( p2(X57)
| ( ~ p3(sK179(X57))
& r1(X57,sK179(X57)) )
| ~ p3(X57)
| ~ r1(sK150,X57) ) )
& ( sP12(sK150)
| sP14(sK150)
| sP13(sK150)
| ! [X55] :
( ~ p3(X55)
| ( ~ p3(sK178(X55))
& r1(X55,sK178(X55)) )
| ~ p3(X55)
| p4(X55)
| ~ r1(sK150,X55) )
| ! [X53] :
( p3(X53)
| ( ~ p4(sK177(X53))
& r1(X53,sK177(X53)) )
| ~ p4(X53)
| ~ r1(sK150,X53) ) )
& ( sP17(sK150)
| sP19(sK150)
| sP18(sK150)
| ! [X51] :
( ~ p4(X51)
| ( ~ p4(sK176(X51))
& r1(X51,sK176(X51)) )
| ~ p4(X51)
| p5(X51)
| ~ r1(sK150,X51) )
| ! [X49] :
( p4(X49)
| ( ~ p5(sK175(X49))
& r1(X49,sK175(X49)) )
| ~ p5(X49)
| ~ r1(sK150,X49) ) )
& ( sP22(sK150)
| sP24(sK150)
| sP23(sK150)
| ! [X47] :
( ~ p5(X47)
| ( ~ p5(sK174(X47))
& r1(X47,sK174(X47)) )
| ~ p5(X47)
| p6(X47)
| ~ r1(sK150,X47) )
| ! [X45] :
( p5(X45)
| ( ~ p6(sK173(X45))
& r1(X45,sK173(X45)) )
| ~ p6(X45)
| ~ r1(sK150,X45) ) )
& p15(sK172)
& ! [X44] :
( p15(X44)
| ~ r1(sK172,X44) )
& ~ p15(sK172)
& r1(sK150,sK172)
& p15(sK171)
& ! [X42] :
( p15(X42)
| ~ r1(sK171,X42) )
& ~ p15(sK171)
& r1(sK150,sK171)
& ( sP27(sK150)
| sP29(sK150)
| sP28(sK150)
| ! [X39] :
( ~ p6(X39)
| ( ~ p6(sK170(X39))
& r1(X39,sK170(X39)) )
| ~ p6(X39)
| p7(X39)
| ~ r1(sK150,X39) )
| ! [X37] :
( p6(X37)
| ( ~ p7(sK169(X37))
& r1(X37,sK169(X37)) )
| ~ p7(X37)
| ~ r1(sK150,X37) ) )
& ( sP32(sK150)
| sP34(sK150)
| sP33(sK150)
| ! [X35] :
( ~ p7(X35)
| ( ~ p7(sK168(X35))
& r1(X35,sK168(X35)) )
| ~ p7(X35)
| p8(X35)
| ~ r1(sK150,X35) )
| ! [X33] :
( p7(X33)
| ( ~ p8(sK167(X33))
& r1(X33,sK167(X33)) )
| ~ p8(X33)
| ~ r1(sK150,X33) ) )
& ( sP37(sK150)
| sP39(sK150)
| sP38(sK150)
| ! [X31] :
( ~ p8(X31)
| ( ~ p8(sK166(X31))
& r1(X31,sK166(X31)) )
| ~ p8(X31)
| p9(X31)
| ~ r1(sK150,X31) )
| ! [X29] :
( p8(X29)
| ( ~ p9(sK165(X29))
& r1(X29,sK165(X29)) )
| ~ p9(X29)
| ~ r1(sK150,X29) ) )
& ( sP42(sK150)
| sP44(sK150)
| sP43(sK150)
| ! [X27] :
( ~ p9(X27)
| ( ~ p9(sK164(X27))
& r1(X27,sK164(X27)) )
| ~ p9(X27)
| p10(X27)
| ~ r1(sK150,X27) )
| ! [X25] :
( p9(X25)
| ( ~ p10(sK163(X25))
& r1(X25,sK163(X25)) )
| ~ p10(X25)
| ~ r1(sK150,X25) ) )
& ( sP47(sK150)
| sP49(sK150)
| sP48(sK150)
| ! [X23] :
( ~ p10(X23)
| ( ~ p10(sK162(X23))
& r1(X23,sK162(X23)) )
| ~ p10(X23)
| p11(X23)
| ~ r1(sK150,X23) )
| ! [X21] :
( p10(X21)
| ( ~ p11(sK161(X21))
& r1(X21,sK161(X21)) )
| ~ p11(X21)
| ~ r1(sK150,X21) ) )
& ( sP52(sK150)
| sP54(sK150)
| sP53(sK150)
| ! [X19] :
( ~ p11(X19)
| ( ~ p11(sK160(X19))
& r1(X19,sK160(X19)) )
| ~ p11(X19)
| p12(X19)
| ~ r1(sK150,X19) )
| ! [X17] :
( p11(X17)
| ( ~ p12(sK159(X17))
& r1(X17,sK159(X17)) )
| ~ p12(X17)
| ~ r1(sK150,X17) ) )
& ( sP57(sK150)
| sP59(sK150)
| sP58(sK150)
| ! [X15] :
( ~ p12(X15)
| ( ~ p12(sK158(X15))
& r1(X15,sK158(X15)) )
| ~ p12(X15)
| p13(X15)
| ~ r1(sK150,X15) )
| ! [X13] :
( p12(X13)
| ( ~ p13(sK157(X13))
& r1(X13,sK157(X13)) )
| ~ p13(X13)
| ~ r1(sK150,X13) ) )
& ( sP62(sK150)
| sP64(sK150)
| sP63(sK150)
| ! [X11] :
( ~ p13(X11)
| ( ~ p13(sK156(X11))
& r1(X11,sK156(X11)) )
| ~ p13(X11)
| p14(X11)
| ~ r1(sK150,X11) )
| ! [X9] :
( p13(X9)
| ( ~ p14(sK155(X9))
& r1(X9,sK155(X9)) )
| ~ p14(X9)
| ~ r1(sK150,X9) ) )
& ( sP67(sK150)
| sP69(sK150)
| sP68(sK150)
| ! [X7] :
( ~ p14(X7)
| ( ~ p14(sK154(X7))
& r1(X7,sK154(X7)) )
| ~ p14(X7)
| p15(X7)
| ~ r1(sK150,X7) )
| ! [X5] :
( p14(X5)
| ( ~ p15(sK153(X5))
& r1(X5,sK153(X5)) )
| ~ p15(X5)
| ~ r1(sK150,X5) ) )
& ( sP72(sK150)
| sP74(sK150)
| sP73(sK150)
| ! [X3] :
( ~ p15(X3)
| ( ~ p15(sK152(X3))
& r1(X3,sK152(X3)) )
| ~ p15(X3)
| p16(X3)
| ~ r1(sK150,X3) )
| ! [X1] :
( p15(X1)
| ( ~ p16(sK151(X1))
& r1(X1,sK151(X1)) )
| ~ p16(X1)
| ~ r1(sK150,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK150,sK151,sK152,sK153,sK154,sK155,sK156,sK157,sK158,sK159,sK160,sK161,sK162,sK163,sK164,sK165,sK166,sK167,sK168,sK169,sK170,sK171,sK172,sK173,sK174,sK175,sK176,sK177,sK178,sK179,sK180,sK181,sK182]),skolemize(X0,sK150),skolemize(X2,sK151(X1)),skolemize(X4,sK152(X3)),skolemize(X6,sK153(X5)),skolemize(X8,sK154(X7)),skolemize(X10,sK155(X9)),skolemize(X12,sK156(X11)),skolemize(X14,sK157(X13)),skolemize(X16,sK158(X15)),skolemize(X18,sK159(X17)),skolemize(X20,sK160(X19)),skolemize(X22,sK161(X21)),skolemize(X24,sK162(X23)),skolemize(X26,sK163(X25)),skolemize(X28,sK164(X27)),skolemize(X30,sK165(X29)),skolemize(X32,sK166(X31)),skolemize(X34,sK167(X33)),skolemize(X36,sK168(X35)),skolemize(X38,sK169(X37)),skolemize(X40,sK170(X39)),skolemize(X41,sK171),skolemize(X43,sK172),skolemize(X46,sK173(X45)),skolemize(X48,sK174(X47)),skolemize(X50,sK175(X49)),skolemize(X52,sK176(X51)),skolemize(X54,sK177(X53)),skolemize(X56,sK178(X55)),skolemize(X58,sK179(X57)),skolemize(X60,sK180(X59)),skolemize(X62,sK181(X61)),skolemize(X64,sK182(X63))],[f308]) ).
fof(f750,plain,
p15(sK172),
inference(cnf_transformation,[],[f309]) ).
fof(f752,plain,
~ p15(sK172),
inference(cnf_transformation,[],[f309]) ).
tcf(c_514,negated_conjecture,
~ p15(sK172),
inference(cnf_transformation,[],[f752]) ).
tcf(c_516,negated_conjecture,
p15(sK172),
inference(cnf_transformation,[],[f750]) ).
tcf(c_537,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_514,c_516]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/5.39 % Computer : n014.cluster.edu
% 0.13/5.39 % Model : x86_64 x86_64
% 0.13/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.39 % Memory : 8046.5625MB
% 0.13/5.39 % OS : Linux 6.8.0-71-generic
% 0.13/5.39 % CPULimit : 300
% 0.13/5.39 % WCLimit : 300
% 0.13/5.39 % DateTime : Wed Sep 23 23:55:10 UTC 2026
% 0.13/5.39 % CPUTime :
% 0.13/5.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.43 Running first-order theorem proving
% 0.16/5.43 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.16/5.45
% 0.16/5.45 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.45
% 0.16/5.45 % Detected problem language: tptp
% 0.16/5.46 % Proving...
% 2.06/6.31 % SZS status Started for theBenchmark.p
% 2.06/6.31 % SZS status Theorem for theBenchmark.p
% 2.06/6.31
% 2.06/6.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.06/6.31
% 2.06/6.31 % ------ iProver source info
% 2.06/6.31
% 2.06/6.31 % git: date: 2026-07-19 20:42:38 +0200
% 2.06/6.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.06/6.31 % git: non_committed_changes: false
% 2.06/6.31
% 2.06/6.31 % ------ Parsing...
% 2.06/6.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.06/6.31
% 2.06/6.31 % ------ Preprocessing...%
% 2.06/6.31
% 2.06/6.31 % SZS status Theorem for theBenchmark.p
% 2.06/6.31
% 2.06/6.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.06/6.31
% 2.06/6.31
%------------------------------------------------------------------------------