%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWX240_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:15:44 AM UTC 2026
% Result : Theorem 35.39s 7.18s
% Output : CNFRefutation 35.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 56 ( 18 unt; 0 def)
% Number of atoms : 129 ( 23 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 131 ( 58 ~; 59 |; 1 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 100 ( 12 sgn 28 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_012,axiom,
! [X0,X1] : nand(X0,X1) != tT ).
fof(axiom_016,axiom,
! [X0] : tT != var(X0) ).
fof(axiom_031,axiom,
! [X0] :
( X0 != nand(proj1Nand(X0),proj2Nand(X0))
=> ( X0 != var(proj1Var(X0))
=> ~ secret(X0) ) ) ).
fof(axiom_035,axiom,
typeCorrect(skip) ).
fof(axiom_037,axiom,
! [X0,X1] :
( typeCorrect(assign(low(X1),X0))
<=> ~ secret(X0) ) ).
fof(axiom_039,axiom,
! [X0,X1,X2] :
( typeCorrect(ifThenElse(X0,X1,X2))
<=> ( typeCorrect(X2)
& typeCorrect(X1) ) ) ).
fof(axiom_040,axiom,
l = low(zero) ).
fof(axiom_042,axiom,
! [X0] : ~ elem(X0,nil) ).
fof(axiom_043,axiom,
! [X0,X1,X2] :
( elem(X0,cons(X1,X2))
<=> ( elem(X0,X2)
| X1 = X0 ) ) ).
fof(axiom_045,axiom,
! [X0] : eval(X0,tT) ).
fof(axiom_047,axiom,
! [X0,X1] :
( eval(X0,var(X1))
<=> elem(X1,X0) ) ).
fof(axiom_051,axiom,
! [X0] : run(X0,skip) = X0 ).
fof(axiom_052,axiom,
! [X0,X1,X2] :
( eval(X0,X2)
=> run(X0,assign(X1,X2)) = cons(X1,X0) ) ).
fof(axiom_055,axiom,
! [X0,X1,X2,X3] :
( eval(X0,X1)
=> run(X0,ifThenElse(X1,X2,X3)) = run(X0,X2) ) ).
fof(axiom_056,axiom,
! [X0,X1,X2,X3] :
( ~ eval(X0,X1)
=> run(X0,ifThenElse(X1,X2,X3)) = run(X0,X3) ) ).
fof(goal_057,conjecture,
? [X0,X1] :
~ ( typeCorrect(X0)
=> ( elem(l,run(X1,X0))
<=> elem(l,run(cons(h,X1),X0)) ) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1] :
~ ( typeCorrect(X0)
=> ( elem(l,run(X1,X0))
<=> elem(l,run(cons(h,X1),X0)) ) ),
inference(negate_conjecture,[status(cth)],[goal_057]) ).
cnf(c11,plain,
nand(X0,X1) != tT,
inference(clausification,[status(esa)],[axiom_012]) ).
cnf(c15,plain,
tT != var(X0),
inference(clausification,[status(esa)],[axiom_016]) ).
cnf(c30,plain,
( ~ secret(X0)
| X0 = var(proj1Var(X0))
| X0 = nand(proj1Nand(X0),proj2Nand(X0)) ),
inference(clausification,[status(esa)],[axiom_031]) ).
cnf(c36,plain,
typeCorrect(skip),
inference(clausification,[status(esa)],[axiom_035]) ).
cnf(c39,plain,
( secret(X1)
| typeCorrect(assign(low(X0),X1)) ),
inference(clausification,[status(esa)],[axiom_037]) ).
cnf(c45,plain,
( ~ typeCorrect(X2)
| ~ typeCorrect(X1)
| typeCorrect(ifThenElse(X0,X1,X2)) ),
inference(clausification,[status(esa)],[axiom_039]) ).
cnf(c46,plain,
l = low(zero),
inference(clausification,[status(esa)],[axiom_040]) ).
cnf(c48,plain,
~ elem(X0,nil),
inference(clausification,[status(esa)],[axiom_042]) ).
cnf(c50,plain,
( X1 != X0
| elem(X0,cons(X1,X2)) ),
inference(clausification,[status(esa)],[axiom_043]) ).
cnf(c55,plain,
eval(X0,tT),
inference(clausification,[status(esa)],[axiom_045]) ).
cnf(c57,plain,
( elem(X1,X0)
| ~ eval(X0,var(X1)) ),
inference(clausification,[status(esa)],[axiom_047]) ).
cnf(c58,plain,
( ~ elem(X1,X0)
| eval(X0,var(X1)) ),
inference(clausification,[status(esa)],[axiom_047]) ).
cnf(c62,plain,
run(X0,skip) = X0,
inference(clausification,[status(esa)],[axiom_051]) ).
cnf(c63,plain,
( run(X0,assign(X2,X1)) = cons(X2,X0)
| ~ eval(X0,X1) ),
inference(clausification,[status(esa)],[axiom_052]) ).
cnf(c66,plain,
( run(X0,ifThenElse(X1,X2,X3)) = run(X0,X2)
| ~ eval(X0,X1) ),
inference(clausification,[status(esa)],[axiom_055]) ).
cnf(c67,plain,
( run(X0,ifThenElse(X1,X2,X3)) = run(X0,X3)
| eval(X0,X1) ),
inference(clausification,[status(esa)],[axiom_056]) ).
cnf(c69,plain,
( ~ elem(l,run(cons(h,X1),X0))
| elem(l,run(X1,X0))
| ~ typeCorrect(X0) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( secret(X0)
| typeCorrect(assign(l,X0)) ),
inference(superposition,[status(thm)],[c46,c39]) ).
cnf(d1,plain,
elem(X0,cons(X0,X1)),
inference(equality_resolution,[status(thm)],[c50]) ).
cnf(d2,plain,
( ~ eval(cons(h,X0),X2)
| elem(l,run(X0,assign(X1,X2)))
| ~ typeCorrect(assign(X1,X2))
| ~ elem(l,cons(X1,cons(h,X0))) ),
inference(superposition,[status(thm)],[c63,c69]) ).
cnf(d3,plain,
( ~ eval(cons(h,X1),X0)
| elem(l,run(X1,assign(l,X0)))
| ~ typeCorrect(assign(l,X0)) ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( elem(l,run(X1,assign(l,X0)))
| ~ typeCorrect(assign(l,X0))
| ~ eval(cons(h,cons(h,X1)),X0)
| ~ typeCorrect(assign(l,X0)) ),
inference(resolution,[status(thm)],[d3,c69]) ).
cnf(d5,plain,
( elem(l,run(X0,assign(l,tT)))
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[d4,c55]) ).
cnf(d6,plain,
( ~ eval(cons(h,X0),X1)
| elem(l,run(X0,ifThenElse(X1,X2,X3)))
| ~ typeCorrect(ifThenElse(X1,X2,X3))
| ~ elem(l,run(cons(h,X0),X2)) ),
inference(superposition,[status(thm)],[c66,c69]) ).
cnf(d7,plain,
( eval(X0,X1)
| ~ eval(cons(h,X0),X1)
| ~ elem(l,run(cons(h,X0),X2))
| ~ typeCorrect(ifThenElse(X1,X2,X3))
| elem(l,run(X0,X3)) ),
inference(superposition,[status(thm)],[c67,d6]) ).
cnf(d8,plain,
( ~ typeCorrect(assign(l,tT))
| ~ eval(cons(h,X2),X0)
| eval(X2,X0)
| elem(l,run(X2,X1))
| ~ typeCorrect(ifThenElse(X0,assign(l,tT),X1)) ),
inference(resolution,[status(thm)],[d7,d5]) ).
cnf(d9,plain,
( ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(X1)
| ~ eval(cons(h,X0),X2)
| eval(X0,X2)
| elem(l,run(X0,X1))
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[d8,c45]) ).
cnf(d10,plain,
( ~ elem(X2,cons(h,X1))
| eval(X1,var(X2))
| elem(l,run(X1,X0))
| ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(X0) ),
inference(resolution,[status(thm)],[d9,c58]) ).
cnf(d11,plain,
( eval(X1,var(h))
| elem(l,run(X1,X0))
| ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(X0) ),
inference(resolution,[status(thm)],[d10,d1]) ).
cnf(d12,plain,
( eval(X0,var(h))
| ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(skip)
| elem(l,X0) ),
inference(superposition,[status(thm)],[c62,d11]) ).
cnf(d13,plain,
( eval(X0,var(h))
| elem(l,X0)
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[c36,d12]) ).
cnf(d14,plain,
( secret(tT)
| eval(X0,var(h))
| elem(l,X0) ),
inference(resolution,[status(thm)],[d13,d0]) ).
cnf(d15,plain,
( ~ secret(X0)
| X0 = var(proj1Var(X0))
| X0 != tT ),
inference(superposition,[status(thm)],[c30,c11]) ).
cnf(d16,plain,
( ~ secret(tT)
| tT = var(proj1Var(tT)) ),
inference(equality_resolution,[status(thm)],[d15]) ).
cnf(d17,plain,
~ secret(tT),
inference(resolution,[status(thm)],[c15,d16]) ).
cnf(d18,plain,
( eval(X0,var(h))
| elem(l,X0) ),
inference(resolution,[status(thm)],[d17,d14]) ).
cnf(d19,plain,
( elem(h,X0)
| elem(l,X0) ),
inference(resolution,[status(thm)],[d18,c57]) ).
cnf(d20,plain,
elem(l,nil),
inference(resolution,[status(thm)],[d19,c48]) ).
cnf(d21,plain,
$false,
inference(resolution,[status(thm)],[c48,d20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX240_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.38 % Computer : n026.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sat Sep 26 17:04:41 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 35.39/7.18 % SZS status Theorem for theBenchmark.p
% 35.39/7.18 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------