%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV042+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 : n005.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 139.79s 23.83s
% Output : CNFRefutation 139.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV042+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n005.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 13:09:34 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.79/23.83 % SZS status Theorem for theBenchmark.p
% 139.79/23.83 % SZS output start CNFRefutation for theBenchmark.p
% 139.79/23.83 fof(gt_1_0, axiom, gt(n1,n0)).
% 139.79/23.83 fof(gt_2_0, axiom, gt(n2,n0)).
% 139.79/23.83 fof(finite_domain_2, axiom, ! [X0] : (((leq(n0,X0) & leq(X0,n2)) => (X0 = n0 | (X0 = n1 | X0 = n2))))).
% 139.79/23.83 fof(successor_1, axiom, succ(n0) = n1).
% 139.79/23.83 fof(successor_2, axiom, succ(succ(n0)) = n2).
% 139.79/23.83 fof(reflexivity_leq, axiom, ! [X0] : leq(X0,X0)).
% 139.79/23.83 fof(leq_gt1, axiom, ! [X0] : ! [X1] : ((gt(X1,X0) => leq(X0,X1)))).
% 139.79/23.83 fof(gt_succ, axiom, ! [X0] : gt(succ(X0),X0)).
% 139.79/23.83 fof(succ_plus_1_l, axiom, ! [X0] : plus(n1,X0) = succ(X0)).
% 139.79/23.83 fof(pred_minus_1, axiom, ! [X0] : minus(X0,n1) = pred(X0)).
% 139.79/23.83 fof(pred_succ, axiom, ! [X0] : pred(succ(X0)) = X0).
% 139.79/23.83 fof(succ_pred, axiom, ! [X0] : succ(pred(X0)) = X0).
% 139.79/23.83 fof(gauss_init_0081, conjecture, ((! [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,minus(plus(n1,n2),n1))) => 'a$uselect2'('s$ucenter7$uinit',X3) = init)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init)))))) => (! [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)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init)))))))).
% 139.79/23.83 fof(negated_conjecture, negated_conjecture, ~(((! [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,minus(plus(n1,n2),n1))) => 'a$uselect2'('s$ucenter7$uinit',X3) = init)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init)))))) => (! [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)) & (gt(loopcounter,n1) => ('pvar1400$uinit' = init & ('pvar1401$uinit' = init & 'pvar1402$uinit' = init)))))))), inference(negate_conjecture, [status(cth)], [gauss_init_0081])).
% 139.79/23.83 cnf(c9, plain, gt(n1,n0), inference(clausification, [status(esa)], [gt_1_0])).
% 139.79/23.83 cnf(c10, plain, gt(n2,n0), inference(clausification, [status(esa)], [gt_2_0])).
% 139.79/23.83 cnf(c25, plain, X0 = n2 | X0 = n0 | ~leq(n0,X0) | ~leq(X0,n2) | X0 = n1, inference(clausification, [status(esa)], [finite_domain_2])).
% 139.79/23.83 cnf(c29, plain, succ(n0) = n1, inference(clausification, [status(esa)], [successor_1])).
% 139.79/23.83 cnf(c30, plain, succ(succ(n0)) = n2, inference(clausification, [status(esa)], [successor_2])).
% 139.79/23.83 cnf(c35, plain, leq(X0,X0), inference(clausification, [status(esa)], [reflexivity_leq])).
% 139.79/23.83 cnf(c41, plain, ~gt(X0,X1) | leq(X1,X0), inference(clausification, [status(esa)], [leq_gt1])).
% 139.79/23.83 cnf(c45, plain, gt(succ(X0),X0), inference(clausification, [status(esa)], [gt_succ])).
% 139.79/23.83 cnf(c125, plain, plus(n1,X0) = succ(X0), inference(clausification, [status(esa)], [succ_plus_1_l])).
% 139.79/23.83 cnf(c134, plain, minus(X0,n1) = pred(X0), inference(clausification, [status(esa)], [pred_minus_1])).
% 139.79/23.83 cnf(c135, plain, pred(succ(X0)) = X0, inference(clausification, [status(esa)], [pred_succ])).
% 139.79/23.83 cnf(c136, plain, succ(pred(X0)) = X0, inference(clausification, [status(esa)], [succ_pred])).
% 139.79/23.83 cnf(c156, plain, ~leq(X0,n2) | ~leq(X1,n3) | ~leq(n0,X0) | 'a$uselect3'('simplex7$uinit',X1,X0) = init | ~leq(n0,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c157, plain, ~leq(n0,X0) | ~leq(X0,n3) | 'a$uselect2'('s$uvalues7$uinit',X0) = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c158, plain, ~leq(n0,X0) | ~leq(X0,minus(plus(n1,n2),n1)) | 'a$uselect2'('s$ucenter7$uinit',X0) = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c159, plain, ~gt(loopcounter,n1) | 'pvar1400$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c160, plain, ~gt(loopcounter,n1) | 'pvar1401$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c161, plain, ~gt(loopcounter,n1) | 'pvar1402$uinit' = init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c162, plain, ~X0 | ~X1 | ~X2 | gt(loopcounter,n1), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c163, plain, ~X0 | ~X1 | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | 'pvar1400$uinit' != init | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c164, plain, X0 | leq(n0,sK188), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c165, plain, X0 | leq(sK188,n2), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c166, plain, X0 | 'a$uselect2'('s$ucenter7$uinit',sK188) != init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c167, plain, X0 | leq(n0,sK189), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c168, plain, X0 | leq(sK189,n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c169, plain, X0 | 'a$uselect2'('s$uvalues7$uinit',sK189) != init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c170, plain, X0 | leq(n0,sK190), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c171, plain, X0 | leq(sK190,n2), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c172, plain, X0 | leq(n0,sK191), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c173, plain, X0 | leq(sK191,n3), inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(c174, plain, X0 | 'a$uselect3'('simplex7$uinit',sK191,sK190) != init, inference(clausification, [status(esa)], [negated_conjecture])).
% 139.79/23.83 cnf(d0, plain, succ(n1) = n2, inference(demodulation, [status(thm)], [c30,c29])).
% 139.79/23.83 cnf(d1, plain, pred(n2) = n1, inference(superposition, [status(thm)], [d0,c135])).
% 139.79/23.83 cnf(d2, plain, gt(X0,pred(X0)), inference(superposition, [status(thm)], [c136,c45])).
% 139.79/23.83 cnf(d3, plain, leq(pred(X0),X0), inference(resolution, [status(thm)], [c41,d2])).
% 139.79/23.83 cnf(d4, plain, 'a$uselect2'('s$ucenter7$uinit',pred(minus(plus(n1,n2),n1))) = init | ~leq(n0,pred(minus(plus(n1,n2),n1))), inference(resolution, [status(thm)], [d3,c158])).
% 139.79/23.83 cnf(d5, plain, 'a$uselect2'('s$ucenter7$uinit',pred(minus(succ(n2),n1))) = init | ~leq(n0,pred(minus(plus(n1,n2),n1))), inference(demodulation, [status(thm)], [d4,c125])).
% 139.79/23.83 cnf(d6, plain, 'a$uselect2'('s$ucenter7$uinit',pred(minus(succ(n2),n1))) = init | ~leq(n0,pred(minus(succ(n2),n1))), inference(demodulation, [status(thm)], [d5,c125])).
% 139.79/23.83 cnf(d7, plain, 'a$uselect2'('s$ucenter7$uinit',pred(pred(succ(n2)))) = init | ~leq(n0,pred(minus(succ(n2),n1))), inference(demodulation, [status(thm)], [d6,c134])).
% 139.79/23.83 cnf(d8, plain, 'a$uselect2'('s$ucenter7$uinit',pred(n2)) = init | ~leq(n0,pred(minus(succ(n2),n1))), inference(demodulation, [status(thm)], [d7,c135])).
% 139.79/23.83 cnf(d9, plain, 'a$uselect2'('s$ucenter7$uinit',n1) = init | ~leq(n0,pred(minus(succ(n2),n1))), inference(demodulation, [status(thm)], [d8,d1])).
% 139.79/23.83 cnf(d10, plain, 'a$uselect2'('s$ucenter7$uinit',n1) = init | ~leq(n0,pred(pred(succ(n2)))), inference(demodulation, [status(thm)], [d9,c134])).
% 139.79/23.83 cnf(d11, plain, 'a$uselect2'('s$ucenter7$uinit',n1) = init | ~leq(n0,pred(n2)), inference(demodulation, [status(thm)], [d10,c135])).
% 139.79/23.83 cnf(d12, plain, 'a$uselect2'('s$ucenter7$uinit',n1) = init | ~leq(n0,n1), inference(demodulation, [status(thm)], [d11,d1])).
% 139.79/23.83 cnf(d13, plain, leq(n0,n1), inference(resolution, [status(thm)], [c41,c9])).
% 139.79/23.83 cnf(d14, plain, 'a$uselect2'('s$ucenter7$uinit',n1) = init, inference(resolution, [status(thm)], [d13,d12])).
% 139.79/23.83 cnf(d15, plain, init != init | 'Ts182' | ~leq(sK189,n3) | ~leq(n0,sK189), inference(superposition, [status(thm)], [c157,c169])).
% 139.79/23.83 cnf(d16, plain, ~leq(n0,sK189) | ~leq(sK189,n3) | 'Ts182', inference(equality_resolution, [status(thm)], [d15])).
% 139.79/23.83 cnf(d17, plain, ~leq(n0,sK189) | 'Ts182' | 'Ts182', inference(resolution, [status(thm)], [d16,c168])).
% 139.79/23.83 cnf(d18, plain, 'Ts182' | 'Ts182', inference(resolution, [status(thm)], [d17,c167])).
% 139.79/23.83 cnf(d19, plain, 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | 'pvar1402$uinit' != init | ~'Ts181' | ~'Ts183', inference(resolution, [status(thm)], [d18,c163])).
% 139.79/23.83 cnf(d20, plain, ~'Ts181' | ~'Ts183' | ~'Ts182' | 'pvar1402$uinit' = init, inference(resolution, [status(thm)], [c162,c161])).
% 139.79/23.83 cnf(d21, plain, 'pvar1402$uinit' = init | ~'Ts181' | ~'Ts183', inference(resolution, [status(thm)], [d18,d20])).
% 139.79/23.83 cnf(d22, plain, init != init | 'pvar1400$uinit' != init | 'pvar1401$uinit' != init | ~'Ts181' | ~'Ts183' | ~'Ts181' | ~'Ts183', inference(superposition, [status(thm)], [d21,d19])).
% 139.79/23.83 cnf(d23, plain, ~'Ts181' | ~'Ts183' | ~'Ts182' | 'pvar1401$uinit' = init, inference(resolution, [status(thm)], [c162,c160])).
% 139.79/23.83 cnf(d24, plain, 'pvar1401$uinit' = init | ~'Ts181' | ~'Ts183', inference(resolution, [status(thm)], [d18,d23])).
% 139.79/23.83 cnf(d25, plain, init != init | init != init | 'pvar1400$uinit' != init | ~'Ts181' | ~'Ts183' | ~'Ts181' | ~'Ts183', inference(superposition, [status(thm)], [d24,d22])).
% 139.79/23.83 cnf(d26, plain, ~'Ts181' | ~'Ts183' | ~'Ts182' | 'pvar1400$uinit' = init, inference(resolution, [status(thm)], [c162,c159])).
% 139.79/23.83 cnf(d27, plain, 'pvar1400$uinit' = init | ~'Ts181' | ~'Ts183', inference(resolution, [status(thm)], [d18,d26])).
% 139.79/23.83 cnf(d28, plain, init != init | init != init | ~'Ts181' | ~'Ts183' | ~'Ts181' | ~'Ts183', inference(superposition, [status(thm)], [d27,d25])).
% 139.79/23.83 cnf(d29, plain, ~'Ts181' | ~'Ts183', inference(equality_resolution, [status(thm)], [d28])).
% 139.79/23.83 cnf(d30, plain, init != init | 'Ts183' | ~leq(sK190,n2) | ~leq(sK191,n3) | ~leq(n0,sK190) | ~leq(n0,sK191), inference(superposition, [status(thm)], [c156,c174])).
% 139.79/23.83 cnf(d31, plain, ~leq(n0,sK190) | ~leq(n0,sK191) | ~leq(sK190,n2) | ~leq(sK191,n3) | 'Ts183', inference(equality_resolution, [status(thm)], [d30])).
% 139.79/23.83 cnf(d32, plain, ~leq(n0,sK190) | ~leq(n0,sK191) | ~leq(sK190,n2) | 'Ts183' | 'Ts183', inference(resolution, [status(thm)], [d31,c173])).
% 139.79/23.83 cnf(d33, plain, ~leq(n0,sK190) | ~leq(n0,sK191) | 'Ts183' | 'Ts183', inference(resolution, [status(thm)], [d32,c171])).
% 139.79/23.83 cnf(d34, plain, ~leq(n0,sK190) | 'Ts183' | 'Ts183', inference(resolution, [status(thm)], [d33,c172])).
% 139.79/23.83 cnf(d35, plain, 'Ts183' | 'Ts183', inference(resolution, [status(thm)], [d34,c170])).
% 139.79/23.83 cnf(d36, plain, ~'Ts181', inference(resolution, [status(thm)], [d35,d29])).
% 139.79/23.83 cnf(d37, plain, 'a$uselect2'('s$ucenter7$uinit',sK188) != init, inference(resolution, [status(thm)], [d36,c166])).
% 139.79/23.83 cnf(d38, plain, leq(n0,sK188), inference(resolution, [status(thm)], [d36,c164])).
% 139.79/23.83 cnf(d39, plain, sK188 = n0 | sK188 = n1 | sK188 = n2 | ~leq(sK188,n2), inference(resolution, [status(thm)], [c25,d38])).
% 139.79/23.83 cnf(d40, plain, leq(sK188,n2), inference(resolution, [status(thm)], [d36,c165])).
% 139.79/23.83 cnf(d41, plain, sK188 = n0 | sK188 = n1 | sK188 = n2, inference(resolution, [status(thm)], [d40,d39])).
% 139.79/23.83 cnf(d42, plain, 'a$uselect2'('s$ucenter7$uinit',n2) != init | sK188 = n0 | sK188 = n1, inference(superposition, [status(thm)], [d41,d37])).
% 139.79/23.83 cnf(d43, plain, 'a$uselect2'('s$ucenter7$uinit',minus(plus(n1,n2),n1)) = init | ~leq(n0,minus(plus(n1,n2),n1)), inference(resolution, [status(thm)], [c35,c158])).
% 139.79/23.83 cnf(d44, plain, 'a$uselect2'('s$ucenter7$uinit',minus(succ(n2),n1)) = init | ~leq(n0,minus(plus(n1,n2),n1)), inference(demodulation, [status(thm)], [d43,c125])).
% 139.79/23.83 cnf(d45, plain, 'a$uselect2'('s$ucenter7$uinit',minus(succ(n2),n1)) = init | ~leq(n0,minus(succ(n2),n1)), inference(demodulation, [status(thm)], [d44,c125])).
% 139.79/23.83 cnf(d46, plain, 'a$uselect2'('s$ucenter7$uinit',pred(succ(n2))) = init | ~leq(n0,minus(succ(n2),n1)), inference(demodulation, [status(thm)], [d45,c134])).
% 139.79/23.83 cnf(d47, plain, 'a$uselect2'('s$ucenter7$uinit',n2) = init | ~leq(n0,minus(succ(n2),n1)), inference(demodulation, [status(thm)], [d46,c135])).
% 139.79/23.83 cnf(d48, plain, 'a$uselect2'('s$ucenter7$uinit',n2) = init | ~leq(n0,pred(succ(n2))), inference(demodulation, [status(thm)], [d47,c134])).
% 139.79/23.83 cnf(d49, plain, 'a$uselect2'('s$ucenter7$uinit',n2) = init | ~leq(n0,n2), inference(demodulation, [status(thm)], [d48,c135])).
% 139.79/23.83 cnf(d50, plain, leq(n0,n2), inference(resolution, [status(thm)], [c41,c10])).
% 139.79/23.83 cnf(d51, plain, 'a$uselect2'('s$ucenter7$uinit',n2) = init, inference(resolution, [status(thm)], [d50,d49])).
% 139.79/23.83 cnf(d52, plain, sK188 = n0 | sK188 = n1, inference(resolution, [status(thm)], [d51,d42])).
% 139.79/23.83 cnf(d53, plain, 'a$uselect2'('s$ucenter7$uinit',n1) != init | sK188 = n0, inference(superposition, [status(thm)], [d52,d37])).
% 139.79/23.83 cnf(d54, plain, init != init | sK188 = n0, inference(demodulation, [status(thm)], [d53,d14])).
% 139.79/23.83 cnf(d55, plain, sK188 = n0, inference(equality_resolution, [status(thm)], [d54])).
% 139.79/23.83 cnf(d56, plain, 'a$uselect2'('s$ucenter7$uinit',X0) = init | ~leq(X0,minus(succ(n2),n1)) | ~leq(n0,X0), inference(demodulation, [status(thm)], [c158,c125])).
% 139.79/23.83 cnf(d57, plain, 'a$uselect2'('s$ucenter7$uinit',X0) = init | ~leq(X0,pred(succ(n2))) | ~leq(n0,X0), inference(demodulation, [status(thm)], [d56,c134])).
% 139.79/23.83 cnf(d58, plain, 'a$uselect2'('s$ucenter7$uinit',X0) = init | ~leq(X0,n2) | ~leq(n0,X0), inference(demodulation, [status(thm)], [d57,c135])).
% 139.79/23.83 cnf(d59, plain, init != init | ~leq(sK188,n2) | ~leq(n0,sK188), inference(superposition, [status(thm)], [d58,d37])).
% 139.79/23.83 cnf(d60, plain, init != init | ~leq(n0,n0) | ~leq(sK188,n2), inference(demodulation, [status(thm)], [d59,d55])).
% 139.79/23.83 cnf(d61, plain, init != init | ~leq(n0,n0) | ~leq(n0,n2), inference(demodulation, [status(thm)], [d60,d55])).
% 139.79/23.83 cnf(d62, plain, init != init | ~leq(n0,n2), inference(resolution, [status(thm)], [c35,d61])).
% 139.79/23.83 cnf(d63, plain, init != init, inference(resolution, [status(thm)], [d50,d62])).
% 139.79/23.83 cnf(d64, plain, $false, inference(equality_resolution, [status(thm)], [d63])).
% 139.79/23.83 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------