%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV008-1.002 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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:34:17 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.41s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 29
% Syntax : Number of formulae : 118 ( 43 unt; 0 def)
% Number of atoms : 226 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 233 ( 125 ~; 108 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 87 ( 1 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(value_propagation2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( value(VAR_0,VAR_2)
| ~ value(VAR_1,VAR_2)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation2) ).
cnf(c_2,plain,
( value(A,C)
| ~ value(B,C)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation2]) ).
fof(value_propagation1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( value(VAR_1,VAR_2)
| ~ value(VAR_0,VAR_2)
| ~ connection(VAR_0,VAR_1) ),
file('theBenchmark.p',value_propagation1) ).
cnf(c_3,plain,
( value(B,C)
| ~ value(A,C)
| ~ connection(A,B) ),
inference(clausify,[status(thm)],[value_propagation1]) ).
fof(halfadder_connection_in1_in1and2,axiom,
! [VAR_0] :
( connection(in(n1,VAR_0),in(n1,and2(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_in1_in1and2) ).
cnf(c_5,plain,
( connection(in(n1,A),in(n1,and2(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_in1_in1and2]) ).
fof(halfadder_connection_outc_out1and2,axiom,
! [VAR_0] :
( connection(out(c,VAR_0),out(n1,and2(VAR_0)))
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_connection_outc_out1and2) ).
cnf(c_8,plain,
( connection(out(c,A),out(n1,and2(A)))
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_connection_outc_out1and2]) ).
fof(fulladder_connection_outch1_in2or1,axiom,
! [VAR_0] :
( connection(out(c,h1(VAR_0)),in(n2,or1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outch1_in2or1) ).
cnf(c_13,plain,
( connection(out(c,h1(A)),in(n2,or1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outch1_in2or1]) ).
fof(fulladder_connection_outch2_in1or1,axiom,
! [VAR_0] :
( connection(out(c,h2(VAR_0)),in(n1,or1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outch2_in1or1) ).
cnf(c_14,plain,
( connection(out(c,h2(A)),in(n1,or1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outch2_in1or1]) ).
fof(fulladder_connection_in1_in1h2,axiom,
! [VAR_0] :
( connection(in(n1,VAR_0),in(n1,h2(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_in1_in1h2) ).
cnf(c_15,plain,
( connection(in(n1,A),in(n1,h2(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_in1_in1h2]) ).
fof(fulladder_connection_in2_in1h1,axiom,
! [VAR_0] :
( connection(in(n2,VAR_0),in(n1,h1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_in2_in1h1) ).
cnf(c_16,plain,
( connection(in(n2,A),in(n1,h1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_in2_in1h1]) ).
fof(fulladder_connection_outc_out1or1,axiom,
! [VAR_0] :
( connection(out(c,VAR_0),out(n1,or1(VAR_0)))
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_connection_outc_out1or1) ).
cnf(c_19,plain,
( connection(out(c,A),out(n1,or1(A)))
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_connection_outc_out1or1]) ).
fof(nbit_adder_connection_outc_outcf1,axiom,
! [VAR_0] :
( connection(out(c,VAR_0),out(c,f(n2,VAR_0)))
| ~ type(VAR_0,nbit_adder(n2)) ),
file('theBenchmark.p',nbit_adder_connection_outc_outcf1) ).
cnf(c_22,plain,
( connection(out(c,A),out(c,f(n2,A)))
| ~ type(A,nbit_adder(n2)) ),
inference(clausify,[status(thm)],[nbit_adder_connection_outc_outcf1]) ).
fof(nbit_adder_connection_ina2_in1f2,axiom,
! [VAR_0] :
( connection(in(a2,VAR_0),in(n1,f(n2,VAR_0)))
| ~ type(VAR_0,nbit_adder(n2)) ),
file('theBenchmark.p',nbit_adder_connection_ina2_in1f2) ).
cnf(c_25,plain,
( connection(in(a2,A),in(n1,f(n2,A)))
| ~ type(A,nbit_adder(n2)) ),
inference(clausify,[status(thm)],[nbit_adder_connection_ina2_in1f2]) ).
fof(nbit_adder_connection_inb2_in2f2,axiom,
! [VAR_0] :
( connection(in(b2,VAR_0),in(n2,f(n2,VAR_0)))
| ~ type(VAR_0,nbit_adder(n2)) ),
file('theBenchmark.p',nbit_adder_connection_inb2_in2f2) ).
cnf(c_26,plain,
( connection(in(b2,A),in(n2,f(n2,A)))
| ~ type(A,nbit_adder(n2)) ),
inference(clausify,[status(thm)],[nbit_adder_connection_inb2_in2f2]) ).
fof(unique_value,axiom,
! [VAR_0,VAR_1,VAR_2] :
( equal_value(VAR_1,VAR_2)
| ~ value(VAR_0,VAR_2)
| ~ value(VAR_0,VAR_1) ),
file('theBenchmark.p',unique_value) ).
cnf(c_29,plain,
( equal_value(B,C)
| ~ value(A,C)
| ~ value(A,B) ),
inference(clausify,[status(thm)],[unique_value]) ).
fof(equal_value1,axiom,
~ equal_value(n0,n1),
file('theBenchmark.p',equal_value1) ).
cnf(c_30,plain,
~ equal_value(n0,n1),
inference(clausify,[status(thm)],[equal_value1]) ).
cnf(c_32,plain,
( ~ value(A,n1)
| ~ value(A,n0) ),
inference(resolve,[status(thm)],[c_29,c_30]) ).
fof(ok_or_abnormal,axiom,
! [VAR_0,VAR_1] :
( mode(VAR_0,abnormal)
| mode(VAR_0,ok)
| ~ type(VAR_0,VAR_1) ),
file('theBenchmark.p',ok_or_abnormal) ).
cnf(c_34,plain,
( mode(A,abnormal)
| mode(A,ok)
| ~ type(A,B) ),
inference(clausify,[status(thm)],[ok_or_abnormal]) ).
fof(and_1_1x,axiom,
! [VAR_0] :
( value(in(n1,VAR_0),n1)
| ~ value(out(n1,VAR_0),n1)
| ~ type(VAR_0,and)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',and_1_1x) ).
cnf(c_38,plain,
( value(in(n1,A),n1)
| ~ value(out(n1,A),n1)
| ~ type(A,and)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[and_1_1x]) ).
fof(or_1_11,axiom,
! [VAR_0] :
( value(in(n2,VAR_0),n1)
| value(in(n1,VAR_0),n1)
| ~ value(out(n1,VAR_0),n1)
| ~ type(VAR_0,or)
| ~ mode(VAR_0,ok) ),
file('theBenchmark.p',or_1_11) ).
cnf(c_42,plain,
( value(in(n2,A),n1)
| value(in(n1,A),n1)
| ~ value(out(n1,A),n1)
| ~ type(A,or)
| ~ mode(A,ok) ),
inference(clausify,[status(thm)],[or_1_11]) ).
fof(halfadder_and2,axiom,
! [VAR_0] :
( type(and2(VAR_0),and)
| ~ type(VAR_0,halfadder) ),
file('theBenchmark.p',halfadder_and2) ).
cnf(c_50,plain,
( type(and2(A),and)
| ~ type(A,halfadder) ),
inference(clausify,[status(thm)],[halfadder_and2]) ).
fof(fulladder_halfadder1,axiom,
! [VAR_0] :
( type(h1(VAR_0),halfadder)
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_halfadder1) ).
cnf(c_53,plain,
( type(h1(A),halfadder)
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_halfadder1]) ).
fof(fulladder_halfadder2,axiom,
! [VAR_0] :
( type(h2(VAR_0),halfadder)
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_halfadder2) ).
cnf(c_54,plain,
( type(h2(A),halfadder)
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_halfadder2]) ).
fof(fulladder_or1,axiom,
! [VAR_0] :
( type(or1(VAR_0),or)
| ~ type(VAR_0,fulladder) ),
file('theBenchmark.p',fulladder_or1) ).
cnf(c_55,plain,
( type(or1(A),or)
| ~ type(A,fulladder) ),
inference(clausify,[status(thm)],[fulladder_or1]) ).
fof(nbit_adder_fulladder2,axiom,
! [VAR_0] :
( type(f(n2,VAR_0),fulladder)
| ~ type(VAR_0,nbit_adder(n2)) ),
file('theBenchmark.p',nbit_adder_fulladder2) ).
cnf(c_57,plain,
( type(f(n2,A),fulladder)
| ~ type(A,nbit_adder(n2)) ),
inference(clausify,[status(thm)],[nbit_adder_fulladder2]) ).
fof(a_isa_2bit_adder,axiom,
type(a,nbit_adder(n2)),
file('theBenchmark.p',a_isa_2bit_adder) ).
cnf(c_58,plain,
type(a,nbit_adder(n2)),
inference(clausify,[status(thm)],[a_isa_2bit_adder]) ).
fof(ina2_0,axiom,
value(in(a2,a),n0),
file('theBenchmark.p',ina2_0) ).
cnf(c_60,plain,
value(in(a2,a),n0),
inference(clausify,[status(thm)],[ina2_0]) ).
fof(inb2_0,axiom,
value(in(b2,a),n0),
file('theBenchmark.p',inb2_0) ).
cnf(c_62,plain,
value(in(b2,a),n0),
inference(clausify,[status(thm)],[inb2_0]) ).
fof(outc_1,axiom,
value(out(c,a),n1),
file('theBenchmark.p',outc_1) ).
cnf(c_66,plain,
value(out(c,a),n1),
inference(clausify,[status(thm)],[outc_1]) ).
fof(diagnosis_or1f2a,axiom,
~ mode(or1(f(n2,a)),abnormal),
file('theBenchmark.p',diagnosis_or1f2a) ).
cnf(c_67,plain,
~ mode(or1(f(n2,a)),abnormal),
inference(clausify,[status(thm)],[diagnosis_or1f2a]) ).
fof(diagnosis_and2h2f2a,axiom,
~ mode(and2(h1(f(n2,a))),abnormal),
file('theBenchmark.p',diagnosis_and2h2f2a) ).
cnf(c_68,plain,
~ mode(and2(h1(f(n2,a))),abnormal),
inference(clausify,[status(thm)],[diagnosis_and2h2f2a]) ).
fof(diagnosis_and2h1f2a,axiom,
~ mode(and2(h2(f(n2,a))),abnormal),
file('theBenchmark.p',diagnosis_and2h1f2a) ).
cnf(c_69,plain,
~ mode(and2(h2(f(n2,a))),abnormal),
inference(clausify,[status(thm)],[diagnosis_and2h1f2a]) ).
cnf(c_74,plain,
( value(in(n1,A),B)
| ~ value(in(n1,and2(A)),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_5,c_2]) ).
cnf(c_81,plain,
( value(out(n1,and2(A)),B)
| ~ value(out(c,A),B)
| ~ type(A,halfadder) ),
inference(resolve,[status(thm)],[c_8,c_3]) ).
cnf(c_90,plain,
( value(out(c,h1(A)),B)
| ~ value(in(n2,or1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_13,c_2]) ).
cnf(c_92,plain,
( value(out(c,h2(A)),B)
| ~ value(in(n1,or1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_14,c_2]) ).
cnf(c_94,plain,
( value(in(n1,A),B)
| ~ value(in(n1,h2(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_15,c_2]) ).
cnf(c_96,plain,
( value(in(n2,A),B)
| ~ value(in(n1,h1(A)),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_16,c_2]) ).
cnf(c_103,plain,
( value(out(n1,or1(A)),B)
| ~ value(out(c,A),B)
| ~ type(A,fulladder) ),
inference(resolve,[status(thm)],[c_19,c_3]) ).
cnf(c_109,plain,
( value(out(c,f(n2,A)),B)
| ~ value(out(c,A),B)
| ~ type(A,nbit_adder(n2)) ),
inference(resolve,[status(thm)],[c_22,c_3]) ).
cnf(c_114,plain,
( value(in(a2,A),B)
| ~ value(in(n1,f(n2,A)),B)
| ~ type(A,nbit_adder(n2)) ),
inference(resolve,[status(thm)],[c_25,c_2]) ).
cnf(c_116,plain,
( value(in(b2,A),B)
| ~ value(in(n2,f(n2,A)),B)
| ~ type(A,nbit_adder(n2)) ),
inference(resolve,[status(thm)],[c_26,c_2]) ).
cnf(c_122,plain,
type(f(n2,a),fulladder),
inference(resolve,[status(thm)],[c_58,c_57]) ).
cnf(c_126,plain,
~ value(in(a2,a),n1),
inference(resolve,[status(thm)],[c_60,c_32]) ).
cnf(c_128,plain,
~ value(in(b2,a),n1),
inference(resolve,[status(thm)],[c_62,c_32]) ).
cnf(c_416,plain,
( value(out(c,f(n2,a)),n1)
| ~ type(a,nbit_adder(n2)) ),
inference(resolve,[status(thm)],[c_109,c_66]) ).
cnf(c_148,plain,
value(out(c,f(n2,a)),n1),
inference(resolve,[status(thm)],[c_58,c_416]) ).
cnf(c_182,plain,
type(or1(f(n2,a)),or),
inference(resolve,[status(thm)],[c_122,c_55]) ).
cnf(c_183,plain,
type(h2(f(n2,a)),halfadder),
inference(resolve,[status(thm)],[c_122,c_54]) ).
cnf(c_184,plain,
type(h1(f(n2,a)),halfadder),
inference(resolve,[status(thm)],[c_122,c_53]) ).
cnf(c_417,plain,
( value(in(a2,a),A)
| ~ value(in(n1,f(n2,a)),A) ),
inference(resolve,[status(thm)],[c_114,c_58]) ).
cnf(c_207,plain,
~ value(in(n1,f(n2,a)),n1),
inference(resolve,[status(thm)],[c_417,c_126]) ).
cnf(c_418,plain,
( value(in(b2,a),A)
| ~ value(in(n2,f(n2,a)),A) ),
inference(resolve,[status(thm)],[c_116,c_58]) ).
cnf(c_209,plain,
~ value(in(n2,f(n2,a)),n1),
inference(resolve,[status(thm)],[c_418,c_128]) ).
cnf(c_419,plain,
( mode(or1(f(n2,a)),abnormal)
| mode(or1(f(n2,a)),ok) ),
inference(resolve,[status(thm)],[c_182,c_34]) ).
cnf(c_220,plain,
mode(or1(f(n2,a)),ok),
inference(resolve,[status(thm)],[c_67,c_419]) ).
cnf(c_244,plain,
type(and2(h2(f(n2,a))),and),
inference(resolve,[status(thm)],[c_183,c_50]) ).
cnf(c_267,plain,
type(and2(h1(f(n2,a))),and),
inference(resolve,[status(thm)],[c_184,c_50]) ).
cnf(c_420,plain,
( value(in(n1,f(n2,a)),A)
| ~ value(in(n1,h2(f(n2,a))),A) ),
inference(resolve,[status(thm)],[c_94,c_122]) ).
cnf(c_334,plain,
~ value(in(n1,h2(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_420,c_207]) ).
cnf(c_421,plain,
( value(in(n2,f(n2,a)),A)
| ~ value(in(n1,h1(f(n2,a))),A) ),
inference(resolve,[status(thm)],[c_96,c_122]) ).
cnf(c_336,plain,
~ value(in(n1,h1(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_421,c_209]) ).
cnf(c_422,plain,
( value(out(n1,or1(f(n2,a))),n1)
| ~ type(f(n2,a),fulladder) ),
inference(resolve,[status(thm)],[c_148,c_103]) ).
cnf(c_341,plain,
value(out(n1,or1(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_122,c_422]) ).
cnf(c_423,plain,
( value(in(n1,h2(f(n2,a))),A)
| ~ value(in(n1,and2(h2(f(n2,a)))),A) ),
inference(resolve,[status(thm)],[c_74,c_183]) ).
cnf(c_369,plain,
~ value(in(n1,and2(h2(f(n2,a)))),n1),
inference(resolve,[status(thm)],[c_423,c_334]) ).
cnf(c_424,plain,
( value(in(n1,h1(f(n2,a))),A)
| ~ value(in(n1,and2(h1(f(n2,a)))),A) ),
inference(resolve,[status(thm)],[c_74,c_184]) ).
cnf(c_373,plain,
~ value(in(n1,and2(h1(f(n2,a)))),n1),
inference(resolve,[status(thm)],[c_424,c_336]) ).
cnf(c_425,plain,
( value(in(n1,and2(h2(f(n2,a)))),n1)
| ~ value(out(n1,and2(h2(f(n2,a)))),n1)
| ~ mode(and2(h2(f(n2,a))),ok) ),
inference(resolve,[status(thm)],[c_244,c_38]) ).
cnf(c_379,plain,
( ~ value(out(n1,and2(h2(f(n2,a)))),n1)
| ~ mode(and2(h2(f(n2,a))),ok) ),
inference(resolve,[status(thm)],[c_369,c_425]) ).
cnf(c_426,plain,
( mode(and2(h2(f(n2,a))),abnormal)
| mode(and2(h2(f(n2,a))),ok) ),
inference(resolve,[status(thm)],[c_244,c_34]) ).
cnf(c_380,plain,
mode(and2(h2(f(n2,a))),ok),
inference(resolve,[status(thm)],[c_69,c_426]) ).
cnf(c_381,plain,
~ value(out(n1,and2(h2(f(n2,a)))),n1),
inference(resolve,[status(thm)],[c_380,c_379]) ).
cnf(c_427,plain,
( value(in(n1,and2(h1(f(n2,a)))),n1)
| ~ value(out(n1,and2(h1(f(n2,a)))),n1)
| ~ mode(and2(h1(f(n2,a))),ok) ),
inference(resolve,[status(thm)],[c_267,c_38]) ).
cnf(c_385,plain,
( ~ value(out(n1,and2(h1(f(n2,a)))),n1)
| ~ mode(and2(h1(f(n2,a))),ok) ),
inference(resolve,[status(thm)],[c_373,c_427]) ).
cnf(c_428,plain,
( mode(and2(h1(f(n2,a))),abnormal)
| mode(and2(h1(f(n2,a))),ok) ),
inference(resolve,[status(thm)],[c_267,c_34]) ).
cnf(c_386,plain,
mode(and2(h1(f(n2,a))),ok),
inference(resolve,[status(thm)],[c_68,c_428]) ).
cnf(c_387,plain,
~ value(out(n1,and2(h1(f(n2,a)))),n1),
inference(resolve,[status(thm)],[c_386,c_385]) ).
cnf(c_429,plain,
( value(out(n1,and2(h2(f(n2,a)))),A)
| ~ value(out(c,h2(f(n2,a))),A) ),
inference(resolve,[status(thm)],[c_81,c_183]) ).
cnf(c_397,plain,
~ value(out(c,h2(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_429,c_381]) ).
cnf(c_430,plain,
( value(out(c,h2(f(n2,a))),A)
| ~ value(in(n1,or1(f(n2,a))),A) ),
inference(resolve,[status(thm)],[c_92,c_122]) ).
cnf(c_398,plain,
~ value(in(n1,or1(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_430,c_397]) ).
cnf(c_431,plain,
( value(out(n1,and2(h1(f(n2,a)))),A)
| ~ value(out(c,h1(f(n2,a))),A) ),
inference(resolve,[status(thm)],[c_81,c_184]) ).
cnf(c_413,plain,
~ value(out(c,h1(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_431,c_387]) ).
cnf(c_432,plain,
( value(out(c,h1(f(n2,a))),A)
| ~ value(in(n2,or1(f(n2,a))),A) ),
inference(resolve,[status(thm)],[c_90,c_122]) ).
cnf(c_414,plain,
~ value(in(n2,or1(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_432,c_413]) ).
cnf(c_433,plain,
( value(in(n2,or1(f(n2,a))),n1)
| value(in(n1,or1(f(n2,a))),n1)
| ~ value(out(n1,or1(f(n2,a))),n1)
| ~ type(or1(f(n2,a)),or) ),
inference(resolve,[status(thm)],[c_42,c_220]) ).
cnf(c_434,plain,
( value(in(n2,or1(f(n2,a))),n1)
| value(in(n1,or1(f(n2,a))),n1)
| ~ value(out(n1,or1(f(n2,a))),n1) ),
inference(resolve,[status(thm)],[c_433,c_182]) ).
cnf(c_435,plain,
( value(in(n2,or1(f(n2,a))),n1)
| ~ value(out(n1,or1(f(n2,a))),n1) ),
inference(resolve,[status(thm)],[c_434,c_398]) ).
cnf(c_436,plain,
~ value(out(n1,or1(f(n2,a))),n1),
inference(resolve,[status(thm)],[c_435,c_414]) ).
cnf(c_415,plain,
$false,
inference(resolve,[status(thm)],[c_341,c_436]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-1.002 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /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.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 16:01:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2376875 was started by sandbox on n018,
% 0.10/0.37 % Fri Sep 25 16:01:50 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 0.10/0.41
% 0.10/0.41 % SZS status Unsatisfiable for theBenchmark
% 0.10/0.41
% 0.10/0.41 % Proof 1 at 0.02 (+ 0.01) seconds.
% 0.10/0.41 % Length of proof is 68.
% 0.10/0.41 % Level of proof is 10.
% 0.10/0.41 % Maximum clause weight is 26.000.
% 0.10/0.41 % Given clauses 194.
% 0.10/0.41
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------