%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : HWV005-2 : TPTP v9.3.1. Bugfixed v2.7.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 07:32:51 AM UTC 2026
% Result : Unsatisfiable 20.79s 3.05s
% Output : CNFRefutation 20.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 25
% Syntax : Number of clauses : 79 ( 16 unt; 19 nHn; 79 RR)
% Number of literals : 230 ( 0 equ; 137 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-1 aty)
% Number of variables : 62 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(h_isa_halfadder,hypothesis,
halfadder(h) ).
cnf(in1_1,hypothesis,
one(in1(h)) ).
cnf(outs_0,hypothesis,
zero(outs(h)) ).
cnf(outc_0,hypothesis,
zero(outc(h)) ).
cnf(diagnosis_and1,negated_conjecture,
~ abnormal(and1(h)) ).
cnf(diagnosis_not1,negated_conjecture,
~ abnormal(not1(h)) ).
cnf(diagnosis_or1,negated_conjecture,
~ abnormal(or1(h)) ).
cnf(value_propagation_zero1,axiom,
( zero(X1)
| ~ zero(X0)
| ~ connection(X0,X1) ) ).
cnf(value_propagation_one1,axiom,
( one(X1)
| ~ one(X0)
| ~ connection(X0,X1) ) ).
cnf(unique_value,axiom,
( ~ one(X0)
| ~ zero(X0) ) ).
cnf(and_0_00,axiom,
( zero(in2(X0))
| zero(in1(X0))
| ~ zero(out1(X0))
| ~ 'and$uok'(X0) ) ).
cnf(and_ok_or_abnormal,axiom,
( abnormal(X0)
| 'and$uok'(X0)
| ~ 'logic$uand'(X0) ) ).
cnf(or_1x_1,axiom,
( one(out1(X0))
| ~ one(in1(X0))
| ~ 'or$uok'(X0) ) ).
cnf(or_ok_or_abnormal,axiom,
( abnormal(X0)
| 'or$uok'(X0)
| ~ 'logic$uor'(X0) ) ).
cnf(not_0_1_fw,axiom,
( one(out1(X0))
| ~ zero(in1(X0))
| ~ 'not$uok'(X0) ) ).
cnf(not_ok_or_abnormal,axiom,
( abnormal(X0)
| 'not$uok'(X0)
| ~ 'logic$unot'(X0) ) ).
cnf(halfadder_and1,axiom,
( 'logic$uand'(and1(X0))
| ~ halfadder(X0) ) ).
cnf(halfadder_not1,axiom,
( 'logic$unot'(not1(X0))
| ~ halfadder(X0) ) ).
cnf(halfadder_or1,axiom,
( 'logic$uor'(or1(X0))
| ~ halfadder(X0) ) ).
cnf(halfadder_connection_in1_in1or1,axiom,
( connection(in1(X0),in1(or1(X0)))
| ~ halfadder(X0) ) ).
cnf(halfadder_connection_outs_out1and1,axiom,
( connection(outs(X0),out1(and1(X0)))
| ~ halfadder(X0) ) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( connection(outc(X0),out1(and2(X0)))
| ~ halfadder(X0) ) ).
cnf(halfadder_connection_out1or1_in1_and1,axiom,
( connection(out1(or1(X0)),in1(and1(X0)))
| ~ halfadder(X0) ) ).
cnf(halfadder_connection_out1and2_in1not1,axiom,
( connection(out1(and2(X0)),in1(not1(X0)))
| ~ halfadder(X0) ) ).
cnf(halfadder_connection_out1not1_in2and1,axiom,
( connection(out1(not1(X0)),in2(and1(X0)))
| ~ halfadder(X0) ) ).
cnf(c0,plain,
halfadder(h),
inference(clausification,[status(esa)],[h_isa_halfadder]) ).
cnf(c1,plain,
one(in1(h)),
inference(clausification,[status(esa)],[in1_1]) ).
cnf(c3,plain,
zero(outs(h)),
inference(clausification,[status(esa)],[outs_0]) ).
cnf(c4,plain,
zero(outc(h)),
inference(clausification,[status(esa)],[outc_0]) ).
cnf(c5,plain,
~ abnormal(and1(h)),
inference(clausification,[status(esa)],[diagnosis_and1]) ).
cnf(c6,plain,
~ abnormal(not1(h)),
inference(clausification,[status(esa)],[diagnosis_not1]) ).
cnf(c7,plain,
~ abnormal(or1(h)),
inference(clausification,[status(esa)],[diagnosis_or1]) ).
cnf(c8,plain,
( zero(X1)
| ~ zero(X0)
| ~ connection(X0,X1) ),
inference(clausification,[status(esa)],[value_propagation_zero1]) ).
cnf(c9,plain,
( one(X1)
| ~ one(X0)
| ~ connection(X0,X1) ),
inference(clausification,[status(esa)],[value_propagation_one1]) ).
cnf(c12,plain,
( ~ one(X0)
| ~ zero(X0) ),
inference(clausification,[status(esa)],[unique_value]) ).
cnf(c16,plain,
( zero(in2(X0))
| zero(in1(X0))
| ~ zero(out1(X0))
| ~ 'and$uok'(X0) ),
inference(clausification,[status(esa)],[and_0_00]) ).
cnf(c20,plain,
( abnormal(X0)
| 'and$uok'(X0)
| ~ 'logic$uand'(X0) ),
inference(clausification,[status(esa)],[and_ok_or_abnormal]) ).
cnf(c21,plain,
( one(out1(X0))
| ~ one(in1(X0))
| ~ 'or$uok'(X0) ),
inference(clausification,[status(esa)],[or_1x_1]) ).
cnf(c28,plain,
( abnormal(X0)
| 'or$uok'(X0)
| ~ 'logic$uor'(X0) ),
inference(clausification,[status(esa)],[or_ok_or_abnormal]) ).
cnf(c29,plain,
( one(out1(X0))
| ~ zero(in1(X0))
| ~ 'not$uok'(X0) ),
inference(clausification,[status(esa)],[not_0_1_fw]) ).
cnf(c34,plain,
( abnormal(X0)
| 'not$uok'(X0)
| ~ 'logic$unot'(X0) ),
inference(clausification,[status(esa)],[not_ok_or_abnormal]) ).
cnf(c35,plain,
( 'logic$uand'(and1(X0))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_and1]) ).
cnf(c37,plain,
( 'logic$unot'(not1(X0))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_not1]) ).
cnf(c38,plain,
( 'logic$uor'(or1(X0))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_or1]) ).
cnf(c39,plain,
( connection(in1(X0),in1(or1(X0)))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_connection_in1_in1or1]) ).
cnf(c43,plain,
( connection(outs(X0),out1(and1(X0)))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_connection_outs_out1and1]) ).
cnf(c44,plain,
( connection(outc(X0),out1(and2(X0)))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_connection_outc_out1and2]) ).
cnf(c45,plain,
( connection(out1(or1(X0)),in1(and1(X0)))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_connection_out1or1_in1_and1]) ).
cnf(c46,plain,
( connection(out1(and2(X0)),in1(not1(X0)))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_connection_out1and2_in1not1]) ).
cnf(c47,plain,
( connection(out1(not1(X0)),in2(and1(X0)))
| ~ halfadder(X0) ),
inference(clausification,[status(esa)],[halfadder_connection_out1not1_in2and1]) ).
cnf(d0,plain,
( ~ halfadder(X0)
| 'and$uok'(and1(X0))
| abnormal(and1(X0)) ),
inference(resolution,[status(thm)],[c20,c35]) ).
cnf(d1,plain,
( ~ halfadder(X0)
| 'or$uok'(or1(X0))
| abnormal(or1(X0)) ),
inference(resolution,[status(thm)],[c28,c38]) ).
cnf(d2,plain,
( ~ halfadder(X0)
| 'not$uok'(not1(X0))
| abnormal(not1(X0)) ),
inference(resolution,[status(thm)],[c34,c37]) ).
cnf(d3,plain,
( ~ one(out1(or1(X0)))
| one(in1(and1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[c45,c9]) ).
cnf(d4,plain,
( ~ one(in1(X0))
| one(in1(or1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[c39,c9]) ).
cnf(d5,plain,
( ~ 'or$uok'(or1(X0))
| one(out1(or1(X0)))
| ~ one(in1(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d4,c21]) ).
cnf(d6,plain,
( one(in1(and1(X0)))
| ~ halfadder(X0)
| ~ 'or$uok'(or1(X0))
| ~ one(in1(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d5,d3]) ).
cnf(d7,plain,
( ~ zero(outs(X0))
| zero(out1(and1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[c43,c8]) ).
cnf(d8,plain,
( ~ 'and$uok'(and1(X0))
| zero(in2(and1(X0)))
| zero(in1(and1(X0)))
| ~ zero(outs(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d7,c16]) ).
cnf(d9,plain,
( ~ one(in2(and1(X0)))
| ~ 'and$uok'(and1(X0))
| ~ zero(outs(X0))
| zero(in1(and1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d8,c12]) ).
cnf(d10,plain,
( ~ one(out1(not1(X0)))
| one(in2(and1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[c47,c9]) ).
cnf(d11,plain,
( ~ zero(outc(X0))
| zero(out1(and2(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[c44,c8]) ).
cnf(d12,plain,
( ~ zero(out1(and2(X0)))
| zero(in1(not1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[c46,c8]) ).
cnf(d13,plain,
( ~ zero(outc(X0))
| ~ halfadder(X0)
| zero(in1(not1(X0)))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d12,d11]) ).
cnf(d14,plain,
( ~ 'not$uok'(not1(X0))
| one(out1(not1(X0)))
| ~ zero(outc(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d13,c29]) ).
cnf(d15,plain,
( one(in2(and1(X0)))
| ~ halfadder(X0)
| ~ 'not$uok'(not1(X0))
| ~ zero(outc(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d14,d10]) ).
cnf(d16,plain,
( ~ 'and$uok'(and1(X0))
| ~ zero(outs(X0))
| zero(in1(and1(X0)))
| ~ halfadder(X0)
| ~ 'not$uok'(not1(X0))
| ~ zero(outc(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d15,d9]) ).
cnf(d17,plain,
( ~ one(in1(and1(X0)))
| ~ 'not$uok'(not1(X0))
| ~ 'and$uok'(and1(X0))
| ~ zero(outc(X0))
| ~ zero(outs(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d16,c12]) ).
cnf(d18,plain,
( ~ 'or$uok'(or1(X0))
| ~ one(in1(X0))
| ~ halfadder(X0)
| ~ 'not$uok'(not1(X0))
| ~ 'and$uok'(and1(X0))
| ~ zero(outc(X0))
| ~ zero(outs(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d17,d6]) ).
cnf(d19,plain,
( abnormal(not1(X0))
| ~ halfadder(X0)
| ~ 'or$uok'(or1(X0))
| ~ 'and$uok'(and1(X0))
| ~ zero(outc(X0))
| ~ zero(outs(X0))
| ~ one(in1(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d18,d2]) ).
cnf(d20,plain,
( abnormal(or1(X0))
| ~ halfadder(X0)
| ~ 'and$uok'(and1(X0))
| abnormal(not1(X0))
| ~ zero(outc(X0))
| ~ zero(outs(X0))
| ~ one(in1(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d19,d1]) ).
cnf(d21,plain,
( abnormal(and1(X0))
| ~ halfadder(X0)
| abnormal(or1(X0))
| abnormal(not1(X0))
| ~ zero(outc(X0))
| ~ zero(outs(X0))
| ~ one(in1(X0))
| ~ halfadder(X0) ),
inference(resolution,[status(thm)],[d20,d0]) ).
cnf(d22,plain,
( abnormal(or1(h))
| abnormal(not1(h))
| abnormal(and1(h))
| ~ zero(outs(h))
| ~ one(in1(h))
| ~ halfadder(h) ),
inference(resolution,[status(thm)],[d21,c4]) ).
cnf(d23,plain,
( abnormal(or1(h))
| abnormal(not1(h))
| abnormal(and1(h))
| ~ zero(outs(h))
| ~ one(in1(h)) ),
inference(resolution,[status(thm)],[c0,d22]) ).
cnf(d24,plain,
( abnormal(or1(h))
| abnormal(not1(h))
| abnormal(and1(h))
| ~ zero(outs(h)) ),
inference(resolution,[status(thm)],[c1,d23]) ).
cnf(d25,plain,
( abnormal(or1(h))
| abnormal(not1(h))
| abnormal(and1(h)) ),
inference(resolution,[status(thm)],[c3,d24]) ).
cnf(d26,plain,
( abnormal(or1(h))
| abnormal(not1(h)) ),
inference(resolution,[status(thm)],[c5,d25]) ).
cnf(d27,plain,
abnormal(or1(h)),
inference(resolution,[status(thm)],[c6,d26]) ).
cnf(d28,plain,
$false,
inference(resolution,[status(thm)],[c7,d27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV005-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 16:02:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.79/3.05 % SZS status Unsatisfiable for theBenchmark.p
% 20.79/3.05 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------