%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV039+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:18 AM UTC 2026
% Result : Theorem 19.86s 7.92s
% Output : CNFRefutation 19.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV039+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/5.31 % Computer : n012.cluster.edu
% 0.04/5.31 % Model : x86_64 x86_64
% 0.04/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.31 % Memory : 8046.5625MB
% 0.04/5.31 % OS : Linux 6.8.0-71-generic
% 0.04/5.31 % CPULimit : 300
% 0.04/5.31 % WCLimit : 300
% 0.04/5.31 % DateTime : Sat Sep 26 13:08:06 UTC 2026
% 0.04/5.31 % CPUTime :
% 0.04/5.31 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.86/7.92 % SZS status Theorem for theBenchmark.p
% 19.86/7.92 % SZS output start CNFRefutation for theBenchmark.p
% 19.86/7.92 fof(irreflexivity_gt, axiom, ! [X0] : ~gt(X0,X0)).
% 19.86/7.92 fof(transitivity_leq, axiom, ! [X0] : ! [X1] : ! [X2] : (((leq(X0,X1) & leq(X1,X2)) => leq(X0,X2)))).
% 19.86/7.92 fof(leq_geq, axiom, ! [X0] : ! [X1] : ((geq(X0,X1) <=> leq(X1,X0)))).
% 19.86/7.92 fof(leq_gt_pred, axiom, ! [X0] : ! [X1] : ((leq(X0,pred(X1)) <=> gt(X1,X0)))).
% 19.86/7.92 fof(leq_succ_gt_equiv, axiom, ! [X0] : ! [X1] : ((leq(X0,X1) <=> gt(succ(X1),X0)))).
% 19.86/7.92 fof(succ_tptp_minus_1, axiom, succ('tptp$uminus$u1') = n0).
% 19.86/7.92 fof(pred_minus_1, axiom, ! [X0] : minus(X0,n1) = pred(X0)).
% 19.86/7.92 fof(pred_succ, axiom, ! [X0] : pred(succ(X0)) = X0).
% 19.86/7.92 fof(gauss_init_0069, conjecture, (('s$ubest7$uinit' = init & ('s$usworst7$uinit' = init & ('s$uworst7$uinit' = init & (leq(n0,'s$ubest7') & (leq(n0,'s$usworst7') & (leq(n0,'s$uworst7') & (leq('s$ubest7',n3) & (leq('s$usworst7',n3) & (leq('s$uworst7',n3) & (! [X0] : (((leq(n0,X0) & leq(X0,n2)) => ! [X1] : (((leq(n0,X1) & leq(X1,n3)) => 'a$uselect3'('simplex7$uinit',X1,X0) = init)))) & (! [X2] : (((leq(n0,X2) & leq(X2,n3)) => 'a$uselect2'('s$uvalues7$uinit',X2) = init)) & (! [X3] : (((leq(n0,X3) & leq(X3,n2)) => 'a$uselect2'('s$ucenter7$uinit',X3) = init)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init))))))))))))))) => ('s$ubest7$uinit' = init & ('s$usworst7$uinit' = init & ('s$uworst7$uinit' = init & (leq(n0,'s$ubest7') & (leq(n0,'s$usworst7') & (leq(n0,'s$uworst7') & (leq('s$ubest7',n3) & (leq('s$usworst7',n3) & (leq('s$uworst7',n3) & (! [X4] : (((leq(n0,X4) & leq(X4,n2)) => ! [X5] : (((leq(n0,X5) & leq(X5,n3)) => 'a$uselect3'('simplex7$uinit',X5,X4) = init)))) & (! [X6] : (((leq(n0,X6) & leq(X6,n3)) => 'a$uselect2'('s$uvalues7$uinit',X6) = init)) & (! [X7] : (((leq(n0,X7) & leq(X7,n2)) => 'a$uselect2'('s$ucenter7$uinit',X7) = init)) & (! [X8] : (((leq(n0,X8) & leq(X8,minus(n0,n1))) => 'a$uselect2'('s$utry7$uinit',X8) = init)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init)))))))))))))))))).
% 19.86/7.92 fof(negated_conjecture, negated_conjecture, ~((('s$ubest7$uinit' = init & ('s$usworst7$uinit' = init & ('s$uworst7$uinit' = init & (leq(n0,'s$ubest7') & (leq(n0,'s$usworst7') & (leq(n0,'s$uworst7') & (leq('s$ubest7',n3) & (leq('s$usworst7',n3) & (leq('s$uworst7',n3) & (! [X0] : (((leq(n0,X0) & leq(X0,n2)) => ! [X1] : (((leq(n0,X1) & leq(X1,n3)) => 'a$uselect3'('simplex7$uinit',X1,X0) = init)))) & (! [X2] : (((leq(n0,X2) & leq(X2,n3)) => 'a$uselect2'('s$uvalues7$uinit',X2) = init)) & (! [X3] : (((leq(n0,X3) & leq(X3,n2)) => 'a$uselect2'('s$ucenter7$uinit',X3) = init)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init))))))))))))))) => ('s$ubest7$uinit' = init & ('s$usworst7$uinit' = init & ('s$uworst7$uinit' = init & (leq(n0,'s$ubest7') & (leq(n0,'s$usworst7') & (leq(n0,'s$uworst7') & (leq('s$ubest7',n3) & (leq('s$usworst7',n3) & (leq('s$uworst7',n3) & (! [X4] : (((leq(n0,X4) & leq(X4,n2)) => ! [X5] : (((leq(n0,X5) & leq(X5,n3)) => 'a$uselect3'('simplex7$uinit',X5,X4) = init)))) & (! [X6] : (((leq(n0,X6) & leq(X6,n3)) => 'a$uselect2'('s$uvalues7$uinit',X6) = init)) & (! [X7] : (((leq(n0,X7) & leq(X7,n2)) => 'a$uselect2'('s$ucenter7$uinit',X7) = init)) & (! [X8] : (((leq(n0,X8) & leq(X8,minus(n0,n1))) => 'a$uselect2'('s$utry7$uinit',X8) = init)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init)))))))))))))))))), inference(negate_conjecture, [status(cth)], [gauss_init_0069])).
% 19.86/7.92 cnf(c34, plain, ~gt(X0,X0), inference(clausification, [status(esa)], [irreflexivity_gt])).
% 19.86/7.92 cnf(c36, plain, ~leq(X0,X1) | ~leq(X1,X2) | leq(X0,X2), inference(clausification, [status(esa)], [transitivity_leq])).
% 19.86/7.92 cnf(c39, plain, ~geq(X0,X1) | leq(X1,X0), inference(clausification, [status(esa)], [leq_geq])).
% 19.86/7.92 cnf(c40, plain, geq(X0,X1) | ~leq(X1,X0), inference(clausification, [status(esa)], [leq_geq])).
% 19.86/7.92 cnf(c43, plain, ~leq(X0,pred(X1)) | gt(X1,X0), inference(clausification, [status(esa)], [leq_gt_pred])).
% 19.86/7.92 cnf(c44, plain, leq(X0,pred(X1)) | ~gt(X1,X0), inference(clausification, [status(esa)], [leq_gt_pred])).
% 19.86/7.92 cnf(c47, plain, ~leq(X0,X1) | gt(succ(X1),X0), inference(clausification, [status(esa)], [leq_succ_gt_equiv])).
% 19.86/7.92 cnf(c123, plain, succ('tptp$uminus$u1') = n0, inference(clausification, [status(esa)], [succ_tptp_minus_1])).
% 19.86/7.92 cnf(c134, plain, minus(X0,n1) = pred(X0), inference(clausification, [status(esa)], [pred_minus_1])).
% 19.86/7.92 cnf(c135, plain, pred(succ(X0)) = X0, inference(clausification, [status(esa)], [pred_succ])).
% 19.86/7.92 cnf(c156, plain, 's$ubest7$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c157, plain, 's$usworst7$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c158, plain, 's$uworst7$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c159, plain, leq(n0,'s$ubest7'), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c160, plain, leq(n0,'s$usworst7'), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c161, plain, leq(n0,'s$uworst7'), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c162, plain, leq('s$ubest7',n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c163, plain, leq('s$usworst7',n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c164, plain, leq('s$uworst7',n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c165, plain, ~leq(X0,n2) | ~leq(n0,X0) | 'a$uselect3'('simplex7$uinit',X1,X0) = init | ~leq(X1,n3) | ~leq(n0,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c166, plain, ~leq(n0,X0) | ~leq(X0,n3) | 'a$uselect2'('s$uvalues7$uinit',X0) = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c167, plain, ~leq(n0,X0) | ~leq(X0,n2) | 'a$uselect2'('s$ucenter7$uinit',X0) = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c168, plain, ~gt(loopcounter,n1) | 'pvar1400$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c169, plain, ~gt(loopcounter,n1) | 'pvar1401$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c170, plain, ~gt(loopcounter,n1) | 'pvar1402$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c171, plain, ~X0 | ~leq(n0,'s$usworst7') | 's$uworst7$uinit' != init | 's$ubest7$uinit' != init | 's$usworst7$uinit' != init | ~leq(n0,'s$ubest7') | ~leq('s$ubest7',n3) | gt(loopcounter,n1) | ~X1 | ~leq('s$usworst7',n3) | ~leq(n0,'s$uworst7') | ~X2 | ~X3 | ~leq('s$uworst7',n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c172, plain, ~X0 | ~leq(n0,'s$usworst7') | 's$uworst7$uinit' != init | 's$ubest7$uinit' != init | 's$usworst7$uinit' != init | ~leq(n0,'s$ubest7') | 'pvar1401$uinit' != init | ~leq('s$ubest7',n3) | 'pvar1402$uinit' != init | ~X1 | ~leq('s$usworst7',n3) | 'pvar1400$uinit' != init | ~leq(n0,'s$uworst7') | ~X2 | ~X3 | ~leq('s$uworst7',n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c173, plain, X0 | leq(n0,sK189), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c174, plain, X0 | leq(sK189,minus(n0,n1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c176, plain, X0 | leq(n0,sK190), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c177, plain, X0 | leq(sK190,n2), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c178, plain, X0 | 'a$uselect2'('s$ucenter7$uinit',sK190) != init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c179, plain, X0 | leq(n0,sK191), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c180, plain, X0 | leq(sK191,n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c181, plain, X0 | 'a$uselect2'('s$uvalues7$uinit',sK191) != init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c182, plain, X0 | leq(n0,sK192), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c183, plain, X0 | leq(sK192,n2), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c184, plain, X0 | leq(n0,sK193), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c185, plain, X0 | leq(sK193,n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(c186, plain, X0 | 'a$uselect3'('simplex7$uinit',sK193,sK192) != init, inference(clausification, [status(esa)], [negated_conjecture])).
% 19.86/7.92 cnf(d0, plain, pred(n0) = 'tptp$uminus$u1', inference(superposition, [status(thm)], [c123,c135])).
% 19.86/7.92 cnf(d1, plain, init != init | 's$usworst7$uinit' != init | 's$uworst7$uinit' != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq(n0,'s$ubest7') | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(demodulation, [status(thm)], [c172,c156])).
% 19.86/7.92 cnf(d2, plain, init != init | init != init | 's$uworst7$uinit' != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq(n0,'s$ubest7') | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(demodulation, [status(thm)], [d1,c157])).
% 19.86/7.92 cnf(d3, plain, init != init | init != init | init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq(n0,'s$ubest7') | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(demodulation, [status(thm)], [d2,c158])).
% 19.86/7.92 cnf(d4, plain, init != init | init != init | init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c159,d3])).
% 19.86/7.92 cnf(d5, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c160,d4])).
% 19.86/7.92 cnf(d6, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c161,d5])).
% 19.86/7.92 cnf(d7, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c162,d6])).
% 19.86/7.92 cnf(d8, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c163,d7])).
% 19.86/7.92 cnf(d9, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c164,d8])).
% 19.86/7.92 cnf(d10, plain, init != init | 'Ts183' | ~leq(sK191,n3) | ~leq(n0,sK191), inference(superposition, [status(thm)], [c166,c181])).
% 19.86/7.92 cnf(d11, plain, ~leq(n0,sK191) | ~leq(sK191,n3) | 'Ts183', inference(equality_resolution, [status(thm)], [d10])).
% 19.86/7.92 cnf(d12, plain, ~leq(n0,sK191) | 'Ts183' | 'Ts183', inference(resolution, [status(thm)], [d11,c180])).
% 19.86/7.92 cnf(d13, plain, 'Ts183' | 'Ts183', inference(resolution, [status(thm)], [d12,c179])).
% 19.86/7.92 cnf(d14, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~'Ts184' | ~'Ts181' | ~'Ts182', inference(resolution, [status(thm)], [d13,d9])).
% 19.86/7.92 cnf(d15, plain, init != init | 'Ts182' | ~leq(sK190,n2) | ~leq(n0,sK190), inference(superposition, [status(thm)], [c167,c178])).
% 19.86/7.92 cnf(d16, plain, ~leq(n0,sK190) | ~leq(sK190,n2) | 'Ts182', inference(equality_resolution, [status(thm)], [d15])).
% 19.86/7.92 cnf(d17, plain, ~leq(n0,sK190) | 'Ts182' | 'Ts182', inference(resolution, [status(thm)], [d16,c177])).
% 19.86/7.92 cnf(d18, plain, 'Ts182' | 'Ts182', inference(resolution, [status(thm)], [d17,c176])).
% 19.86/7.92 cnf(d19, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~'Ts184' | ~'Ts181', inference(resolution, [status(thm)], [d18,d14])).
% 19.86/7.92 cnf(d20, plain, init != init | 'Ts184' | ~leq(sK193,n3) | ~leq(sK192,n2) | ~leq(n0,sK193) | ~leq(n0,sK192), inference(superposition, [status(thm)], [c165,c186])).
% 19.86/7.92 cnf(d21, plain, ~leq(n0,sK192) | ~leq(n0,sK193) | ~leq(sK192,n2) | ~leq(sK193,n3) | 'Ts184', inference(equality_resolution, [status(thm)], [d20])).
% 19.86/7.92 cnf(d22, plain, ~leq(n0,sK192) | ~leq(n0,sK193) | ~leq(sK192,n2) | 'Ts184' | 'Ts184', inference(resolution, [status(thm)], [d21,c185])).
% 19.86/7.92 cnf(d23, plain, ~leq(n0,sK192) | ~leq(n0,sK193) | 'Ts184' | 'Ts184', inference(resolution, [status(thm)], [d22,c183])).
% 19.86/7.92 cnf(d24, plain, ~leq(n0,sK192) | 'Ts184' | 'Ts184', inference(resolution, [status(thm)], [d23,c184])).
% 19.86/7.92 cnf(d25, plain, 'Ts184' | 'Ts184', inference(resolution, [status(thm)], [d24,c182])).
% 19.86/7.92 cnf(d26, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~'Ts181', inference(resolution, [status(thm)], [d25,d19])).
% 19.86/7.92 cnf(d27, plain, init != init | 's$usworst7$uinit' != init | 's$uworst7$uinit' != init | gt(loopcounter,n1) | ~leq(n0,'s$ubest7') | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(demodulation, [status(thm)], [c171,c156])).
% 19.86/7.92 cnf(d28, plain, init != init | init != init | 's$uworst7$uinit' != init | gt(loopcounter,n1) | ~leq(n0,'s$ubest7') | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(demodulation, [status(thm)], [d27,c157])).
% 19.86/7.92 cnf(d29, plain, init != init | init != init | init != init | gt(loopcounter,n1) | ~leq(n0,'s$ubest7') | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(demodulation, [status(thm)], [d28,c158])).
% 19.86/7.92 cnf(d30, plain, init != init | init != init | init != init | gt(loopcounter,n1) | ~leq(n0,'s$usworst7') | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c159,d29])).
% 19.86/7.92 cnf(d31, plain, init != init | gt(loopcounter,n1) | ~leq(n0,'s$uworst7') | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c160,d30])).
% 19.86/7.92 cnf(d32, plain, init != init | gt(loopcounter,n1) | ~leq('s$ubest7',n3) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c161,d31])).
% 19.86/7.92 cnf(d33, plain, init != init | gt(loopcounter,n1) | ~leq('s$usworst7',n3) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c162,d32])).
% 19.86/7.92 cnf(d34, plain, init != init | gt(loopcounter,n1) | ~leq('s$uworst7',n3) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c163,d33])).
% 19.86/7.92 cnf(d35, plain, init != init | gt(loopcounter,n1) | ~'Ts184' | ~'Ts181' | ~'Ts182' | ~'Ts183', inference(resolution, [status(thm)], [c164,d34])).
% 19.86/7.92 cnf(d36, plain, init != init | gt(loopcounter,n1) | ~'Ts184' | ~'Ts181' | ~'Ts182', inference(resolution, [status(thm)], [d13,d35])).
% 19.86/7.92 cnf(d37, plain, init != init | gt(loopcounter,n1) | ~'Ts184' | ~'Ts181', inference(resolution, [status(thm)], [d18,d36])).
% 19.86/7.92 cnf(d38, plain, init != init | gt(loopcounter,n1) | ~'Ts181', inference(resolution, [status(thm)], [d25,d37])).
% 19.86/7.92 cnf(d39, plain, gt(loopcounter,n1) | ~'Ts181', inference(equality_resolution, [status(thm)], [d38])).
% 19.86/7.92 cnf(d40, plain, ~'Ts181' | 'pvar1402$uinit' = init, inference(resolution, [status(thm)], [d39,c170])).
% 19.86/7.92 cnf(d41, plain, init != init | init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | ~'Ts181' | ~'Ts181', inference(superposition, [status(thm)], [d40,d26])).
% 19.86/7.92 cnf(d42, plain, ~'Ts181' | 'pvar1401$uinit' = init, inference(resolution, [status(thm)], [d39,c169])).
% 19.86/7.92 cnf(d43, plain, init != init | init != init | 'pvar1400$uinit' != init | ~'Ts181' | ~'Ts181', inference(superposition, [status(thm)], [d42,d41])).
% 19.86/7.92 cnf(d44, plain, ~'Ts181' | 'pvar1400$uinit' = init, inference(resolution, [status(thm)], [d39,c168])).
% 19.86/7.92 cnf(d45, plain, init != init | init != init | ~'Ts181' | ~'Ts181', inference(superposition, [status(thm)], [d44,d43])).
% 19.86/7.92 cnf(d46, plain, ~'Ts181', inference(equality_resolution, [status(thm)], [d45])).
% 19.86/7.92 cnf(d47, plain, leq(sK189,minus(n0,n1)), inference(resolution, [status(thm)], [d46,c174])).
% 19.86/7.92 cnf(d48, plain, geq(minus(n0,n1),sK189), inference(resolution, [status(thm)], [c40,d47])).
% 19.86/7.92 cnf(d49, plain, geq(pred(n0),sK189), inference(demodulation, [status(thm)], [d48,c134])).
% 19.86/7.92 cnf(d50, plain, geq('tptp$uminus$u1',sK189), inference(demodulation, [status(thm)], [d49,d0])).
% 19.86/7.92 cnf(d51, plain, leq(sK189,'tptp$uminus$u1'), inference(resolution, [status(thm)], [d50,c39])).
% 19.86/7.92 cnf(d52, plain, leq(n0,sK189), inference(resolution, [status(thm)], [d46,c173])).
% 19.86/7.92 cnf(d53, plain, ~leq(sK189,X0) | leq(n0,X0), inference(resolution, [status(thm)], [c36,d52])).
% 19.86/7.92 cnf(d54, plain, ~gt(X0,sK189) | leq(n0,pred(X0)), inference(resolution, [status(thm)], [c44,d53])).
% 19.86/7.92 cnf(d55, plain, ~gt(X0,sK189) | gt(X0,n0), inference(resolution, [status(thm)], [d54,c43])).
% 19.86/7.92 cnf(d56, plain, gt(succ(X0),n0) | ~leq(sK189,X0), inference(resolution, [status(thm)], [d55,c47])).
% 19.86/7.92 cnf(d57, plain, gt(n0,n0) | ~leq(sK189,'tptp$uminus$u1'), inference(superposition, [status(thm)], [c123,d56])).
% 19.86/7.92 cnf(d58, plain, ~leq(sK189,'tptp$uminus$u1'), inference(resolution, [status(thm)], [c34,d57])).
% 19.86/7.92 cnf(d59, plain, $false, inference(resolution, [status(thm)], [d58,d51])).
% 19.86/7.92 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------