%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV125+1 : TPTP v9.3.1. Bugfixed v3.3.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 03:16:29 PM UTC 2026
% Result : Theorem 4.39s 6.31s
% Output : CNFRefutation 4.39s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f170ERROR: Could not build tree for root c_9605ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0] : leq(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',reflexivity_leq) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( leq(X1,X2)
& leq(X0,X1) )
=> leq(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',transitivity_leq) ).
fof(f7,axiom,
! [X0,X1] :
( geq(X0,X1)
<=> leq(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_geq) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f10,axiom,
! [X0,X1] :
( leq(X0,pred(X1))
<=> gt(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
fof(f39,axiom,
! [X0] : minus(X0,n1) = pred(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
fof(f40,axiom,
! [X0] : pred(succ(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',pred_succ) ).
fof(f51,axiom,
true,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',ttrue) ).
fof(f55,axiom,
gt(n1000,n588),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_1000_588) ).
fof(f57,axiom,
gt(n5,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_4) ).
fof(f58,axiom,
gt(n6,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_4) ).
fof(f59,axiom,
gt(n7,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_7_4) ).
fof(f62,axiom,
gt(n6,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_5) ).
fof(f63,axiom,
gt(n7,n5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_7_5) ).
fof(f66,axiom,
gt(n7,n6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_7_6) ).
fof(f81,axiom,
gt(n4,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_0) ).
fof(f82,axiom,
gt(n5,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_0) ).
fof(f83,axiom,
gt(n6,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_0) ).
fof(f85,axiom,
gt(n1,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_1_0) ).
fof(f86,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_0) ).
fof(f88,axiom,
gt(n3,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_0) ).
fof(f90,axiom,
gt(n4,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_1) ).
fof(f91,axiom,
gt(n5,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_1) ).
fof(f92,axiom,
gt(n6,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_1) ).
fof(f93,axiom,
gt(n7,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_7_1) ).
fof(f96,axiom,
gt(n3,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_1) ).
fof(f98,axiom,
gt(n4,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_2) ).
fof(f99,axiom,
gt(n5,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_2) ).
fof(f100,axiom,
gt(n6,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_2) ).
fof(f101,axiom,
gt(n7,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_7_2) ).
fof(f103,axiom,
gt(n3,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_3_2) ).
fof(f105,axiom,
gt(n4,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_4_3) ).
fof(f106,axiom,
gt(n5,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_5_3) ).
fof(f107,axiom,
gt(n6,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_6_3) ).
fof(f108,axiom,
gt(n7,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_7_3) ).
fof(f117,axiom,
succ(succ(succ(succ(n0)))) = n4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_4) ).
fof(f118,axiom,
succ(succ(succ(succ(succ(n0))))) = n5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_5) ).
fof(f119,axiom,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_6) ).
fof(f120,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_1) ).
fof(f121,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_2) ).
fof(f122,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_3) ).
fof(f124,plain,
! [X0,X1] :
( geq(X0,X1)
=> leq(X1,X0) ),
inference(unused_predicate_definition_removal,[],[f7]) ).
fof(f135,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f136,plain,
! [X0,X1,X2] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f137,plain,
! [X0,X1,X2] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(flattening,[],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( ~ geq(X0,X1)
| leq(X1,X0) ),
inference(ennf_transformation,[],[f124]) ).
fof(f171,plain,
( ~ sP17
| ( leq(pv5,n588)
& leq(n0,pv5)
& ~ true ) ),
inference(nnf_transformation,[],[f169]) ).
fof(f172,plain,
( ~ sP16
| ( leq(pv5,n588)
& leq(n0,pv5)
& sP7 ) ),
inference(nnf_transformation,[],[f168]) ).
fof(f173,plain,
( ~ sP15
| ( leq(pv5,n588)
& leq(n0,pv5)
& ( ~ leq(pv5,n588)
| ~ leq(n0,pv5) ) ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f174,plain,
( ~ sP14
| ( leq(pv23,minus(n6,n1))
& leq(n0,pv23)
& leq(n0,a_select2(sigma,pv23))
& ~ true ) ),
inference(nnf_transformation,[],[f166]) ).
fof(f175,plain,
( ~ sP13
| ( leq(pv21,minus(n6,n1))
& leq(pv5,n588)
& leq(n0,pv21)
& leq(n0,pv5)
& ( ~ leq(pv21,minus(n6,n1))
| ~ leq(pv21,n5)
| ~ leq(pv5,n588)
| ~ leq(n0,pv21)
| ~ leq(n0,pv5)
| ~ leq(n0,n0) ) ) ),
inference(nnf_transformation,[],[f165]) ).
fof(f176,plain,
( ~ sP12
| ( leq(pv31,minus(n6,n1))
& leq(pv5,n588)
& leq(n0,pv31)
& leq(n0,pv5)
& ( ~ leq(pv31,minus(n6,n1))
| ~ leq(pv5,n588)
| ~ leq(n0,pv31)
| ~ leq(n0,pv5) ) ) ),
inference(nnf_transformation,[],[f164]) ).
fof(f177,plain,
( ~ sP11
| ( leq(pv31,minus(n6,n1))
& leq(pv5,n588)
& leq(n0,pv31)
& leq(n0,pv5)
& ( ~ leq(pv5,n588)
| ~ leq(n0,pv5) ) ) ),
inference(nnf_transformation,[],[f163]) ).
fof(f178,plain,
( ~ sP10
| ( geq(minus(n6,n1),n0)
& geq(minus(n6,n1),n0)
& geq(minus(n1000,n1),n0)
& geq(minus(n4,n1),n0)
& ~ true ) ),
inference(nnf_transformation,[],[f162]) ).
fof(f179,plain,
( ~ sP9
| ( leq(pv32,minus(n6,n1))
& leq(pv31,minus(n6,n1))
& leq(pv5,n588)
& leq(n0,pv32)
& leq(n0,pv31)
& leq(n0,pv5)
& sP8 ) ),
inference(nnf_transformation,[],[f161]) ).
fof(f183,plain,
( ~ sP5
| ( gt(pv5,n0)
& ( sP3
| ( ~ gt(pv5,n0)
& ( ( gt(pv5,n0)
& ( ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ) )
| ( ~ gt(pv5,n0)
& ( ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ) ) ) )
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ) ) ),
inference(nnf_transformation,[],[f157]) ).
fof(f186,plain,
( ~ sP2
| ( gt(pv5,n0)
& ( sP0
| ( ~ gt(pv5,n0)
& ( ( gt(pv5,n0)
& ( ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ) )
| ( ~ gt(pv5,n0)
& ( ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ) ) ) )
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ) ) ),
inference(nnf_transformation,[],[f154]) ).
fof(f191,plain,
! [X0,X1] :
( ( ~ leq(X0,pred(X1))
| gt(X1,X0) )
& ( ~ gt(X1,X0)
| leq(X0,pred(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f194,plain,
( ~ sP17
| ~ true ),
inference(cnf_transformation,[],[f171]) ).
fof(f195,plain,
( ~ sP16
| leq(pv5,n588) ),
inference(cnf_transformation,[],[f172]) ).
fof(f196,plain,
( ~ sP16
| leq(n0,pv5) ),
inference(cnf_transformation,[],[f172]) ).
fof(f197,plain,
( ~ sP16
| sP7 ),
inference(cnf_transformation,[],[f172]) ).
fof(f198,plain,
( ~ sP15
| leq(pv5,n588) ),
inference(cnf_transformation,[],[f173]) ).
fof(f199,plain,
( ~ sP15
| leq(n0,pv5) ),
inference(cnf_transformation,[],[f173]) ).
fof(f200,plain,
( ~ sP15
| ~ leq(pv5,n588)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[],[f173]) ).
fof(f204,plain,
( ~ sP14
| ~ true ),
inference(cnf_transformation,[],[f174]) ).
fof(f205,plain,
( ~ sP13
| leq(pv21,minus(n6,n1)) ),
inference(cnf_transformation,[],[f175]) ).
fof(f206,plain,
( ~ sP13
| leq(pv5,n588) ),
inference(cnf_transformation,[],[f175]) ).
fof(f207,plain,
( ~ sP13
| leq(n0,pv21) ),
inference(cnf_transformation,[],[f175]) ).
fof(f208,plain,
( ~ sP13
| leq(n0,pv5) ),
inference(cnf_transformation,[],[f175]) ).
fof(f209,plain,
( ~ sP13
| ~ leq(pv21,minus(n6,n1))
| ~ leq(pv21,n5)
| ~ leq(pv5,n588)
| ~ leq(n0,pv21)
| ~ leq(n0,pv5)
| ~ leq(n0,n0) ),
inference(cnf_transformation,[],[f175]) ).
fof(f210,plain,
( ~ sP12
| leq(pv31,minus(n6,n1)) ),
inference(cnf_transformation,[],[f176]) ).
fof(f211,plain,
( ~ sP12
| leq(pv5,n588) ),
inference(cnf_transformation,[],[f176]) ).
fof(f212,plain,
( ~ sP12
| leq(n0,pv31) ),
inference(cnf_transformation,[],[f176]) ).
fof(f213,plain,
( ~ sP12
| leq(n0,pv5) ),
inference(cnf_transformation,[],[f176]) ).
fof(f214,plain,
( ~ sP12
| ~ leq(pv31,minus(n6,n1))
| ~ leq(pv5,n588)
| ~ leq(n0,pv31)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[],[f176]) ).
fof(f216,plain,
( ~ sP11
| leq(pv5,n588) ),
inference(cnf_transformation,[],[f177]) ).
fof(f218,plain,
( ~ sP11
| leq(n0,pv5) ),
inference(cnf_transformation,[],[f177]) ).
fof(f219,plain,
( ~ sP11
| ~ leq(pv5,n588)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[],[f177]) ).
fof(f222,plain,
( ~ sP10
| geq(minus(n1000,n1),n0) ),
inference(cnf_transformation,[],[f178]) ).
fof(f224,plain,
( ~ sP10
| ~ true ),
inference(cnf_transformation,[],[f178]) ).
fof(f225,plain,
( ~ sP9
| leq(pv32,minus(n6,n1)) ),
inference(cnf_transformation,[],[f179]) ).
fof(f226,plain,
( ~ sP9
| leq(pv31,minus(n6,n1)) ),
inference(cnf_transformation,[],[f179]) ).
fof(f227,plain,
( ~ sP9
| leq(pv5,n588) ),
inference(cnf_transformation,[],[f179]) ).
fof(f228,plain,
( ~ sP9
| leq(n0,pv32) ),
inference(cnf_transformation,[],[f179]) ).
fof(f229,plain,
( ~ sP9
| leq(n0,pv31) ),
inference(cnf_transformation,[],[f179]) ).
fof(f230,plain,
( ~ sP9
| leq(n0,pv5) ),
inference(cnf_transformation,[],[f179]) ).
fof(f231,plain,
( ~ sP9
| sP8 ),
inference(cnf_transformation,[],[f179]) ).
fof(f250,plain,
( ~ sP5
| gt(pv5,n0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f251,plain,
( ~ sP5
| sP3
| ~ gt(pv5,n0)
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f266,plain,
( ~ sP2
| gt(pv5,n0) ),
inference(cnf_transformation,[],[f186]) ).
fof(f267,plain,
( ~ sP2
| sP0
| ~ gt(pv5,n0)
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0) ),
inference(cnf_transformation,[],[f186]) ).
fof(f282,plain,
geq(minus(n1000,n1),n0),
inference(cnf_transformation,[],[f170]) ).
fof(f289,plain,
( sP10
| sP14
| sP15
| sP16
| sP17
| sP11
| sP12
| sP9
| sP13
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ true ),
inference(cnf_transformation,[],[f170]) ).
fof(f301,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f302,plain,
! [X2,X0,X1] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(cnf_transformation,[],[f137]) ).
fof(f303,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f304,plain,
! [X0,X1] :
( ~ geq(X0,X1)
| leq(X1,X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f305,plain,
true,
inference(cnf_transformation,[],[f51]) ).
fof(f306,plain,
n1 = succ(n0),
inference(cnf_transformation,[],[f120]) ).
fof(f312,plain,
gt(n3,n1),
inference(cnf_transformation,[],[f96]) ).
fof(f314,plain,
gt(n5,n1),
inference(cnf_transformation,[],[f91]) ).
fof(f315,plain,
gt(n4,n1),
inference(cnf_transformation,[],[f90]) ).
fof(f316,plain,
gt(n1,n0),
inference(cnf_transformation,[],[f85]) ).
fof(f317,plain,
n2 = succ(succ(n0)),
inference(cnf_transformation,[],[f121]) ).
fof(f319,plain,
gt(n3,n2),
inference(cnf_transformation,[],[f103]) ).
fof(f320,plain,
gt(n6,n2),
inference(cnf_transformation,[],[f100]) ).
fof(f321,plain,
gt(n5,n2),
inference(cnf_transformation,[],[f99]) ).
fof(f322,plain,
gt(n4,n2),
inference(cnf_transformation,[],[f98]) ).
fof(f323,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f325,plain,
n3 = succ(succ(succ(n0))),
inference(cnf_transformation,[],[f122]) ).
fof(f326,plain,
gt(n6,n3),
inference(cnf_transformation,[],[f107]) ).
fof(f327,plain,
gt(n5,n3),
inference(cnf_transformation,[],[f106]) ).
fof(f328,plain,
gt(n4,n3),
inference(cnf_transformation,[],[f105]) ).
fof(f329,plain,
gt(n3,n0),
inference(cnf_transformation,[],[f88]) ).
fof(f331,plain,
n4 = succ(succ(succ(succ(n0)))),
inference(cnf_transformation,[],[f117]) ).
fof(f332,plain,
gt(n4,n0),
inference(cnf_transformation,[],[f81]) ).
fof(f334,plain,
gt(n6,n4),
inference(cnf_transformation,[],[f58]) ).
fof(f335,plain,
gt(n5,n4),
inference(cnf_transformation,[],[f57]) ).
fof(f336,plain,
n5 = succ(succ(succ(succ(succ(n0))))),
inference(cnf_transformation,[],[f118]) ).
fof(f337,plain,
gt(n5,n0),
inference(cnf_transformation,[],[f82]) ).
fof(f340,plain,
gt(n7,n5),
inference(cnf_transformation,[],[f63]) ).
fof(f341,plain,
gt(n6,n5),
inference(cnf_transformation,[],[f62]) ).
fof(f344,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[],[f39]) ).
fof(f353,plain,
gt(n1000,n588),
inference(cnf_transformation,[],[f55]) ).
fof(f354,plain,
gt(n7,n3),
inference(cnf_transformation,[],[f108]) ).
fof(f355,plain,
gt(n7,n2),
inference(cnf_transformation,[],[f101]) ).
fof(f356,plain,
gt(n7,n1),
inference(cnf_transformation,[],[f93]) ).
fof(f360,plain,
gt(n7,n6),
inference(cnf_transformation,[],[f66]) ).
fof(f361,plain,
gt(n7,n4),
inference(cnf_transformation,[],[f59]) ).
fof(f362,plain,
n6 = succ(succ(succ(succ(succ(succ(n0)))))),
inference(cnf_transformation,[],[f119]) ).
fof(f363,plain,
gt(n6,n1),
inference(cnf_transformation,[],[f92]) ).
fof(f364,plain,
gt(n6,n0),
inference(cnf_transformation,[],[f83]) ).
fof(f378,plain,
! [X0] : pred(succ(X0)) = X0,
inference(cnf_transformation,[],[f40]) ).
fof(f380,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[],[f191]) ).
fof(f382,plain,
! [X0] : minus(succ(X0),n1) = X0,
inference(definition_unfolding,[],[f378,f344]) ).
fof(f383,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,minus(X1,n1)) ),
inference(definition_unfolding,[],[f380,f344]) ).
tcf(c_49,plain,
( ~ sP17
| ~ true ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_52,plain,
( sP7
| ~ sP16 ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_53,plain,
( leq(n0,pv5)
| ~ sP16 ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_54,plain,
( leq(pv5,n588)
| ~ sP16 ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_55,plain,
( ~ sP15
| ~ leq(pv5,n588)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_56,plain,
( leq(n0,pv5)
| ~ sP15 ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_57,plain,
( leq(pv5,n588)
| ~ sP15 ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_58,plain,
( ~ sP14
| ~ true ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_62,plain,
( ~ sP13
| ~ leq(pv21,n5)
| ~ leq(pv5,n588)
| ~ leq(n0,pv21)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(pv21,minus(n6,n1)) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_63,plain,
( leq(n0,pv5)
| ~ sP13 ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_64,plain,
( leq(n0,pv21)
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_65,plain,
( leq(pv5,n588)
| ~ sP13 ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_66,plain,
( leq(pv21,minus(n6,n1))
| ~ sP13 ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_67,plain,
( ~ sP12
| ~ leq(pv5,n588)
| ~ leq(n0,pv31)
| ~ leq(n0,pv5)
| ~ leq(pv31,minus(n6,n1)) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_68,plain,
( leq(n0,pv5)
| ~ sP12 ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_69,plain,
( leq(n0,pv31)
| ~ sP12 ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_70,plain,
( leq(pv5,n588)
| ~ sP12 ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_71,plain,
( leq(pv31,minus(n6,n1))
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_72,plain,
( ~ sP11
| ~ leq(pv5,n588)
| ~ leq(n0,pv5) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_73,plain,
( leq(n0,pv5)
| ~ sP11 ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_75,plain,
( leq(pv5,n588)
| ~ sP11 ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_77,plain,
( ~ sP10
| ~ true ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_79,plain,
( geq(minus(n1000,n1),n0)
| ~ sP10 ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_82,plain,
( sP8
| ~ sP9 ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_83,plain,
( leq(n0,pv5)
| ~ sP9 ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_84,plain,
( leq(n0,pv31)
| ~ sP9 ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_85,plain,
( leq(n0,pv32)
| ~ sP9 ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_86,plain,
( leq(pv5,n588)
| ~ sP9 ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_87,plain,
( leq(pv31,minus(n6,n1))
| ~ sP9 ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_88,plain,
( leq(pv32,minus(n6,n1))
| ~ sP9 ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_89,plain,
( ~ sP8
| ~ leq(pv5,n588)
| ~ leq(n0,pv32)
| ~ leq(n0,pv31)
| ~ leq(n0,pv5)
| ~ leq(pv32,minus(n6,n1))
| ~ leq(pv31,minus(n6,n1)) ),
inference(cnf_transformation,[],[f385]) ).
tcf(c_92,plain,
( sP6
| sP5
| sP4
| ~ sP7
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f386]) ).
tcf(c_93,plain,
( sP6
| sP5
| sP4
| gt(pv5,n0)
| ~ sP7
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f387]) ).
tcf(c_98,plain,
( sP2
| sP1
| ~ sP6
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f389]) ).
tcf(c_107,plain,
( sP3
| ~ sP5
| ~ gt(pv5,n0)
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_108,plain,
( gt(pv5,n0)
| ~ sP5 ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_109,plain,
( ~ sP4
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f395]) ).
tcf(c_113,plain,
( ~ sP3
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f398]) ).
tcf(c_120,plain,
( sP0
| ~ sP2
| ~ gt(pv5,n0)
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_121,plain,
( gt(pv5,n0)
| ~ sP2 ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_122,plain,
( ~ sP1
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f404]) ).
tcf(c_126,plain,
( ~ sP0
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f407]) ).
tcf(c_130,negated_conjecture,
( sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| ~ true
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,n0)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_136,negated_conjecture,
geq(minus(n1000,n1),n0),
inference(cnf_transformation,[],[f282]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( leq(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i] :
( leq(X0,X2)
| ~ leq(X1,X2)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_150,plain,
! [X0: $i] : leq(X0,X0),
inference(cnf_transformation,[],[f303]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i] :
( leq(X1,X0)
| ~ geq(X0,X1) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_152,plain,
true,
inference(cnf_transformation,[],[f305]) ).
tcf(c_153,plain,
succ(n0) = n1,
inference(cnf_transformation,[],[f306]) ).
tcf(c_159,plain,
gt(n3,n1),
inference(cnf_transformation,[],[f312]) ).
tcf(c_161,plain,
gt(n5,n1),
inference(cnf_transformation,[],[f314]) ).
tcf(c_162,plain,
gt(n4,n1),
inference(cnf_transformation,[],[f315]) ).
tcf(c_163,plain,
gt(n1,n0),
inference(cnf_transformation,[],[f316]) ).
tcf(c_164,plain,
succ(succ(n0)) = n2,
inference(cnf_transformation,[],[f317]) ).
tcf(c_166,plain,
gt(n3,n2),
inference(cnf_transformation,[],[f319]) ).
tcf(c_167,plain,
gt(n6,n2),
inference(cnf_transformation,[],[f320]) ).
tcf(c_168,plain,
gt(n5,n2),
inference(cnf_transformation,[],[f321]) ).
tcf(c_169,plain,
gt(n4,n2),
inference(cnf_transformation,[],[f322]) ).
tcf(c_170,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f323]) ).
tcf(c_172,plain,
succ(succ(succ(n0))) = n3,
inference(cnf_transformation,[],[f325]) ).
tcf(c_173,plain,
gt(n6,n3),
inference(cnf_transformation,[],[f326]) ).
tcf(c_174,plain,
gt(n5,n3),
inference(cnf_transformation,[],[f327]) ).
tcf(c_175,plain,
gt(n4,n3),
inference(cnf_transformation,[],[f328]) ).
tcf(c_176,plain,
gt(n3,n0),
inference(cnf_transformation,[],[f329]) ).
tcf(c_178,plain,
succ(succ(succ(succ(n0)))) = n4,
inference(cnf_transformation,[],[f331]) ).
tcf(c_179,plain,
gt(n4,n0),
inference(cnf_transformation,[],[f332]) ).
tcf(c_181,plain,
gt(n6,n4),
inference(cnf_transformation,[],[f334]) ).
tcf(c_182,plain,
gt(n5,n4),
inference(cnf_transformation,[],[f335]) ).
tcf(c_183,plain,
succ(succ(succ(succ(succ(n0))))) = n5,
inference(cnf_transformation,[],[f336]) ).
tcf(c_184,plain,
gt(n5,n0),
inference(cnf_transformation,[],[f337]) ).
tcf(c_187,plain,
gt(n7,n5),
inference(cnf_transformation,[],[f340]) ).
tcf(c_188,plain,
gt(n6,n5),
inference(cnf_transformation,[],[f341]) ).
tcf(c_199,plain,
gt(n1000,n588),
inference(cnf_transformation,[],[f353]) ).
tcf(c_200,plain,
gt(n7,n3),
inference(cnf_transformation,[],[f354]) ).
tcf(c_201,plain,
gt(n7,n2),
inference(cnf_transformation,[],[f355]) ).
tcf(c_202,plain,
gt(n7,n1),
inference(cnf_transformation,[],[f356]) ).
tcf(c_206,plain,
gt(n7,n6),
inference(cnf_transformation,[],[f360]) ).
tcf(c_207,plain,
gt(n7,n4),
inference(cnf_transformation,[],[f361]) ).
tcf(c_208,plain,
succ(succ(succ(succ(succ(succ(n0)))))) = n6,
inference(cnf_transformation,[],[f362]) ).
tcf(c_209,plain,
gt(n6,n1),
inference(cnf_transformation,[],[f363]) ).
tcf(c_210,plain,
gt(n6,n0),
inference(cnf_transformation,[],[f364]) ).
tcf(c_224,plain,
! [X0: $i] : minus(succ(X0),n1) = X0,
inference(cnf_transformation,[],[f382]) ).
tcf(c_225,plain,
! [X0: $i,X1: $i] :
( leq(X1,minus(X0,n1))
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_227,plain,
leq(n0,n0),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_244,plain,
~ sP9,
inference(global_subsumption_just,[status(thm)],[c_82,c_82,c_86,c_85,c_84,c_83,c_88,c_87,c_89]) ).
tcf(c_260,plain,
~ sP11,
inference(global_subsumption_just,[status(thm)],[c_75,c_75,c_73,c_72]) ).
tcf(c_266,plain,
~ sP12,
inference(global_subsumption_just,[status(thm)],[c_70,c_70,c_69,c_68,c_71,c_67]) ).
tcf(c_274,plain,
~ sP15,
inference(global_subsumption_just,[status(thm)],[c_57,c_57,c_56,c_55]) ).
tcf(c_290,plain,
geq(minus(n1000,n1),n0),
inference(global_subsumption_just,[status(thm)],[c_79,c_136]) ).
tcf(c_310,plain,
( ~ sP13
| ~ leq(pv21,n5) ),
inference(global_subsumption_just,[status(thm)],[c_62,c_227,c_65,c_64,c_63,c_66,c_62]) ).
tcf(c_322,plain,
( sP0
| ~ sP2
| ~ leq(n3,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n6)
| ~ leq(n0,n1)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n7)
| ~ leq(n6,n7)
| ~ leq(n1,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n7,n7) ),
inference(global_subsumption_just,[status(thm)],[c_120,c_227,c_121,c_120]) ).
tcf(c_323,plain,
( sP0
| ~ sP2
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_322]) ).
tcf(c_324,plain,
( sP3
| ~ sP5
| ~ leq(n3,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n6)
| ~ leq(n0,n1)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n7)
| ~ leq(n6,n7)
| ~ leq(n1,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n7,n7) ),
inference(global_subsumption_just,[status(thm)],[c_107,c_227,c_108,c_107]) ).
tcf(c_325,plain,
( sP3
| ~ sP5
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_324]) ).
tcf(c_338,plain,
( ~ sP0
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_126,c_227,c_126]) ).
tcf(c_339,plain,
( ~ sP0
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_338]) ).
tcf(c_340,plain,
( ~ sP1
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_122,c_227,c_122]) ).
tcf(c_341,plain,
( ~ sP1
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_340]) ).
tcf(c_342,plain,
( ~ sP3
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_113,c_227,c_113]) ).
tcf(c_343,plain,
( ~ sP3
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_342]) ).
tcf(c_344,plain,
( ~ sP4
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_109,c_227,c_109]) ).
tcf(c_345,plain,
( ~ sP4
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_344]) ).
tcf(c_346,plain,
( sP13
| sP16
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_130,c_152,c_227,c_77,c_58,c_49,c_130,c_244,c_260,c_266,c_274]) ).
tcf(c_347,negated_conjecture,
( sP13
| sP16
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_346]) ).
tcf(c_362,plain,
( ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n6)
| ~ leq(n0,n1)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n7)
| ~ leq(pv5,n588)
| ~ leq(n6,n7)
| ~ leq(n1,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n7,n7)
| ~ sP7 ),
inference(global_subsumption_just,[status(thm)],[c_92,c_227,c_98,c_92,c_323,c_325,c_339,c_341,c_343,c_345]) ).
tcf(c_363,plain,
( ~ sP7
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_362]) ).
tcf(c_378,plain,
( ~ sP7
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_93,c_363]) ).
tcf(c_379,plain,
( ~ sP7
| ~ leq(n7,n7)
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_378]) ).
tcf(c_390,plain,
( sP7
| ~ sP16 ),
inference(prop_impl_just,[status(thm)],[c_52]) ).
tcf(c_402,plain,
( ~ sP13
| ~ leq(pv21,n5) ),
inference(prop_impl_just,[status(thm)],[c_310]) ).
tcf(c_464,plain,
! [X0: $i,X1: $i] :
( leq(X1,X0)
| ~ geq(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_151]) ).
tcf(c_680,plain,
( sP13
| sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_347,c_150]) ).
tcf(c_681,plain,
( ~ sP7
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_379,c_150]) ).
tcf(c_954,plain,
( ~ sP7
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_681,c_149]) ).
tcf(c_955,plain,
( sP13
| sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_680,c_149]) ).
tcf(c_1355,plain,
( sP13
| sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_955,c_149,c_149]) ).
tcf(c_1847,plain,
( ~ sP7
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_954,c_149,c_149]) ).
tcf(c_1974,plain,
succ(n1) = n2,
inference(light_normalisation,[status(thm)],[c_164,c_153]) ).
tcf(c_1975,plain,
succ(n2) = n3,
inference(light_normalisation,[status(thm)],[c_172,c_153,c_1974]) ).
tcf(c_1988,plain,
succ(n3) = n4,
inference(light_normalisation,[status(thm)],[c_178,c_153,c_1974,c_1975]) ).
tcf(c_2017,plain,
succ(n4) = n5,
inference(light_normalisation,[status(thm)],[c_183,c_153,c_1974,c_1975,c_1988]) ).
tcf(c_2026,plain,
succ(n5) = n6,
inference(light_normalisation,[status(thm)],[c_208,c_153,c_1974,c_1975,c_1988,c_2017]) ).
tcf(c_2580,plain,
! [X0: $i,X1: $i] :
( leq(X1,X0)
| ( X1 != n0 )
| ( minus(n1000,n1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_290,c_464]) ).
tcf(c_2581,plain,
leq(n0,minus(n1000,n1)),
inference(unflattening,[status(thm)],[c_2580]) ).
tcf(c_2592,plain,
( sP13
| sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1355,c_2581]) ).
tcf(c_2594,plain,
( ~ sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(pv5,n588)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n0,pv5)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1)) ),
inference(resolution,[status(thm)],[c_390,c_1847]) ).
tcf(c_2595,plain,
( ~ sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n0,n6)
| ~ leq(n0,n1)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n2)
| ~ leq(n0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_2594,c_54,c_53,c_2594]) ).
tcf(c_2596,plain,
( ~ sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(pv5,minus(n1000,n1)) ),
inference(renaming,[status(thm)],[c_2595]) ).
tcf(c_2915,plain,
( sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(pv21,n5)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n1)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1)) ),
inference(resolution,[status(thm)],[c_2592,c_402]) ).
tcf(c_5802,plain,
leq(n1,n3),
inference(superposition,[status(thm)],[c_159,c_148]) ).
tcf(c_5804,plain,
leq(n1,n5),
inference(superposition,[status(thm)],[c_161,c_148]) ).
tcf(c_5806,plain,
leq(n0,n1),
inference(superposition,[status(thm)],[c_163,c_148]) ).
tcf(c_5807,plain,
leq(n2,n3),
inference(superposition,[status(thm)],[c_166,c_148]) ).
tcf(c_5809,plain,
leq(n2,n5),
inference(superposition,[status(thm)],[c_168,c_148]) ).
tcf(c_5811,plain,
leq(n0,n2),
inference(superposition,[status(thm)],[c_170,c_148]) ).
tcf(c_5814,plain,
leq(n3,n5),
inference(superposition,[status(thm)],[c_174,c_148]) ).
tcf(c_5816,plain,
leq(n0,n3),
inference(superposition,[status(thm)],[c_176,c_148]) ).
tcf(c_5818,plain,
leq(n0,n4),
inference(superposition,[status(thm)],[c_179,c_148]) ).
tcf(c_5821,plain,
leq(n4,n5),
inference(superposition,[status(thm)],[c_182,c_148]) ).
tcf(c_5822,plain,
leq(n0,n5),
inference(superposition,[status(thm)],[c_184,c_148]) ).
tcf(c_5825,plain,
leq(n5,n7),
inference(superposition,[status(thm)],[c_187,c_148]) ).
tcf(c_5837,plain,
leq(n3,n7),
inference(superposition,[status(thm)],[c_200,c_148]) ).
tcf(c_5838,plain,
leq(n2,n7),
inference(superposition,[status(thm)],[c_201,c_148]) ).
tcf(c_5839,plain,
leq(n1,n7),
inference(superposition,[status(thm)],[c_202,c_148]) ).
tcf(c_5843,plain,
leq(n6,n7),
inference(superposition,[status(thm)],[c_206,c_148]) ).
tcf(c_5844,plain,
leq(n4,n7),
inference(superposition,[status(thm)],[c_207,c_148]) ).
tcf(c_5846,plain,
leq(n0,n6),
inference(superposition,[status(thm)],[c_210,c_148]) ).
tcf(c_5859,plain,
( sP13
| sP16
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n1,n7)
| ~ leq(n6,n7)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2592,c_5806]) ).
tcf(c_5871,plain,
( sP13
| sP16
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5859,c_5837,c_5838,c_5844,c_5825,c_5839,c_5843,c_5816,c_5811,c_5818,c_5822,c_5846]) ).
tcf(c_5887,plain,
minus(n4,n1) = n3,
inference(superposition,[status(thm)],[c_1988,c_224]) ).
tcf(c_5889,plain,
minus(n6,n1) = n5,
inference(superposition,[status(thm)],[c_2026,c_224]) ).
tcf(c_5891,plain,
( leq(pv21,n5)
| ~ sP13 ),
inference(demodulation,[status(thm)],[c_66,c_5889]) ).
tcf(c_5929,plain,
( ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| sP16 ),
inference(global_subsumption_just,[status(thm)],[c_5871,c_1355,c_2581,c_2915,c_5846,c_5844,c_5843,c_5839,c_5838,c_5837,c_5825,c_5822,c_5818,c_5816,c_5811,c_5806,c_5891]) ).
tcf(c_5930,plain,
( sP16
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1)) ),
inference(renaming,[status(thm)],[c_5929]) ).
tcf(c_5931,plain,
( sP16
| ~ leq(n3,n3)
| ~ leq(n3,n5)
| ~ leq(n2,n3)
| ~ leq(n2,n5)
| ~ leq(n4,n5)
| ~ leq(n5,n5)
| ~ leq(n1,n3)
| ~ leq(n1,n5) ),
inference(light_normalisation,[status(thm)],[c_5930,c_5887,c_5889]) ).
tcf(c_5932,plain,
( sP16
| ~ leq(n3,n5)
| ~ leq(n2,n3)
| ~ leq(n2,n5)
| ~ leq(n4,n5) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5931,c_150,c_150,c_5802,c_5804]) ).
tcf(c_5948,plain,
( sP16
| ~ leq(n3,n5)
| ~ leq(n2,n5)
| ~ leq(n4,n5) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5932,c_5807]) ).
tcf(c_6134,plain,
( leq(n1,minus(n4,n1))
| ~ gt(n4,n1) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6137,plain,
( leq(n2,minus(n6,n1))
| ~ gt(n6,n2) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6139,plain,
( leq(n2,minus(n4,n1))
| ~ gt(n4,n2) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6142,plain,
( leq(n3,minus(n6,n1))
| ~ gt(n6,n3) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6144,plain,
( leq(n3,minus(n4,n1))
| ~ gt(n4,n3) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6149,plain,
( leq(n4,minus(n6,n1))
| ~ gt(n6,n4) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6155,plain,
( leq(n5,minus(n6,n1))
| ~ gt(n6,n5) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6165,plain,
( leq(n588,minus(n1000,n1))
| ~ gt(n1000,n588) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_6174,plain,
( leq(n1,minus(n6,n1))
| ~ gt(n6,n1) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_7020,plain,
! [X0: $i] :
( leq(pv5,minus(n1000,n1))
| ~ leq(pv5,X0)
| ~ leq(X0,minus(n1000,n1)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_9604,plain,
( leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n588,minus(n1000,n1)) ),
inference(instantiation,[status(thm)],[c_7020]) ).
tcf(c_9605,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_9604,c_6174,c_6165,c_6155,c_6149,c_6144,c_6142,c_6139,c_6137,c_6134,c_5948,c_5806,c_5809,c_5811,c_5814,c_5816,c_5818,c_5821,c_5822,c_5825,c_5837,c_5838,c_5839,c_5843,c_5844,c_5846,c_2596,c_54,c_162,c_167,c_169,c_173,c_175,c_181,c_188,c_199,c_209]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV125+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/5.38 % Computer : n011.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Thu Sep 24 18:34:19 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/5.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 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.14/5.43
% 0.14/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.43
% 0.14/5.44 % Detected problem language: tptp
% 0.14/5.45 % Proving...
% 4.39/6.31 % SZS status Started for theBenchmark.p
% 4.39/6.31 % SZS status Theorem for theBenchmark.p
% 4.39/6.31
% 4.39/6.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.39/6.31
% 4.39/6.31 % ------ iProver source info
% 4.39/6.31
% 4.39/6.31 % git: date: 2026-07-19 20:42:38 +0200
% 4.39/6.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.39/6.31 % git: non_committed_changes: false
% 4.39/6.31
% 4.39/6.31 % ------ Parsing...
% 4.39/6.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.39/6.31
% 4.39/6.31 % ------ Preprocessing... sup_sim: 5 sf_s rm: 18 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 4.39/6.31
% 4.39/6.31 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.39/6.31
% 4.39/6.31 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.39/6.31 % ------ Proving...
% 4.39/6.31 % ------ Problem Properties
% 4.39/6.31
% 4.39/6.31 %
% 4.39/6.31 % clauses 100
% 4.39/6.31 % conjectures 0
% 4.39/6.31 % EPR 76
% 4.39/6.31 % Horn 91
% 4.39/6.31 % unary 70
% 4.39/6.31 % binary 17
% 4.39/6.31 % lits 202
% 4.39/6.31 % lits eq 39
% 4.39/6.31 % fd_pure 0
% 4.39/6.31 % fd_pseudo 0
% 4.39/6.31 % fd_cond 7
% 4.39/6.31 % fd_pseudo_cond 2
% 4.39/6.31 % AC symbols 0
% 4.39/6.31
% 4.39/6.31 % ------ Schedule dynamic 5 is on
% 4.39/6.31
% 4.39/6.31 % ------ no conjectures: strip conj schedule
% 4.39/6.31
% 4.39/6.31 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 4.39/6.31
% 4.39/6.31
% 4.39/6.31 % ------
% 4.39/6.31 % Current options:
% 4.39/6.31 % ------
% 4.39/6.31
% 4.39/6.31
% 4.39/6.31 %
% 4.39/6.31
% 4.39/6.31 % ------ Proving...
% 4.39/6.31 %
% 4.39/6.31
% 4.39/6.31 % SZS status Theorem for theBenchmark.p
% 4.39/6.31
% 4.39/6.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.39/6.32
% 4.39/6.32
%------------------------------------------------------------------------------