%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWX241_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 17.02s 4.65s
% Output : CNFRefutation 17.02s
% 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_037,axiom,
! [X0] :
( X0 != nand(proj1Nand(X0),proj2Nand(X0))
=> ( X0 != var(proj1Var(X0))
=> ~ secret(X0) ) ) ).
fof(axiom_041,axiom,
typeCorrect(skip) ).
fof(axiom_043,axiom,
! [X0,X1] :
( typeCorrect(assign(low(X1),X0))
<=> ~ secret(X0) ) ).
fof(axiom_045,axiom,
! [X0,X1,X2] :
( typeCorrect(ifThenElse(X0,X1,X2))
<=> ( typeCorrect(X2)
& typeCorrect(X1) ) ) ).
fof(axiom_047,axiom,
l = low(zero) ).
fof(axiom_049,axiom,
! [X0] : ~ elem(X0,nil) ).
fof(axiom_050,axiom,
! [X0,X1,X2] :
( elem(X0,cons(X1,X2))
<=> ( elem(X0,X2)
| X1 = X0 ) ) ).
fof(axiom_052,axiom,
! [X0] : eval(X0,tT) ).
fof(axiom_054,axiom,
! [X0,X1] :
( eval(X0,var(X1))
<=> elem(X1,X0) ) ).
fof(axiom_058,axiom,
! [X0] : run(X0,skip) = X0 ).
fof(axiom_059,axiom,
! [X0,X1,X2] :
( eval(X0,X2)
=> run(X0,assign(X1,X2)) = cons(X1,X0) ) ).
fof(axiom_062,axiom,
! [X0,X1,X2,X3] :
( eval(X0,X1)
=> run(X0,ifThenElse(X1,X2,X3)) = run(X0,X2) ) ).
fof(axiom_063,axiom,
! [X0,X1,X2,X3] :
( ~ eval(X0,X1)
=> run(X0,ifThenElse(X1,X2,X3)) = run(X0,X3) ) ).
fof(goal_065,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_065]) ).
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(c36,plain,
( ~ secret(X0)
| X0 = var(proj1Var(X0))
| X0 = nand(proj1Nand(X0),proj2Nand(X0)) ),
inference(clausification,[status(esa)],[axiom_037]) ).
cnf(c42,plain,
typeCorrect(skip),
inference(clausification,[status(esa)],[axiom_041]) ).
cnf(c45,plain,
( secret(X1)
| typeCorrect(assign(low(X0),X1)) ),
inference(clausification,[status(esa)],[axiom_043]) ).
cnf(c51,plain,
( ~ typeCorrect(X2)
| ~ typeCorrect(X1)
| typeCorrect(ifThenElse(X0,X1,X2)) ),
inference(clausification,[status(esa)],[axiom_045]) ).
cnf(c54,plain,
l = low(zero),
inference(clausification,[status(esa)],[axiom_047]) ).
cnf(c56,plain,
~ elem(X0,nil),
inference(clausification,[status(esa)],[axiom_049]) ).
cnf(c58,plain,
( X1 != X0
| elem(X0,cons(X1,X2)) ),
inference(clausification,[status(esa)],[axiom_050]) ).
cnf(c63,plain,
eval(X0,tT),
inference(clausification,[status(esa)],[axiom_052]) ).
cnf(c65,plain,
( elem(X1,X0)
| ~ eval(X0,var(X1)) ),
inference(clausification,[status(esa)],[axiom_054]) ).
cnf(c66,plain,
( ~ elem(X1,X0)
| eval(X0,var(X1)) ),
inference(clausification,[status(esa)],[axiom_054]) ).
cnf(c70,plain,
run(X0,skip) = X0,
inference(clausification,[status(esa)],[axiom_058]) ).
cnf(c71,plain,
( run(X0,assign(X2,X1)) = cons(X2,X0)
| ~ eval(X0,X1) ),
inference(clausification,[status(esa)],[axiom_059]) ).
cnf(c74,plain,
( run(X0,ifThenElse(X1,X2,X3)) = run(X0,X2)
| ~ eval(X0,X1) ),
inference(clausification,[status(esa)],[axiom_062]) ).
cnf(c75,plain,
( run(X0,ifThenElse(X1,X2,X3)) = run(X0,X3)
| eval(X0,X1) ),
inference(clausification,[status(esa)],[axiom_063]) ).
cnf(c78,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)],[c54,c45]) ).
cnf(d1,plain,
elem(X0,cons(X0,X1)),
inference(equality_resolution,[status(thm)],[c58]) ).
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)],[c71,c78]) ).
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,c78]) ).
cnf(d5,plain,
( elem(l,run(X0,assign(l,tT)))
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[d4,c63]) ).
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)],[c74,c78]) ).
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)],[c75,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,c51]) ).
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,c66]) ).
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)],[c70,d11]) ).
cnf(d13,plain,
( eval(X0,var(h))
| elem(l,X0)
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[c42,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)],[c36,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,c65]) ).
cnf(d20,plain,
elem(l,nil),
inference(resolution,[status(thm)],[d19,c56]) ).
cnf(d21,plain,
$false,
inference(resolution,[status(thm)],[c56,d20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX241_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 17:04:37 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.11/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.02/4.65 % SZS status Theorem for theBenchmark.p
% 17.02/4.65 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------