%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SWV125+1 : TPTP v9.3.1. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n004.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 : Sun Sep 27 09:01:28 AM UTC 2026 % Result : Theorem 111.14s 45.48s % Output : CNFRefutation 111.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV125+1 : TPTP v9.3.1. Bugfixed v3.3.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/20.61 % Computer : n004.cluster.edu % 0.12/20.61 % Model : x86_64 x86_64 % 0.12/20.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/20.61 % Memory : 8046.5625MB % 0.12/20.61 % OS : Linux 6.8.0-71-generic % 0.12/20.61 % CPULimit : 300 % 0.12/20.61 % WCLimit : 300 % 0.12/20.61 % DateTime : Sat Sep 26 13:14:59 UTC 2026 % 0.12/20.61 % CPUTime : % 0.12/20.61 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 111.14/45.48 % SZS status Theorem for theBenchmark.p % 111.14/45.48 % SZS output start CNFRefutation for theBenchmark.p % 111.14/45.48 fof(gt_1000_588, axiom, gt(n1000,n588)). % 111.14/45.48 fof(gt_5_4, axiom, gt(n5,n4)). % 111.14/45.48 fof(gt_7_4, axiom, gt(n7,n4)). % 111.14/45.48 fof(gt_7_5, axiom, gt(n7,n5)). % 111.14/45.48 fof(gt_7_6, axiom, gt(n7,n6)). % 111.14/45.48 fof(gt_4_0, axiom, gt(n4,n0)). % 111.14/45.48 fof(gt_5_0, axiom, gt(n5,n0)). % 111.14/45.48 fof(gt_6_0, axiom, gt(n6,n0)). % 111.14/45.48 fof(gt_1_0, axiom, gt(n1,n0)). % 111.14/45.48 fof(gt_2_0, axiom, gt(n2,n0)). % 111.14/45.48 fof(gt_5_1, axiom, gt(n5,n1)). % 111.14/45.48 fof(gt_7_1, axiom, gt(n7,n1)). % 111.14/45.48 fof(gt_3_1, axiom, gt(n3,n1)). % 111.14/45.48 fof(gt_5_2, axiom, gt(n5,n2)). % 111.14/45.48 fof(gt_7_2, axiom, gt(n7,n2)). % 111.14/45.48 fof(gt_3_2, axiom, gt(n3,n2)). % 111.14/45.48 fof(gt_4_3, axiom, gt(n4,n3)). % 111.14/45.48 fof(gt_5_3, axiom, gt(n5,n3)). % 111.14/45.48 fof(gt_7_3, axiom, gt(n7,n3)). % 111.14/45.48 fof(successor_4, axiom, succ(succ(succ(succ(n0)))) = n4). % 111.14/45.48 fof(successor_5, axiom, succ(succ(succ(succ(succ(n0))))) = n5). % 111.14/45.48 fof(successor_6, axiom, succ(succ(succ(succ(succ(succ(n0)))))) = n6). % 111.14/45.48 fof(successor_1, axiom, succ(n0) = n1). % 111.14/45.48 fof(successor_2, axiom, succ(succ(n0)) = n2). % 111.14/45.48 fof(successor_3, axiom, succ(succ(succ(n0))) = n3). % 111.14/45.48 fof(reflexivity_leq, axiom, ! [X0] : leq(X0,X0)). % 111.14/45.48 fof(transitivity_leq, axiom, ! [X0] : ! [X1] : ! [X2] : (((leq(X0,X1) & leq(X1,X2)) => leq(X0,X2)))). % 111.14/45.48 fof(leq_geq, axiom, ! [X0] : ! [X1] : ((geq(X0,X1) <=> leq(X1,X0)))). % 111.14/45.48 fof(leq_gt1, axiom, ! [X0] : ! [X1] : ((gt(X1,X0) => leq(X0,X1)))). % 111.14/45.48 fof(leq_gt_pred, axiom, ! [X0] : ! [X1] : ((leq(X0,pred(X1)) <=> gt(X1,X0)))). % 111.14/45.48 fof(pred_minus_1, axiom, ! [X0] : minus(X0,n1) = pred(X0)). % 111.14/45.48 fof(pred_succ, axiom, ! [X0] : pred(succ(X0)) = X0). % 111.14/45.48 fof(ttrue, axiom, true). % 111.14/45.48 fof(thruster_array_0001, conjecture, ((geq(minus(n4,n1),n0) & geq(minus(n1000,n1),n0)) => ! [X0] : (((geq(n7,n0) & geq(minus(n1000,n1),n0)) => ! [X1] : (((true => true) & ((true => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n0,minus(n1000,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & leq(n7,n7))))))))))))))))))))))))))) & (((leq(n0,pv5) & (leq(n0,pv21) & (leq(pv5,n588) & leq(pv21,minus(n6,n1))))) => (leq(n0,n0) & (leq(n0,pv5) & (leq(n0,pv21) & (leq(pv5,n588) & (leq(pv21,n5) & leq(pv21,minus(n6,n1)))))))) & (((leq(n0,pv5) & (leq(n0,pv31) & (leq(n0,pv32) & (leq(pv5,n588) & (leq(pv31,minus(n6,n1)) & leq(pv32,minus(n6,n1))))))) => ((pv31 != pv32 => (leq(n0,pv5) & (leq(n0,pv31) & (leq(n0,pv32) & (leq(pv5,n588) & (leq(pv31,minus(n6,n1)) & leq(pv32,minus(n6,n1)))))))) & (pv31 = pv32 => (leq(n0,pv5) & (leq(n0,pv31) & (leq(n0,pv32) & (leq(pv5,n588) & (leq(pv31,minus(n6,n1)) & leq(pv32,minus(n6,n1)))))))))) & (((leq(n0,pv5) & (leq(n0,pv31) & (leq(pv5,n588) & leq(pv31,minus(n6,n1))))) => (leq(n0,pv5) & (leq(n0,pv31) & (leq(pv5,n588) & leq(pv31,minus(n6,n1)))))) & (((leq(n0,pv5) & (leq(n0,pv31) & (leq(pv5,n588) & leq(pv31,minus(n6,n1))))) => (leq(n0,pv5) & leq(pv5,n588))) & (((leq(n0,pv5) & leq(pv5,n588)) => true) & (((leq(n0,pv5) & leq(pv5,n588)) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n2,n7) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n5,n7) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n2,n7) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n5,n7) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) & (((leq(n0,pv5) & leq(pv5,n588)) => (leq(n0,pv5) & leq(pv5,n588))) & (((leq(n0,pv23) & leq(pv23,minus(n6,n1))) => (leq(n0,'a$uselect2'(sigma,pv23)) => true)) & (geq(minus(n6,n1),n0) => (geq(minus(n6,n1),n0) => ((geq(minus(n4,n1),n0) & geq(minus(n1000,n1),n0)) => true)))))))))))))))))). % 111.14/45.48 fof(negated_conjecture, negated_conjecture, ~(((geq(minus(n4,n1),n0) & geq(minus(n1000,n1),n0)) => ! [X0] : (((geq(n7,n0) & geq(minus(n1000,n1),n0)) => ! [X1] : (((true => true) & ((true => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n0,minus(n1000,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & leq(n7,n7))))))))))))))))))))))))))) & (((leq(n0,pv5) & (leq(n0,pv21) & (leq(pv5,n588) & leq(pv21,minus(n6,n1))))) => (leq(n0,n0) & (leq(n0,pv5) & (leq(n0,pv21) & (leq(pv5,n588) & (leq(pv21,n5) & leq(pv21,minus(n6,n1)))))))) & (((leq(n0,pv5) & (leq(n0,pv31) & (leq(n0,pv32) & (leq(pv5,n588) & (leq(pv31,minus(n6,n1)) & leq(pv32,minus(n6,n1))))))) => ((pv31 != pv32 => (leq(n0,pv5) & (leq(n0,pv31) & (leq(n0,pv32) & (leq(pv5,n588) & (leq(pv31,minus(n6,n1)) & leq(pv32,minus(n6,n1)))))))) & (pv31 = pv32 => (leq(n0,pv5) & (leq(n0,pv31) & (leq(n0,pv32) & (leq(pv5,n588) & (leq(pv31,minus(n6,n1)) & leq(pv32,minus(n6,n1)))))))))) & (((leq(n0,pv5) & (leq(n0,pv31) & (leq(pv5,n588) & leq(pv31,minus(n6,n1))))) => (leq(n0,pv5) & (leq(n0,pv31) & (leq(pv5,n588) & leq(pv31,minus(n6,n1)))))) & (((leq(n0,pv5) & (leq(n0,pv31) & (leq(pv5,n588) & leq(pv31,minus(n6,n1))))) => (leq(n0,pv5) & leq(pv5,n588))) & (((leq(n0,pv5) & leq(pv5,n588)) => true) & (((leq(n0,pv5) & leq(pv5,n588)) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n2,n7) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n5,n7) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n2,n7) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n5,n7) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n1,minus(n4,n1)) & (leq(n2,minus(n4,n1)) & (leq(n3,minus(n4,n1)) & (leq(pv5,minus(n1000,n1)) & ((~gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))) & (gt(pv5,n0) => (leq(n0,n0) & (leq(n0,n1) & (leq(n0,n2) & (leq(n0,n3) & (leq(n0,n4) & (leq(n0,n5) & (leq(n0,n6) & (leq(n0,n7) & (leq(n0,pv5) & (leq(n0,minus(n4,n1)) & (leq(n0,minus(n6,n1)) & (leq(n1,n7) & (leq(n1,minus(n4,n1)) & (leq(n1,minus(n6,n1)) & (leq(n2,n7) & (leq(n2,minus(n4,n1)) & (leq(n2,minus(n6,n1)) & (leq(n3,n7) & (leq(n3,minus(n4,n1)) & (leq(n3,minus(n6,n1)) & (leq(n4,n7) & (leq(n4,minus(n6,n1)) & (leq(n5,n7) & (leq(n5,minus(n6,n1)) & (leq(n6,n7) & (leq(n7,n7) & (leq(pv5,n588) & leq(pv5,minus(n1000,n1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) & (((leq(n0,pv5) & leq(pv5,n588)) => (leq(n0,pv5) & leq(pv5,n588))) & (((leq(n0,pv23) & leq(pv23,minus(n6,n1))) => (leq(n0,'a$uselect2'(sigma,pv23)) => true)) & (geq(minus(n6,n1),n0) => (geq(minus(n6,n1),n0) => ((geq(minus(n4,n1),n0) & geq(minus(n1000,n1),n0)) => true)))))))))))))))))), inference(negate_conjecture, [status(cth)], [thruster_array_0001])). % 111.14/45.48 cnf(c0, plain, gt(n1000,n588), inference(clausification, [status(esa)], [gt_1000_588])). % 111.14/45.48 cnf(c2, plain, gt(n5,n4), inference(clausification, [status(esa)], [gt_5_4])). % 111.14/45.48 cnf(c4, plain, gt(n7,n4), inference(clausification, [status(esa)], [gt_7_4])). % 111.14/45.48 cnf(c8, plain, gt(n7,n5), inference(clausification, [status(esa)], [gt_7_5])). % 111.14/45.48 cnf(c11, plain, gt(n7,n6), inference(clausification, [status(esa)], [gt_7_6])). % 111.14/45.48 cnf(c26, plain, gt(n4,n0), inference(clausification, [status(esa)], [gt_4_0])). % 111.14/45.48 cnf(c27, plain, gt(n5,n0), inference(clausification, [status(esa)], [gt_5_0])). % 111.14/45.48 cnf(c28, plain, gt(n6,n0), inference(clausification, [status(esa)], [gt_6_0])). % 111.14/45.48 cnf(c30, plain, gt(n1,n0), inference(clausification, [status(esa)], [gt_1_0])). % 111.14/45.48 cnf(c31, plain, gt(n2,n0), inference(clausification, [status(esa)], [gt_2_0])). % 111.14/45.48 cnf(c36, plain, gt(n5,n1), inference(clausification, [status(esa)], [gt_5_1])). % 111.14/45.48 cnf(c38, plain, gt(n7,n1), inference(clausification, [status(esa)], [gt_7_1])). % 111.14/45.48 cnf(c41, plain, gt(n3,n1), inference(clausification, [status(esa)], [gt_3_1])). % 111.14/45.48 cnf(c44, plain, gt(n5,n2), inference(clausification, [status(esa)], [gt_5_2])). % 111.14/45.48 cnf(c46, plain, gt(n7,n2), inference(clausification, [status(esa)], [gt_7_2])). % 111.14/45.48 cnf(c48, plain, gt(n3,n2), inference(clausification, [status(esa)], [gt_3_2])). % 111.14/45.48 cnf(c50, plain, gt(n4,n3), inference(clausification, [status(esa)], [gt_4_3])). % 111.14/45.48 cnf(c51, plain, gt(n5,n3), inference(clausification, [status(esa)], [gt_5_3])). % 111.14/45.48 cnf(c53, plain, gt(n7,n3), inference(clausification, [status(esa)], [gt_7_3])). % 111.14/45.48 cnf(c62, plain, succ(succ(succ(succ(n0)))) = n4, inference(clausification, [status(esa)], [successor_4])). % 111.14/45.48 cnf(c63, plain, succ(succ(succ(succ(succ(n0))))) = n5, inference(clausification, [status(esa)], [successor_5])). % 111.14/45.48 cnf(c64, plain, succ(succ(succ(succ(succ(succ(n0)))))) = n6, inference(clausification, [status(esa)], [successor_6])). % 111.14/45.48 cnf(c65, plain, succ(n0) = n1, inference(clausification, [status(esa)], [successor_1])). % 111.14/45.48 cnf(c66, plain, succ(succ(n0)) = n2, inference(clausification, [status(esa)], [successor_2])). % 111.14/45.48 cnf(c67, plain, succ(succ(succ(n0))) = n3, inference(clausification, [status(esa)], [successor_3])). % 111.14/45.48 cnf(c71, plain, leq(X0,X0), inference(clausification, [status(esa)], [reflexivity_leq])). % 111.14/45.48 cnf(c72, plain, ~leq(X0,X1) | ~leq(X2,X0) | leq(X2,X1), inference(clausification, [status(esa)], [transitivity_leq])). % 111.14/45.48 cnf(c75, plain, ~geq(X0,X1) | leq(X1,X0), inference(clausification, [status(esa)], [leq_geq])). % 111.14/45.48 cnf(c76, plain, geq(X0,X1) | ~leq(X1,X0), inference(clausification, [status(esa)], [leq_geq])). % 111.14/45.48 cnf(c77, plain, ~gt(X0,X1) | leq(X1,X0), inference(clausification, [status(esa)], [leq_gt1])). % 111.14/45.48 cnf(c79, plain, ~leq(X0,pred(X1)) | gt(X1,X0), inference(clausification, [status(esa)], [leq_gt_pred])). % 111.14/45.48 cnf(c80, plain, leq(X0,pred(X1)) | ~gt(X1,X0), inference(clausification, [status(esa)], [leq_gt_pred])). % 111.14/45.48 cnf(c170, plain, pred(X0) = minus(X0,n1), inference(clausification, [status(esa)], [pred_minus_1])). % 111.14/45.48 cnf(c171, plain, pred(succ(X0)) = X0, inference(clausification, [status(esa)], [pred_succ])). % 111.14/45.48 cnf(c190, plain, true, inference(clausification, [status(esa)], [ttrue])). % 111.14/45.48 cnf(c192, plain, geq(minus(n1000,n1),n0), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c193, plain, geq(minus(n4,n1),n0), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c195, plain, geq(n7,n0), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c197, plain, ~leq(n0,minus(n1000,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n0,n4) | ~leq(n6,n7) | ~leq(n1,n7) | ~leq(n3,minus(n6,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n0,n2) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n1) | ~leq(n5,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n0,n7) | ~leq(n3,n7) | X0 | ~leq(n7,n7) | ~leq(n0,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n1,minus(n4,n1)) | ~leq(n0,n0) | ~leq(n0,n3) | ~leq(n5,minus(n6,n1)) | ~leq(n4,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,n7) | ~leq(n4,minus(n6,n1)), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c198, plain, ~X0 | leq(n0,pv21), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c199, plain, ~X0 | leq(pv21,minus(n6,n1)), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c200, plain, ~X0 | leq(pv5,n588), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c201, plain, ~X0 | leq(n0,pv5), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c202, plain, ~X0 | ~leq(pv21,n5) | ~leq(n0,n0) | ~leq(pv5,n588) | ~leq(pv21,minus(n6,n1)) | ~leq(n0,pv5) | ~leq(n0,pv21), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c206, plain, ~X0 | ~true, inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c209, plain, ~X0 | ~true, inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c211, plain, ~X0 | leq(pv5,n588), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c212, plain, ~X0 | leq(n0,pv5), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c216, plain, ~leq(pv5,minus(n1000,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n0,n4) | ~leq(n6,n7) | ~X0 | ~leq(n1,n7) | ~leq(n3,minus(n6,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n1) | ~leq(n5,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n0,n7) | ~leq(n3,n7) | ~leq(n7,n7) | ~leq(n0,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n1,minus(n4,n1)) | ~leq(n0,n0) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n0,n2) | ~leq(n5,minus(n6,n1)) | ~leq(n4,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,n7) | ~leq(n4,minus(n6,n1)), inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(c219, plain, ~true | X0 | X1 | X2 | ~X3 | X4, inference(clausification, [status(esa)], [negated_conjecture])). % 111.14/45.48 cnf(d0, plain, succ(n1) = n2, inference(demodulation, [status(thm)], [c66,c65])). % 111.14/45.48 cnf(d1, plain, succ(succ(n1)) = n3, inference(demodulation, [status(thm)], [c67,c65])). % 111.14/45.48 cnf(d2, plain, succ(n2) = n3, inference(demodulation, [status(thm)], [d1,d0])). % 111.14/45.48 cnf(d3, plain, succ(succ(succ(n1))) = n4, inference(demodulation, [status(thm)], [c62,c65])). % 111.14/45.48 cnf(d4, plain, succ(succ(n2)) = n4, inference(demodulation, [status(thm)], [d3,d0])). % 111.14/45.48 cnf(d5, plain, pred(n4) = succ(n2), inference(superposition, [status(thm)], [d4,c171])). % 111.14/45.48 cnf(d6, plain, pred(n4) = n3, inference(demodulation, [status(thm)], [d5,d2])). % 111.14/45.48 cnf(d7, plain, succ(succ(succ(succ(n1)))) = n5, inference(demodulation, [status(thm)], [c63,c65])). % 111.14/45.48 cnf(d8, plain, succ(succ(succ(n2))) = n5, inference(demodulation, [status(thm)], [d7,d0])). % 111.14/45.48 cnf(d9, plain, succ(n4) = n5, inference(demodulation, [status(thm)], [d8,d4])). % 111.14/45.48 cnf(d10, plain, succ(succ(succ(succ(succ(n1))))) = n6, inference(demodulation, [status(thm)], [c64,c65])). % 111.14/45.48 cnf(d11, plain, succ(succ(succ(succ(n2)))) = n6, inference(demodulation, [status(thm)], [d10,d0])). % 111.14/45.48 cnf(d12, plain, succ(succ(n4)) = n6, inference(demodulation, [status(thm)], [d11,d4])). % 111.14/45.48 cnf(d13, plain, succ(n5) = n6, inference(demodulation, [status(thm)], [d12,d9])). % 111.14/45.48 cnf(d14, plain, pred(n6) = n5, inference(superposition, [status(thm)], [d13,c171])). % 111.14/45.48 cnf(d15, plain, ~leq(n4,n7) | ~leq(n4,pred(n6)) | ~leq(n5,n7) | ~leq(n5,minus(n6,n1)) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [c216,c170])). % 111.14/45.48 cnf(d16, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,minus(n6,n1)) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d15,d14])). % 111.14/45.48 cnf(d17, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,pred(n6)) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d16,c170])). % 111.14/45.48 cnf(d18, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d17,d14])). % 111.14/45.48 cnf(d19, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,minus(n6,n1)) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d18,c170])). % 111.14/45.48 cnf(d20, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,pred(n6)) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d19,c170])). % 111.14/45.48 cnf(d21, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d20,d14])). % 111.14/45.48 cnf(d22, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d21,c170])). % 111.14/45.48 cnf(d23, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,pred(n6)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d22,c170])). % 111.14/45.48 cnf(d24, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d23,d14])). % 111.14/45.48 cnf(d25, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d24,c170])). % 111.14/45.48 cnf(d26, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,pred(n6)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d25,c170])). % 111.14/45.48 cnf(d27, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d26,d14])). % 111.14/45.48 cnf(d28, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,minus(n6,n1)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d27,c170])). % 111.14/45.48 cnf(d29, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,pred(n6)) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d28,c170])). % 111.14/45.48 cnf(d30, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,n5) | ~leq(pv5,n588) | ~leq(pv5,minus(n1000,n1)) | ~'Ts185', inference(demodulation, [status(thm)], [d29,d14])). % 111.14/45.48 cnf(d31, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,n5) | ~leq(pv5,n588) | ~leq(pv5,pred(n1000)) | ~'Ts185', inference(demodulation, [status(thm)], [d30,c170])). % 111.14/45.48 cnf(d32, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n0,pv5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,n5) | ~leq(pv5,n588) | ~leq(pv5,pred(n1000)) | ~'Ts185', inference(resolution, [status(thm)], [c71,d31])). % 111.14/45.48 cnf(d33, plain, leq(n0,n7), inference(resolution, [status(thm)], [c75,c195])). % 111.14/45.48 cnf(d34, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(pv5,n588) | ~leq(pv5,pred(n1000)) | ~'Ts185', inference(resolution, [status(thm)], [d33,d32])). % 111.14/45.48 cnf(d35, plain, leq(n0,minus(n4,n1)), inference(resolution, [status(thm)], [c75,c193])). % 111.14/45.48 cnf(d36, plain, leq(n0,pred(n4)), inference(demodulation, [status(thm)], [d35,c170])). % 111.14/45.48 cnf(d37, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(pv5,n588) | ~leq(pv5,pred(n1000)) | ~'Ts185', inference(resolution, [status(thm)], [d36,d34])). % 111.14/45.48 cnf(d38, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(pv5,n588) | ~'Ts185' | ~gt(n1000,pv5), inference(resolution, [status(thm)], [d37,c80])). % 111.14/45.48 cnf(d39, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(pv5,n588) | ~'Ts185', inference(demodulation, [status(thm)], [d38,d6])). % 111.14/45.48 cnf(d40, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(pv5,n588) | ~'Ts185', inference(demodulation, [status(thm)], [d39,d6])). % 111.14/45.48 cnf(d41, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(demodulation, [status(thm)], [d40,d6])). % 111.14/45.48 cnf(d42, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [c71,d41])). % 111.14/45.48 cnf(d43, plain, leq(n0,n3), inference(demodulation, [status(thm)], [d36,d6])). % 111.14/45.48 cnf(d44, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d43,d42])). % 111.14/45.48 cnf(d45, plain, leq(n0,n6), inference(resolution, [status(thm)], [c77,c28])). % 111.14/45.48 cnf(d46, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d45,d44])). % 111.14/45.48 cnf(d47, plain, leq(n0,n4), inference(resolution, [status(thm)], [c77,c26])). % 111.14/45.48 cnf(d48, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d47,d46])). % 111.14/45.48 cnf(d49, plain, leq(n2,n3), inference(resolution, [status(thm)], [c77,c48])). % 111.14/45.48 cnf(d50, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d49,d48])). % 111.14/45.48 cnf(d51, plain, leq(n1,n3), inference(resolution, [status(thm)], [c77,c41])). % 111.14/45.48 cnf(d52, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d51,d50])). % 111.14/45.48 cnf(d53, plain, leq(n0,n2), inference(resolution, [status(thm)], [c77,c31])). % 111.14/45.48 cnf(d54, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d53,d52])). % 111.14/45.48 cnf(d55, plain, leq(n0,n1), inference(resolution, [status(thm)], [c77,c30])). % 111.14/45.48 cnf(d56, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d55,d54])). % 111.14/45.48 cnf(d57, plain, leq(n6,n7), inference(resolution, [status(thm)], [c77,c11])). % 111.14/45.48 cnf(d58, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d57,d56])). % 111.14/45.48 cnf(d59, plain, leq(n4,n7), inference(resolution, [status(thm)], [c77,c4])). % 111.14/45.48 cnf(d60, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d59,d58])). % 111.14/45.48 cnf(d61, plain, leq(n3,n7), inference(resolution, [status(thm)], [c77,c53])). % 111.14/45.48 cnf(d62, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d61,d60])). % 111.14/45.48 cnf(d63, plain, leq(n2,n7), inference(resolution, [status(thm)], [c77,c46])). % 111.14/45.48 cnf(d64, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n3,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d63,d62])). % 111.14/45.48 cnf(d65, plain, leq(n1,n7), inference(resolution, [status(thm)], [c77,c38])). % 111.14/45.48 cnf(d66, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d65,d64])). % 111.14/45.48 cnf(d67, plain, leq(n5,n7), inference(resolution, [status(thm)], [c77,c8])). % 111.14/45.48 cnf(d68, plain, ~gt(n1000,pv5) | ~leq(n4,n5) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d67,d66])). % 111.14/45.48 cnf(d69, plain, leq(n4,n5), inference(resolution, [status(thm)], [c77,c2])). % 111.14/45.48 cnf(d70, plain, ~gt(n1000,pv5) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d69,d68])). % 111.14/45.48 cnf(d71, plain, leq(n3,n5), inference(resolution, [status(thm)], [c77,c51])). % 111.14/45.48 cnf(d72, plain, ~gt(n1000,pv5) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d71,d70])). % 111.14/45.48 cnf(d73, plain, leq(n0,n5), inference(resolution, [status(thm)], [c77,c27])). % 111.14/45.48 cnf(d74, plain, ~gt(n1000,pv5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d73,d72])). % 111.14/45.48 cnf(d75, plain, leq(n2,n5), inference(resolution, [status(thm)], [c77,c44])). % 111.14/45.48 cnf(d76, plain, ~gt(n1000,pv5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n1,n5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d75,d74])). % 111.14/45.48 cnf(d77, plain, leq(n1,n5), inference(resolution, [status(thm)], [c77,c36])). % 111.14/45.48 cnf(d78, plain, ~gt(n1000,pv5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n3,n3) | ~leq(pv5,n588) | ~'Ts185', inference(resolution, [status(thm)], [d77,d76])). % 111.14/45.48 cnf(d79, plain, ~'Ts186' | 'Ts182' | 'Ts183' | 'Ts184' | 'Ts185', inference(resolution, [status(thm)], [c190,c219])). % 111.14/45.48 cnf(d80, plain, ~'Ts183', inference(resolution, [status(thm)], [c190,c206])). % 111.14/45.48 cnf(d81, plain, ~'Ts186' | 'Ts182' | 'Ts184' | 'Ts185', inference(resolution, [status(thm)], [d80,d79])). % 111.14/45.48 cnf(d82, plain, ~'Ts184', inference(resolution, [status(thm)], [c190,c209])). % 111.14/45.48 cnf(d83, plain, ~'Ts186' | 'Ts182' | 'Ts185', inference(resolution, [status(thm)], [d82,d81])). % 111.14/45.48 cnf(d84, plain, ~leq(n0,n0) | ~leq(n0,pv21) | ~leq(n0,pv5) | ~leq(pv21,n5) | ~leq(pv5,n588) | ~'Ts182' | ~'Ts182', inference(resolution, [status(thm)], [c202,c199])). % 111.14/45.48 cnf(d85, plain, ~leq(n0,n0) | ~leq(n0,pv21) | ~leq(n0,pv5) | ~leq(pv21,n5) | ~'Ts182' | ~'Ts182', inference(resolution, [status(thm)], [d84,c200])). % 111.14/45.48 cnf(d86, plain, ~leq(n0,pv21) | ~leq(n0,pv5) | ~leq(pv21,n5) | ~'Ts182', inference(resolution, [status(thm)], [c71,d85])). % 111.14/45.48 cnf(d87, plain, geq(minus(n6,n1),pv21) | ~'Ts182', inference(resolution, [status(thm)], [c76,c199])). % 111.14/45.48 cnf(d88, plain, geq(pred(n6),pv21) | ~'Ts182', inference(demodulation, [status(thm)], [d87,c170])). % 111.14/45.48 cnf(d89, plain, geq(n5,pv21) | ~'Ts182', inference(demodulation, [status(thm)], [d88,d14])). % 111.14/45.48 cnf(d90, plain, ~'Ts182' | leq(pv21,n5), inference(resolution, [status(thm)], [d89,c75])). % 111.14/45.48 cnf(d91, plain, ~'Ts182' | ~leq(n0,pv21) | ~leq(n0,pv5) | ~'Ts182', inference(resolution, [status(thm)], [d90,d86])). % 111.14/45.48 cnf(d92, plain, ~leq(n0,pv21) | ~'Ts182' | ~'Ts182', inference(resolution, [status(thm)], [d91,c201])). % 111.14/45.48 cnf(d93, plain, ~'Ts182' | ~'Ts182', inference(resolution, [status(thm)], [d92,c198])). % 111.14/45.48 cnf(d94, plain, ~'Ts186' | 'Ts185', inference(resolution, [status(thm)], [d93,d83])). % 111.14/45.48 cnf(d95, plain, ~leq(n4,n7) | ~leq(n4,pred(n6)) | ~leq(n5,n7) | ~leq(n5,minus(n6,n1)) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n1000,n1)) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [c197,c170])). % 111.14/45.48 cnf(d96, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,minus(n6,n1)) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n1000,n1)) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d95,d14])). % 111.14/45.48 cnf(d97, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,pred(n6)) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n1000,n1)) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d96,c170])). % 111.14/45.48 cnf(d98, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,minus(n1000,n1)) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d97,d14])). % 111.14/45.48 cnf(d99, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,minus(n4,n1)) | ~leq(n0,minus(n6,n1)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d98,c170])). % 111.14/45.48 cnf(d100, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,minus(n6,n1)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d99,c170])). % 111.14/45.48 cnf(d101, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,pred(n6)) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d100,c170])). % 111.14/45.48 cnf(d102, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,minus(n4,n1)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d101,d14])). % 111.14/45.48 cnf(d103, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,minus(n6,n1)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d102,c170])). % 111.14/45.48 cnf(d104, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,pred(n6)) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d103,c170])). % 111.14/45.48 cnf(d105, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,minus(n4,n1)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d104,d14])). % 111.14/45.48 cnf(d106, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,minus(n6,n1)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d105,c170])). % 111.14/45.48 cnf(d107, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,pred(n6)) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d106,c170])). % 111.14/45.48 cnf(d108, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,minus(n4,n1)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d107,d14])). % 111.14/45.48 cnf(d109, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,minus(n6,n1)) | 'Ts186', inference(demodulation, [status(thm)], [d108,c170])). % 111.14/45.48 cnf(d110, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,pred(n6)) | 'Ts186', inference(demodulation, [status(thm)], [d109,c170])). % 111.14/45.48 cnf(d111, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n5,n5) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,n5) | 'Ts186', inference(demodulation, [status(thm)], [d110,d14])). % 111.14/45.48 cnf(d112, plain, ~leq(n4,n7) | ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n7) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n0,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n1,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n2,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | ~leq(n3,n5) | 'Ts186', inference(resolution, [status(thm)], [c71,d111])). % 111.14/45.48 cnf(d113, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n1000)) | ~leq(n0,pred(n4)) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | 'Ts186', inference(resolution, [status(thm)], [d33,d112])). % 111.14/45.48 cnf(d114, plain, leq(n0,minus(n1000,n1)), inference(resolution, [status(thm)], [c75,c192])). % 111.14/45.48 cnf(d115, plain, leq(n0,pred(n1000)), inference(demodulation, [status(thm)], [d114,c170])). % 111.14/45.48 cnf(d116, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n0,pred(n4)) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | 'Ts186', inference(resolution, [status(thm)], [d115,d113])). % 111.14/45.48 cnf(d117, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | ~leq(n3,pred(n4)) | 'Ts186', inference(resolution, [status(thm)], [d36,d116])). % 111.14/45.48 cnf(d118, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,pred(n4)) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186' | ~gt(n4,n3), inference(resolution, [status(thm)], [d117,c80])). % 111.14/45.48 cnf(d119, plain, ~gt(n4,n3) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,pred(n4)) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(demodulation, [status(thm)], [d118,d6])). % 111.14/45.48 cnf(d120, plain, ~gt(n4,n3) | ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(demodulation, [status(thm)], [d119,d6])). % 111.14/45.48 cnf(d121, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n7,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [c50,d120])). % 111.14/45.48 cnf(d122, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n0,n3) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [c71,d121])). % 111.14/45.48 cnf(d123, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n6) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d43,d122])). % 111.14/45.48 cnf(d124, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n4) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d45,d123])). % 111.14/45.48 cnf(d125, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n2,n3) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d47,d124])). % 111.14/45.48 cnf(d126, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n1,n3) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d49,d125])). % 111.14/45.48 cnf(d127, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n0,n2) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d51,d126])). % 111.14/45.48 cnf(d128, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n0,n1) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d53,d127])). % 111.14/45.48 cnf(d129, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n6,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d55,d128])). % 111.14/45.48 cnf(d130, plain, ~leq(n4,n5) | ~leq(n4,n7) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d57,d129])). % 111.14/45.48 cnf(d131, plain, ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | ~leq(n3,n7) | 'Ts186', inference(resolution, [status(thm)], [d59,d130])). % 111.14/45.48 cnf(d132, plain, ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n2,n7) | ~leq(n3,n5) | 'Ts186', inference(resolution, [status(thm)], [d61,d131])). % 111.14/45.48 cnf(d133, plain, ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n1,n7) | ~leq(n2,n5) | ~leq(n3,n5) | 'Ts186', inference(resolution, [status(thm)], [d63,d132])). % 111.14/45.48 cnf(d134, plain, ~leq(n4,n5) | ~leq(n5,n7) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n5) | 'Ts186', inference(resolution, [status(thm)], [d65,d133])). % 111.14/45.48 cnf(d135, plain, ~leq(n4,n5) | ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n5) | 'Ts186', inference(resolution, [status(thm)], [d67,d134])). % 111.14/45.48 cnf(d136, plain, ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n2,n5) | ~leq(n3,n5) | 'Ts186', inference(resolution, [status(thm)], [d69,d135])). % 111.14/45.48 cnf(d137, plain, ~leq(n0,n5) | ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n2,n5) | 'Ts186', inference(resolution, [status(thm)], [d71,d136])). % 111.14/45.48 cnf(d138, plain, ~leq(n0,n0) | ~leq(n1,n5) | ~leq(n2,n5) | 'Ts186', inference(resolution, [status(thm)], [d73,d137])). % 111.14/45.48 cnf(d139, plain, ~leq(n0,n0) | ~leq(n1,n5) | 'Ts186', inference(resolution, [status(thm)], [d75,d138])). % 111.14/45.48 cnf(d140, plain, ~leq(n0,n0) | 'Ts186', inference(resolution, [status(thm)], [d77,d139])). % 111.14/45.48 cnf(d141, plain, 'Ts186', inference(resolution, [status(thm)], [d140,c71])). % 111.14/45.48 cnf(d142, plain, 'Ts185', inference(resolution, [status(thm)], [d141,d94])). % 111.14/45.48 cnf(d143, plain, ~gt(n1000,pv5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n3,n3) | ~leq(pv5,n588), inference(resolution, [status(thm)], [d142,d78])). % 111.14/45.48 cnf(d144, plain, leq(pv5,n588), inference(resolution, [status(thm)], [d142,c211])). % 111.14/45.48 cnf(d145, plain, ~gt(n1000,pv5) | ~leq(n0,n0) | ~leq(n0,pv5) | ~leq(n3,n3), inference(resolution, [status(thm)], [d144,d143])). % 111.14/45.48 cnf(d146, plain, leq(n0,pv5), inference(resolution, [status(thm)], [d142,c212])). % 111.14/45.48 cnf(d147, plain, ~gt(n1000,pv5) | ~leq(n0,n0) | ~leq(n3,n3), inference(resolution, [status(thm)], [d146,d145])). % 111.14/45.48 cnf(d148, plain, ~gt(X0,X1) | leq(X2,pred(X0)) | ~leq(X2,X1), inference(resolution, [status(thm)], [c80,c72])). % 111.14/45.48 cnf(d149, plain, ~gt(X0,n588) | leq(pv5,pred(X0)) | ~'Ts185', inference(resolution, [status(thm)], [d148,c211])). % 111.14/45.48 cnf(d150, plain, ~gt(X0,n588) | ~'Ts185' | gt(X0,pv5), inference(resolution, [status(thm)], [d149,c79])). % 111.14/45.48 cnf(d151, plain, gt(n1000,pv5) | ~'Ts185', inference(resolution, [status(thm)], [d150,c0])). % 111.14/45.48 cnf(d152, plain, gt(n1000,pv5), inference(resolution, [status(thm)], [d142,d151])). % 111.14/45.48 cnf(d153, plain, ~leq(n0,n0) | ~leq(n3,n3), inference(resolution, [status(thm)], [d152,d147])). % 111.14/45.48 cnf(d154, plain, ~leq(n0,n0), inference(resolution, [status(thm)], [d153,c71])). % 111.14/45.48 cnf(d155, plain, $false, inference(resolution, [status(thm)], [c71,d154])). % 111.14/45.48 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------