%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR014+1 : TPTP v9.3.1. Bugfixed v3.1.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 07:03:41 AM UTC 2026
% Result : Theorem 16.28s 7.41s
% Output : CNFRefutation 16.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 31 ( 21 unt; 0 def)
% Number of atoms : 45 ( 15 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 36 ( 22 ~; 9 |; 3 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 25 ( 6 sgn 8 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(plus0_1,axiom,
plus(n0,n1) = n1 ).
fof(plus1_1,axiom,
plus(n1,n1) = n2 ).
fof(plus1_2,axiom,
plus(n1,n2) = n3 ).
fof(symmetry_of_plus,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0) ).
fof(not_released_filling_0,hypothesis,
~ releasedAt(filling,n0) ).
fof(keep_not_released,axiom,
! [X0,X1] :
( ( ~ ? [X2] :
( releases(X2,X0,X1)
& happens(X2,X1) )
& ~ releasedAt(X0,X1) )
=> ~ releasedAt(X0,plus(X1,n1)) ) ).
fof(releases_all_defn,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X1 = waterLevel(X3)
& X0 = tapOn ) ) ).
fof(filling_not_waterLevel,axiom,
! [X0] : filling != waterLevel(X0) ).
fof(filling_3_l1,conjecture,
~ releasedAt(filling,n3) ).
fof(negated_conjecture,negated_conjecture,
~ ~ releasedAt(filling,n3),
inference(negate_conjecture,[status(cth)],[filling_3_l1]) ).
cnf(c1,plain,
plus(n0,n1) = n1,
inference(clausification,[status(esa)],[plus0_1]) ).
cnf(c4,plain,
plus(n1,n1) = n2,
inference(clausification,[status(esa)],[plus1_1]) ).
cnf(c5,plain,
plus(n1,n2) = n3,
inference(clausification,[status(esa)],[plus1_2]) ).
cnf(c10,plain,
plus(X0,X1) = plus(X1,X0),
inference(clausification,[status(esa)],[symmetry_of_plus]) ).
cnf(c40,plain,
~ releasedAt(filling,n0),
inference(clausification,[status(esa)],[not_released_filling_0]) ).
cnf(c65,plain,
( ~ releasedAt(X0,plus(X1,n1))
| releases(sK54(X0,X1),X0,X1)
| releasedAt(X0,X1) ),
inference(clausification,[status(esa)],[keep_not_released]) ).
cnf(c98,plain,
( X1 = waterLevel(sK84(X0,X1))
| ~ releases(X0,X1,X2) ),
inference(clausification,[status(esa)],[releases_all_defn]) ).
cnf(c113,plain,
filling != waterLevel(X0),
inference(clausification,[status(esa)],[filling_not_waterLevel]) ).
cnf(c118,plain,
releasedAt(filling,n3),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ releases(X0,X1,X2)
| filling != X1 ),
inference(superposition,[status(thm)],[c98,c113]) ).
cnf(d1,plain,
~ releases(X0,filling,X1),
inference(equality_resolution,[status(thm)],[d0]) ).
cnf(d2,plain,
( ~ releasedAt(filling,plus(X0,n1))
| releasedAt(filling,X0) ),
inference(resolution,[status(thm)],[d1,c65]) ).
cnf(d3,plain,
( releasedAt(filling,X0)
| ~ releasedAt(filling,plus(n1,X0)) ),
inference(superposition,[status(thm)],[c10,d2]) ).
cnf(d4,plain,
( releasedAt(filling,n2)
| ~ releasedAt(filling,n3) ),
inference(superposition,[status(thm)],[c5,d3]) ).
cnf(d5,plain,
releasedAt(filling,n2),
inference(resolution,[status(thm)],[c118,d4]) ).
cnf(d6,plain,
( releasedAt(filling,n1)
| ~ releasedAt(filling,n2) ),
inference(superposition,[status(thm)],[c4,d2]) ).
cnf(d7,plain,
plus(n1,n0) = n1,
inference(demodulation,[status(thm)],[c1,c10]) ).
cnf(d8,plain,
( releasedAt(filling,n0)
| ~ releasedAt(filling,n1) ),
inference(superposition,[status(thm)],[d7,d3]) ).
cnf(d9,plain,
~ releasedAt(filling,n1),
inference(resolution,[status(thm)],[c40,d8]) ).
cnf(d10,plain,
~ releasedAt(filling,n2),
inference(resolution,[status(thm)],[d9,d6]) ).
cnf(d11,plain,
$false,
inference(resolution,[status(thm)],[d10,d5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR014+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/5.31 % Computer : n012.cluster.edu
% 0.03/5.31 % Model : x86_64 x86_64
% 0.03/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.31 % Memory : 8046.5625MB
% 0.03/5.31 % OS : Linux 6.8.0-71-generic
% 0.03/5.31 % CPULimit : 300
% 0.03/5.31 % WCLimit : 300
% 0.03/5.32 % DateTime : Sat Sep 26 23:55:40 UTC 2026
% 0.03/5.32 % CPUTime :
% 0.03/5.32 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.28/7.41 % SZS status Theorem for theBenchmark.p
% 16.28/7.41 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------