%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV050+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:19 AM UTC 2026
% Result : Theorem 4.29s 4.09s
% Output : CNFRefutation 4.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 40 ( 27 unt; 0 def)
% Number of atoms : 69 ( 68 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 63 ( 34 ~; 21 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 16 con; 0-3 aty)
% Number of variables : 6 ( 1 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(successor_4,axiom,
succ(succ(succ(succ(n0)))) = n4 ).
fof(successor_5,axiom,
succ(succ(succ(succ(succ(n0))))) = n5 ).
fof(successor_1,axiom,
succ(n0) = n1 ).
fof(sum_plus_base,axiom,
! [X0] : sum(n0,'tptp$uminus$u1',X0) = n0 ).
fof(succ_tptp_minus_1,axiom,
succ('tptp$uminus$u1') = n0 ).
fof(pred_minus_1,axiom,
! [X0] : minus(X0,n1) = pred(X0) ).
fof(pred_succ,axiom,
! [X0] : pred(succ(X0)) = X0 ).
fof(cl5_nebula_norm_0022,conjecture,
( ( pv88 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
& pv86 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87))))) )
=> ( pv88 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
& pv86 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
& n0 = sum(n0,minus(n0,n1),divide(abs(minus('a$uselect2'(sigma,pv91),'a$uselect2'(sigmaold,pv91))),plus(abs('a$uselect2'(sigma,pv91)),abs('a$uselect2'(sigmaold,pv91))))) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ( ( pv88 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
& pv86 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87))))) )
=> ( pv88 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
& pv86 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
& n0 = sum(n0,minus(n0,n1),divide(abs(minus('a$uselect2'(sigma,pv91),'a$uselect2'(sigmaold,pv91))),plus(abs('a$uselect2'(sigma,pv91)),abs('a$uselect2'(sigmaold,pv91))))) ) ),
inference(negate_conjecture,[status(cth)],[cl5_nebula_norm_0022]) ).
cnf(c27,plain,
succ(succ(succ(succ(n0)))) = n4,
inference(clausification,[status(esa)],[successor_4]) ).
cnf(c28,plain,
succ(succ(succ(succ(succ(n0))))) = n5,
inference(clausification,[status(esa)],[successor_5]) ).
cnf(c29,plain,
succ(n0) = n1,
inference(clausification,[status(esa)],[successor_1]) ).
cnf(c121,plain,
sum(n0,'tptp$uminus$u1',X0) = n0,
inference(clausification,[status(esa)],[sum_plus_base]) ).
cnf(c123,plain,
succ('tptp$uminus$u1') = n0,
inference(clausification,[status(esa)],[succ_tptp_minus_1]) ).
cnf(c134,plain,
minus(X0,n1) = pred(X0),
inference(clausification,[status(esa)],[pred_minus_1]) ).
cnf(c135,plain,
pred(succ(X0)) = X0,
inference(clausification,[status(esa)],[pred_succ]) ).
cnf(c156,plain,
pv86 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c157,plain,
pv88 = sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89))))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c158,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
| n0 != sum(n0,minus(n0,n1),divide(abs(minus('a$uselect2'(sigma,pv91),'a$uselect2'(sigmaold,pv91))),plus(abs('a$uselect2'(sigma,pv91)),abs('a$uselect2'(sigmaold,pv91))))) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
succ(succ(succ(n1))) = n4,
inference(demodulation,[status(thm)],[c27,c29]) ).
cnf(d1,plain,
succ(succ(succ(succ(n1)))) = n5,
inference(demodulation,[status(thm)],[c28,c29]) ).
cnf(d2,plain,
succ(n4) = n5,
inference(demodulation,[status(thm)],[d1,d0]) ).
cnf(d3,plain,
pred(n5) = n4,
inference(superposition,[status(thm)],[d2,c135]) ).
cnf(d4,plain,
pv88 = sum(n0,pred(n5),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89))))),
inference(demodulation,[status(thm)],[c157,c134]) ).
cnf(d5,plain,
pv88 = sum(n0,n4,divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89))))),
inference(demodulation,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
pv86 = sum(n0,pred(n5),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87))))),
inference(demodulation,[status(thm)],[c156,c134]) ).
cnf(d7,plain,
pv86 = sum(n0,n4,divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87))))),
inference(demodulation,[status(thm)],[d6,d3]) ).
cnf(d8,plain,
pred(n0) = 'tptp$uminus$u1',
inference(superposition,[status(thm)],[c123,c135]) ).
cnf(d9,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
| n0 != sum(n0,pred(n0),divide(abs(minus('a$uselect2'(sigma,pv91),'a$uselect2'(sigmaold,pv91))),plus(abs('a$uselect2'(sigma,pv91)),abs('a$uselect2'(sigmaold,pv91))))) ),
inference(demodulation,[status(thm)],[c158,c134]) ).
cnf(d10,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
| n0 != sum(n0,'tptp$uminus$u1',divide(abs(minus('a$uselect2'(sigma,pv91),'a$uselect2'(sigmaold,pv91))),plus(abs('a$uselect2'(sigma,pv91)),abs('a$uselect2'(sigmaold,pv91))))) ),
inference(demodulation,[status(thm)],[d9,d8]) ).
cnf(d11,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
| n0 != n0 ),
inference(demodulation,[status(thm)],[d10,c121]) ).
cnf(d12,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != sum(n0,pred(n5),divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
| n0 != n0 ),
inference(demodulation,[status(thm)],[d11,c134]) ).
cnf(d13,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != sum(n0,n4,divide(abs(minus('a$uselect2'(mu,pv87),'a$uselect2'(muold,pv87))),plus(abs('a$uselect2'(mu,pv87)),abs('a$uselect2'(muold,pv87)))))
| n0 != n0 ),
inference(demodulation,[status(thm)],[d12,d3]) ).
cnf(d14,plain,
( pv88 != sum(n0,minus(n5,n1),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != pv86
| n0 != n0 ),
inference(demodulation,[status(thm)],[d13,d7]) ).
cnf(d15,plain,
( pv88 != sum(n0,pred(n5),divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != pv86
| n0 != n0 ),
inference(demodulation,[status(thm)],[d14,c134]) ).
cnf(d16,plain,
( pv88 != sum(n0,n4,divide(abs(minus('a$uselect2'(rho,pv89),'a$uselect2'(rhoold,pv89))),plus(abs('a$uselect2'(rho,pv89)),abs('a$uselect2'(rhoold,pv89)))))
| pv86 != pv86
| n0 != n0 ),
inference(demodulation,[status(thm)],[d15,d3]) ).
cnf(d17,plain,
( pv88 != pv88
| pv86 != pv86
| n0 != n0 ),
inference(demodulation,[status(thm)],[d16,d5]) ).
cnf(d18,plain,
( pv86 != pv86
| n0 != n0 ),
inference(equality_resolution,[status(thm)],[d17]) ).
cnf(d19,plain,
n0 != n0,
inference(equality_resolution,[status(thm)],[d18]) ).
cnf(d20,plain,
$false,
inference(equality_resolution,[status(thm)],[d19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV050+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.17/0.45 % Computer : n005.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Sat Sep 26 13:09:02 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/4.09 % SZS status Theorem for theBenchmark.p
% 4.29/4.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------