%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/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:08:11 PM UTC 2026
% Result : Theorem 0.29s 1.07s
% Output : CNFRefutation 0.29s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f33ERROR: Could not build tree for root c_4315ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f37,plain,
! [X4] :
( ~ sP20(X4)
| ? [X92] :
( ( ~ p1(X92)
| ~ p2(X92) )
& ( p2(X92)
| p1(X92) )
& ( ~ p2(X92)
| ~ p3(X92) )
& ( p3(X92)
| p2(X92) )
& ( ~ p3(X92)
| ~ p4(X92) )
& ( p4(X92)
| p3(X92) )
& ( ~ p4(X92)
| ~ p5(X92) )
& ( p5(X92)
| p4(X92) )
& ( ~ p5(X92)
| ~ p6(X92) )
& ( p6(X92)
| p5(X92) )
& ( ~ p6(X92)
| ~ p7(X92) )
& ( p7(X92)
| p6(X92) )
& ( ~ p7(X92)
| ~ p8(X92) )
& ( p8(X92)
| p7(X92) )
& ( ~ p8(X92)
| ~ p9(X92) )
& ( p9(X92)
| p8(X92) )
& ( ~ p9(X92)
| ~ p10(X92) )
& ( p10(X92)
| p9(X92) )
& ( ~ p10(X92)
| ~ p11(X92) )
& ( p11(X92)
| p10(X92) )
& ( ~ p11(X92)
| ~ p12(X92) )
& ( p12(X92)
| p11(X92) )
& ( ~ p12(X92)
| ~ p13(X92) )
& ( p13(X92)
| p12(X92) )
& ( ~ p13(X92)
| ~ p14(X92) )
& ( p14(X92)
| p13(X92) )
& ( ~ p14(X92)
| ~ p15(X92) )
& ( p15(X92)
| p14(X92) )
& ( ~ p15(X92)
| ~ p16(X92) )
& ( p16(X92)
| p15(X92) )
& ( ~ p16(X92)
| ~ p17(X92) )
& ( p17(X92)
| p16(X92) )
& ( ~ p17(X92)
| ~ p18(X92) )
& ( p18(X92)
| p17(X92) )
& ( ~ p18(X92)
| ~ p19(X92) )
& ( p19(X92)
| p18(X92) )
& ( ~ p19(X92)
| ~ p20(X92) )
& ( p20(X92)
| p19(X92) )
& ( ~ p20(X92)
| ~ p21(X92) )
& ( p21(X92)
| p20(X92) )
& ( ~ p21(X92)
| ~ p22(X92) )
& ( p22(X92)
| p21(X92) )
& ( ~ p22(X92)
| ~ p23(X92) )
& ( p23(X92)
| p22(X92) )
& ( ~ p23(X92)
| ~ p24(X92) )
& ( p24(X92)
| p23(X92) )
& ( ~ p24(X92)
| ~ p25(X92) )
& ( p25(X92)
| p24(X92) )
& ( ~ p25(X92)
| ~ p26(X92) )
& ( p26(X92)
| p25(X92) )
& ( ~ p26(X92)
| ~ p27(X92) )
& ( p27(X92)
| p26(X92) )
& ( ~ p27(X92)
| ~ p28(X92) )
& ( p28(X92)
| p27(X92) )
& ( ~ p28(X92)
| ~ p29(X92) )
& ( p29(X92)
| p28(X92) )
& ( ~ p29(X92)
| ~ p30(X92) )
& ( p30(X92)
| p29(X92) )
& ( ~ p30(X92)
| ~ p31(X92) )
& ( p31(X92)
| p30(X92) )
& ( ~ p31(X92)
| ~ p32(X92) )
& ( p32(X92)
| p31(X92) )
& ( ~ p32(X92)
| ~ p33(X92) )
& ( p33(X92)
| p32(X92) )
& ( ~ p33(X92)
| ~ p34(X92) )
& ( p34(X92)
| p33(X92) )
& ( ~ p34(X92)
| ~ p35(X92) )
& ( p35(X92)
| p34(X92) )
& ( ~ p35(X92)
| ~ p36(X92) )
& ( p36(X92)
| p35(X92) )
& ( ~ p36(X92)
| ~ p37(X92) )
& ( p37(X92)
| p36(X92) )
& ( ~ p37(X92)
| ~ p38(X92) )
& ( p38(X92)
| p37(X92) )
& ( ~ p38(X92)
| ~ p39(X92) )
& ( p39(X92)
| p38(X92) )
& ( ~ p39(X92)
| ~ p40(X92) )
& ( p40(X92)
| p39(X92) )
& ( ~ p40(X92)
| ~ p41(X92) )
& ( p41(X92)
| p40(X92) )
& ( ~ p41(X92)
| ~ p42(X92) )
& ( p42(X92)
| p41(X92) )
& ( ~ p42(X92)
| ~ p43(X92) )
& ( p43(X92)
| p42(X92) )
& ( ~ p43(X92)
| ~ p44(X92) )
& ( p44(X92)
| p43(X92) )
& r1(X4,X92) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f38,plain,
! [X0] :
( ~ sP20(X0)
| ? [X1] :
( ( ~ p1(X1)
| ~ p2(X1) )
& ( p2(X1)
| p1(X1) )
& ( ~ p2(X1)
| ~ p3(X1) )
& ( p3(X1)
| p2(X1) )
& ( ~ p3(X1)
| ~ p4(X1) )
& ( p4(X1)
| p3(X1) )
& ( ~ p4(X1)
| ~ p5(X1) )
& ( p5(X1)
| p4(X1) )
& ( ~ p5(X1)
| ~ p6(X1) )
& ( p6(X1)
| p5(X1) )
& ( ~ p6(X1)
| ~ p7(X1) )
& ( p7(X1)
| p6(X1) )
& ( ~ p7(X1)
| ~ p8(X1) )
& ( p8(X1)
| p7(X1) )
& ( ~ p8(X1)
| ~ p9(X1) )
& ( p9(X1)
| p8(X1) )
& ( ~ p9(X1)
| ~ p10(X1) )
& ( p10(X1)
| p9(X1) )
& ( ~ p10(X1)
| ~ p11(X1) )
& ( p11(X1)
| p10(X1) )
& ( ~ p11(X1)
| ~ p12(X1) )
& ( p12(X1)
| p11(X1) )
& ( ~ p12(X1)
| ~ p13(X1) )
& ( p13(X1)
| p12(X1) )
& ( ~ p13(X1)
| ~ p14(X1) )
& ( p14(X1)
| p13(X1) )
& ( ~ p14(X1)
| ~ p15(X1) )
& ( p15(X1)
| p14(X1) )
& ( ~ p15(X1)
| ~ p16(X1) )
& ( p16(X1)
| p15(X1) )
& ( ~ p16(X1)
| ~ p17(X1) )
& ( p17(X1)
| p16(X1) )
& ( ~ p17(X1)
| ~ p18(X1) )
& ( p18(X1)
| p17(X1) )
& ( ~ p18(X1)
| ~ p19(X1) )
& ( p19(X1)
| p18(X1) )
& ( ~ p19(X1)
| ~ p20(X1) )
& ( p20(X1)
| p19(X1) )
& ( ~ p20(X1)
| ~ p21(X1) )
& ( p21(X1)
| p20(X1) )
& ( ~ p21(X1)
| ~ p22(X1) )
& ( p22(X1)
| p21(X1) )
& ( ~ p22(X1)
| ~ p23(X1) )
& ( p23(X1)
| p22(X1) )
& ( ~ p23(X1)
| ~ p24(X1) )
& ( p24(X1)
| p23(X1) )
& ( ~ p24(X1)
| ~ p25(X1) )
& ( p25(X1)
| p24(X1) )
& ( ~ p25(X1)
| ~ p26(X1) )
& ( p26(X1)
| p25(X1) )
& ( ~ p26(X1)
| ~ p27(X1) )
& ( p27(X1)
| p26(X1) )
& ( ~ p27(X1)
| ~ p28(X1) )
& ( p28(X1)
| p27(X1) )
& ( ~ p28(X1)
| ~ p29(X1) )
& ( p29(X1)
| p28(X1) )
& ( ~ p29(X1)
| ~ p30(X1) )
& ( p30(X1)
| p29(X1) )
& ( ~ p30(X1)
| ~ p31(X1) )
& ( p31(X1)
| p30(X1) )
& ( ~ p31(X1)
| ~ p32(X1) )
& ( p32(X1)
| p31(X1) )
& ( ~ p32(X1)
| ~ p33(X1) )
& ( p33(X1)
| p32(X1) )
& ( ~ p33(X1)
| ~ p34(X1) )
& ( p34(X1)
| p33(X1) )
& ( ~ p34(X1)
| ~ p35(X1) )
& ( p35(X1)
| p34(X1) )
& ( ~ p35(X1)
| ~ p36(X1) )
& ( p36(X1)
| p35(X1) )
& ( ~ p36(X1)
| ~ p37(X1) )
& ( p37(X1)
| p36(X1) )
& ( ~ p37(X1)
| ~ p38(X1) )
& ( p38(X1)
| p37(X1) )
& ( ~ p38(X1)
| ~ p39(X1) )
& ( p39(X1)
| p38(X1) )
& ( ~ p39(X1)
| ~ p40(X1) )
& ( p40(X1)
| p39(X1) )
& ( ~ p40(X1)
| ~ p41(X1) )
& ( p41(X1)
| p40(X1) )
& ( ~ p41(X1)
| ~ p42(X1) )
& ( p42(X1)
| p41(X1) )
& ( ~ p42(X1)
| ~ p43(X1) )
& ( p43(X1)
| p42(X1) )
& ( ~ p43(X1)
| ~ p44(X1) )
& ( p44(X1)
| p43(X1) )
& r1(X0,X1) ) ),
inference(rectify,[],[f37]) ).
fof(f39,plain,
! [X0] :
( ~ sP20(X0)
| ( ( ~ p1(sK24(X0))
| ~ p2(sK24(X0)) )
& ( p2(sK24(X0))
| p1(sK24(X0)) )
& ( ~ p2(sK24(X0))
| ~ p3(sK24(X0)) )
& ( p3(sK24(X0))
| p2(sK24(X0)) )
& ( ~ p3(sK24(X0))
| ~ p4(sK24(X0)) )
& ( p4(sK24(X0))
| p3(sK24(X0)) )
& ( ~ p4(sK24(X0))
| ~ p5(sK24(X0)) )
& ( p5(sK24(X0))
| p4(sK24(X0)) )
& ( ~ p5(sK24(X0))
| ~ p6(sK24(X0)) )
& ( p6(sK24(X0))
| p5(sK24(X0)) )
& ( ~ p6(sK24(X0))
| ~ p7(sK24(X0)) )
& ( p7(sK24(X0))
| p6(sK24(X0)) )
& ( ~ p7(sK24(X0))
| ~ p8(sK24(X0)) )
& ( p8(sK24(X0))
| p7(sK24(X0)) )
& ( ~ p8(sK24(X0))
| ~ p9(sK24(X0)) )
& ( p9(sK24(X0))
| p8(sK24(X0)) )
& ( ~ p9(sK24(X0))
| ~ p10(sK24(X0)) )
& ( p10(sK24(X0))
| p9(sK24(X0)) )
& ( ~ p10(sK24(X0))
| ~ p11(sK24(X0)) )
& ( p11(sK24(X0))
| p10(sK24(X0)) )
& ( ~ p11(sK24(X0))
| ~ p12(sK24(X0)) )
& ( p12(sK24(X0))
| p11(sK24(X0)) )
& ( ~ p12(sK24(X0))
| ~ p13(sK24(X0)) )
& ( p13(sK24(X0))
| p12(sK24(X0)) )
& ( ~ p13(sK24(X0))
| ~ p14(sK24(X0)) )
& ( p14(sK24(X0))
| p13(sK24(X0)) )
& ( ~ p14(sK24(X0))
| ~ p15(sK24(X0)) )
& ( p15(sK24(X0))
| p14(sK24(X0)) )
& ( ~ p15(sK24(X0))
| ~ p16(sK24(X0)) )
& ( p16(sK24(X0))
| p15(sK24(X0)) )
& ( ~ p16(sK24(X0))
| ~ p17(sK24(X0)) )
& ( p17(sK24(X0))
| p16(sK24(X0)) )
& ( ~ p17(sK24(X0))
| ~ p18(sK24(X0)) )
& ( p18(sK24(X0))
| p17(sK24(X0)) )
& ( ~ p18(sK24(X0))
| ~ p19(sK24(X0)) )
& ( p19(sK24(X0))
| p18(sK24(X0)) )
& ( ~ p19(sK24(X0))
| ~ p20(sK24(X0)) )
& ( p20(sK24(X0))
| p19(sK24(X0)) )
& ( ~ p20(sK24(X0))
| ~ p21(sK24(X0)) )
& ( p21(sK24(X0))
| p20(sK24(X0)) )
& ( ~ p21(sK24(X0))
| ~ p22(sK24(X0)) )
& ( p22(sK24(X0))
| p21(sK24(X0)) )
& ( ~ p22(sK24(X0))
| ~ p23(sK24(X0)) )
& ( p23(sK24(X0))
| p22(sK24(X0)) )
& ( ~ p23(sK24(X0))
| ~ p24(sK24(X0)) )
& ( p24(sK24(X0))
| p23(sK24(X0)) )
& ( ~ p24(sK24(X0))
| ~ p25(sK24(X0)) )
& ( p25(sK24(X0))
| p24(sK24(X0)) )
& ( ~ p25(sK24(X0))
| ~ p26(sK24(X0)) )
& ( p26(sK24(X0))
| p25(sK24(X0)) )
& ( ~ p26(sK24(X0))
| ~ p27(sK24(X0)) )
& ( p27(sK24(X0))
| p26(sK24(X0)) )
& ( ~ p27(sK24(X0))
| ~ p28(sK24(X0)) )
& ( p28(sK24(X0))
| p27(sK24(X0)) )
& ( ~ p28(sK24(X0))
| ~ p29(sK24(X0)) )
& ( p29(sK24(X0))
| p28(sK24(X0)) )
& ( ~ p29(sK24(X0))
| ~ p30(sK24(X0)) )
& ( p30(sK24(X0))
| p29(sK24(X0)) )
& ( ~ p30(sK24(X0))
| ~ p31(sK24(X0)) )
& ( p31(sK24(X0))
| p30(sK24(X0)) )
& ( ~ p31(sK24(X0))
| ~ p32(sK24(X0)) )
& ( p32(sK24(X0))
| p31(sK24(X0)) )
& ( ~ p32(sK24(X0))
| ~ p33(sK24(X0)) )
& ( p33(sK24(X0))
| p32(sK24(X0)) )
& ( ~ p33(sK24(X0))
| ~ p34(sK24(X0)) )
& ( p34(sK24(X0))
| p33(sK24(X0)) )
& ( ~ p34(sK24(X0))
| ~ p35(sK24(X0)) )
& ( p35(sK24(X0))
| p34(sK24(X0)) )
& ( ~ p35(sK24(X0))
| ~ p36(sK24(X0)) )
& ( p36(sK24(X0))
| p35(sK24(X0)) )
& ( ~ p36(sK24(X0))
| ~ p37(sK24(X0)) )
& ( p37(sK24(X0))
| p36(sK24(X0)) )
& ( ~ p37(sK24(X0))
| ~ p38(sK24(X0)) )
& ( p38(sK24(X0))
| p37(sK24(X0)) )
& ( ~ p38(sK24(X0))
| ~ p39(sK24(X0)) )
& ( p39(sK24(X0))
| p38(sK24(X0)) )
& ( ~ p39(sK24(X0))
| ~ p40(sK24(X0)) )
& ( p40(sK24(X0))
| p39(sK24(X0)) )
& ( ~ p40(sK24(X0))
| ~ p41(sK24(X0)) )
& ( p41(sK24(X0))
| p40(sK24(X0)) )
& ( ~ p41(sK24(X0))
| ~ p42(sK24(X0)) )
& ( p42(sK24(X0))
| p41(sK24(X0)) )
& ( ~ p42(sK24(X0))
| ~ p43(sK24(X0)) )
& ( p43(sK24(X0))
| p42(sK24(X0)) )
& ( ~ p43(sK24(X0))
| ~ p44(sK24(X0)) )
& ( p44(sK24(X0))
| p43(sK24(X0)) )
& r1(X0,sK24(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(X1,sK24(X0))],[f38]) ).
fof(f100,plain,
? [X0] :
( ? [X3] :
( ! [X4] :
( ( sP20(X4)
& ? [X6] :
( ~ p45(X6)
& r1(X4,X6) )
& ! [X5] :
( ( ( ~ p1(X5)
| p2(X5) )
& ( p1(X5)
| ~ p2(X5) ) )
| ~ r1(X4,X5) )
& sP21(X4) )
| ~ r1(X3,X4) )
& r1(X0,X3) )
& ? [X1] :
( ? [X2] :
( p1(X2)
& r1(X1,X2) )
& p45(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f33]) ).
fof(f101,plain,
( ! [X4] :
( ( sP20(X4)
& ~ p45(sK70(X4))
& r1(X4,sK70(X4))
& ! [X5] :
( ( ( ~ p1(X5)
| p2(X5) )
& ( p1(X5)
| ~ p2(X5) ) )
| ~ r1(X4,X5) )
& sP21(X4) )
| ~ r1(sK69,X4) )
& r1(sK66,sK69)
& p1(sK68)
& r1(sK67,sK68)
& p45(sK67)
& r1(sK66,sK67) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66,sK67,sK68,sK69,sK70]),skolemize(X0,sK66),skolemize(X1,sK67),skolemize(X2,sK68),skolemize(X3,sK69),skolemize(X6,sK70(X4))],[f100]) ).
fof(f102,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f111,plain,
! [X0] :
( ~ sP20(X0)
| ~ p1(sK24(X0))
| ~ p2(sK24(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f112,plain,
! [X0] :
( ~ sP20(X0)
| p2(sK24(X0))
| p1(sK24(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f197,plain,
! [X0] :
( ~ sP20(X0)
| r1(X0,sK24(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f338,plain,
! [X4] :
( sP20(X4)
| ~ r1(sK69,X4) ),
inference(cnf_transformation,[],[f101]) ).
fof(f341,plain,
! [X4,X5] :
( ~ p1(X5)
| p2(X5)
| ~ r1(X4,X5)
| ~ r1(sK69,X4) ),
inference(cnf_transformation,[],[f101]) ).
fof(f342,plain,
! [X4,X5] :
( p1(X5)
| ~ p2(X5)
| ~ r1(X4,X5)
| ~ r1(sK69,X4) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f102]) ).
tcf(c_58,plain,
! [X0: $i] :
( r1(X0,sK24(X0))
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_143,plain,
! [X0: $i] :
( p1(sK24(X0))
| p2(sK24(X0))
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_144,plain,
! [X0: $i] :
( ~ sP20(X0)
| ~ p1(sK24(X0))
| ~ p2(sK24(X0)) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_291,negated_conjecture,
! [X0: $i,X1: $i] :
( p1(X1)
| ~ p2(X1)
| ~ r1(sK69,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f342]) ).
tcf(c_292,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(X1)
| ~ p1(X1)
| ~ r1(sK69,X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f341]) ).
tcf(c_295,negated_conjecture,
! [X0: $i] :
( sP20(X0)
| ~ r1(sK69,X0) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_296,plain,
r1(sK69,sK69),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_297,plain,
( sP20(sK69)
| ~ r1(sK69,sK69) ),
inference(instantiation,[status(thm)],[c_295]) ).
tcf(c_339,plain,
( r1(sK69,sK24(sK69))
| ~ sP20(sK69) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_4299,plain,
! [X0: $i,X1: $i] :
( ~ sP20(X1)
| ~ p1(sK24(X1))
| ~ r1(sK69,X0)
| ~ r1(X0,sK24(X1)) ),
inference(resolution,[status(thm)],[c_292,c_144]) ).
tcf(c_4300,plain,
( ~ sP20(sK69)
| ~ p1(sK24(sK69))
| ~ r1(sK69,sK69)
| ~ r1(sK69,sK24(sK69)) ),
inference(instantiation,[status(thm)],[c_4299]) ).
tcf(c_4313,plain,
! [X0: $i,X1: $i] :
( p1(sK24(X1))
| ~ sP20(X1)
| ~ r1(sK69,X0)
| ~ r1(X0,sK24(X1)) ),
inference(resolution,[status(thm)],[c_291,c_143]) ).
tcf(c_4314,plain,
( p1(sK24(sK69))
| ~ sP20(sK69)
| ~ r1(sK69,sK69)
| ~ r1(sK69,sK24(sK69)) ),
inference(instantiation,[status(thm)],[c_4313]) ).
tcf(c_4315,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_4314,c_4300,c_339,c_297,c_296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 00:20:03 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.03/0.40 Running first-order theorem proving
% 0.03/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.41
% 0.03/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.03/0.41
% 0.03/0.41 % Detected problem language: tptp
% 0.03/0.42 % Proving...
% 0.29/1.07 % SZS status Started for theBenchmark.p
% 0.29/1.07 % SZS status Theorem for theBenchmark.p
% 0.29/1.07
% 0.29/1.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.29/1.07
% 0.29/1.07 % ------ iProver source info
% 0.29/1.07
% 0.29/1.07 % git: date: 2026-07-19 20:42:38 +0200
% 0.29/1.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.29/1.07 % git: non_committed_changes: false
% 0.29/1.07
% 0.29/1.07 % ------ Parsing...
% 0.29/1.07 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 0.29/1.07
% 0.29/1.07 % ------ Preprocessing... sf_s rm: 2 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s%
% 0.29/1.07
% 0.29/1.07 % SZS status Theorem for theBenchmark.p
% 0.29/1.07
% 0.29/1.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.29/1.07
%------------------------------------------------------------------------------