%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWC003-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Thu Sep 24 12:45:50 PM UTC 2026
% Result : Unsatisfiable 269.27s 34.41s
% Output : CNFRefutation 228.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 11
% Syntax : Number of formulae : 88 ( 79 unt; 0 def)
% Number of atoms : 99 ( 14 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 27 ( 16 ~; 11 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-10 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-8 aty)
% Number of variables : 153 ( 153 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
not(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
not(n1) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] : add_inverter(list(X,Y),Z) = list(X,add_inverter(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : add_inverter(X,Y) = list(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [V] : make_reverse_list(V) = end,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X1,X2,X3,X4,X5,X6,X7,X8,V] :
( test(not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7),not(X8),add_inverter(V,inverter_table(not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7),not(X8))),make_reverse_list(list(inverter_table(not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7),not(X8)),V)))
| ~ output(X1,X2,X3,X4,X5,X6,X7,X8,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X1,X2,X3,X4,X5,X6,X7,X8,V,Xrevlist] :
( output(X1,X2,X3,X4,X5,X6,X7,X8,V)
| ~ test(X1,X2,X3,X4,X5,X6,X7,X8,V,Xrevlist) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [X] : output(n0,n0,n0,n0,n1,n1,n1,n1,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [X] : output(n0,n0,n1,n1,n0,n0,n1,n1,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [X] : output(n0,n1,n0,n1,n0,n1,n0,n1,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [V] :
( ~ output(n1,n0,n1,n0,n1,n0,n1,n0,V)
| ~ output(n1,n1,n0,n0,n1,n1,n0,n0,V)
| ~ output(n1,n1,n1,n1,n0,n0,n0,n0,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,plain,
not(n0) = n1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f30,plain,
not(n1) = n0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f31,plain,
! [X0,X1,X2] : add_inverter(list(X0,X1),X2) = list(X0,add_inverter(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f32,plain,
! [X0,X1] : add_inverter(X0,X1) = list(X1,X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f34,plain,
! [X0] : make_reverse_list(X0) = end,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( test(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7),add_inverter(X8,inverter_table(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7))),make_reverse_list(list(inverter_table(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7)),X8)))
| ~ output(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f44,plain,
! [X1,X2,X3,X4,X5,X6,X7,X8,V] :
( output(X1,X2,X3,X4,X5,X6,X7,X8,V)
| ! [Xrevlist] : ~ test(X1,X2,X3,X4,X5,X6,X7,X8,V,Xrevlist) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f45,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( output(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ test(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0] : output(n0,n0,n0,n0,n1,n1,n1,n1,X0),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f47,plain,
! [X0] : output(n0,n0,n1,n1,n0,n0,n1,n1,X0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f48,plain,
! [X0] : output(n0,n1,n0,n1,n0,n1,n0,n1,X0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f49,plain,
! [X0] :
( ~ output(n1,n0,n1,n0,n1,n0,n1,n0,X0)
| ~ output(n1,n1,n0,n0,n1,n1,n0,n0,X0)
| ~ output(n1,n1,n1,n1,n0,n0,n0,n0,X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f50,plain,
! [X0,X1,X2] : add_inverter(list(X0,X1),X2) = add_inverter(add_inverter(X1,X2),X0),
inference(backward_demodulation,[status(thm)],[f32,f31]) ).
fof(f53,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( test(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7),add_inverter(X8,inverter_table(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7))),end)
| ~ output(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(forward_demodulation,[status(thm)],[f34,f43]) ).
fof(f54,plain,
! [X0,X1,X2] : add_inverter(add_inverter(X0,X1),X2) = add_inverter(add_inverter(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f32,f50]) ).
fof(f82,plain,
! [X0,X1,X2,X3] : add_inverter(add_inverter(add_inverter(X0,X1),X2),X3) = add_inverter(add_inverter(add_inverter(X0,X2),X3),X1),
inference(paramodulation,[status(thm)],[f54,f54]) ).
fof(f216,plain,
! [X0,X1,X2,X3] : add_inverter(add_inverter(add_inverter(X0,X1),X2),X3) = add_inverter(add_inverter(add_inverter(X0,X2),X1),X3),
inference(paramodulation,[status(thm)],[f54,f82]) ).
fof(f2235,plain,
! [X0] : test(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(resolution,[status(thm)],[f53,f48]) ).
fof(f2236,plain,
! [X0] : test(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(resolution,[status(thm)],[f53,f47]) ).
fof(f2237,plain,
! [X0] : test(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(resolution,[status(thm)],[f53,f46]) ).
fof(f2238,plain,
! [X0] : test(n1,not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2235]) ).
fof(f2239,plain,
! [X0] : test(n1,n0,not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2238]) ).
fof(f2240,plain,
! [X0] : test(n1,n0,n1,not(n1),not(n0),not(n1),not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2239]) ).
fof(f2241,plain,
! [X0] : test(n1,n0,n1,n0,not(n0),not(n1),not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2240]) ).
fof(f2242,plain,
! [X0] : test(n1,n0,n1,n0,n1,not(n1),not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2241]) ).
fof(f2243,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,not(n0),not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2242]) ).
fof(f2244,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,not(n1),add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2243]) ).
fof(f2245,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2244]) ).
fof(f2246,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2245]) ).
fof(f2247,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,not(n0),not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2246]) ).
fof(f2248,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,not(n1),not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2247]) ).
fof(f2249,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,n0,not(n0),not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2248]) ).
fof(f2250,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,n0,n1,not(n1),not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2249]) ).
fof(f2251,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,n0,n1,n0,not(n0),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2250]) ).
fof(f2252,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,n0,n1,n0,n1,not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2251]) ).
fof(f2253,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,n0,n1,n0,n1,n0)),end),
inference(forward_demodulation,[status(thm)],[f30,f2252]) ).
fof(f2254,plain,
! [X0] : test(n1,not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2236]) ).
fof(f2255,plain,
! [X0] : test(n1,n1,not(n1),not(n1),not(n0),not(n0),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2254]) ).
fof(f2256,plain,
! [X0] : test(n1,n1,n0,not(n1),not(n0),not(n0),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2255]) ).
fof(f2257,plain,
! [X0] : test(n1,n1,n0,n0,not(n0),not(n0),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2256]) ).
fof(f2258,plain,
! [X0] : test(n1,n1,n0,n0,n1,not(n0),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2257]) ).
fof(f2259,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2258]) ).
fof(f2260,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2259]) ).
fof(f2261,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2260]) ).
fof(f2262,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2261]) ).
fof(f2263,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,not(n1),not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2262]) ).
fof(f2264,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,not(n1),not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2263]) ).
fof(f2265,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,n0,not(n0),not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2264]) ).
fof(f2266,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,not(n0),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2265]) ).
fof(f2267,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2266]) ).
fof(f2268,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,n0,not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2267]) ).
fof(f2269,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,n0,n0)),end),
inference(forward_demodulation,[status(thm)],[f30,f2268]) ).
fof(f2270,plain,
! [X0] : test(n1,not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2237]) ).
fof(f2271,plain,
! [X0] : test(n1,n1,not(n0),not(n0),not(n1),not(n1),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2270]) ).
fof(f2272,plain,
! [X0] : test(n1,n1,n1,not(n0),not(n1),not(n1),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2271]) ).
fof(f2273,plain,
! [X0] : test(n1,n1,n1,n1,not(n1),not(n1),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2272]) ).
fof(f2274,plain,
! [X0] : test(n1,n1,n1,n1,n0,not(n1),not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2273]) ).
fof(f2275,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,not(n1),not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2274]) ).
fof(f2276,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,not(n1),add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2275]) ).
fof(f2277,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2276]) ).
fof(f2278,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2277]) ).
fof(f2279,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,not(n0),not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2278]) ).
fof(f2280,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,not(n0),not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2279]) ).
fof(f2281,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,not(n1),not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f29,f2280]) ).
fof(f2282,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,not(n1),not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2281]) ).
fof(f2283,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,n0,not(n1),not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2282]) ).
fof(f2284,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,n0,n0,not(n1))),end),
inference(forward_demodulation,[status(thm)],[f30,f2283]) ).
fof(f2285,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,n0,n0,n0)),end),
inference(forward_demodulation,[status(thm)],[f30,f2284]) ).
fof(f2400,plain,
! [X0] : output(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n0,n1,n0,n1,n0,n1,n0))),
inference(resolution,[status(thm)],[f2253,f45]) ).
fof(f2418,plain,
! [X0,X1] : output(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(add_inverter(X0,inverter_table(n1,n0,n1,n0,n1,n0,n1,n0)),X1)),
inference(paramodulation,[status(thm)],[f54,f2400]) ).
fof(f2453,plain,
! [X0] : output(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,n0,n0))),
inference(resolution,[status(thm)],[f2269,f45]) ).
fof(f2471,plain,
! [X0,X1] : output(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,n0,n0)),X1)),
inference(paramodulation,[status(thm)],[f54,f2453]) ).
fof(f2506,plain,
! [X0] : output(n1,n1,n1,n1,n0,n0,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,n0,n0,n0))),
inference(resolution,[status(thm)],[f2285,f45]) ).
fof(f2515,plain,
! [X0] :
( ~ output(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,n0,n0,n0)))
| ~ output(n1,n1,n0,n0,n1,n1,n0,n0,add_inverter(X0,inverter_table(n1,n1,n1,n1,n0,n0,n0,n0))) ),
inference(resolution,[status(thm)],[f2506,f49]) ).
fof(f2620,plain,
! [X0] : ~ output(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,n0,n0)),inverter_table(n1,n1,n1,n1,n0,n0,n0,n0))),
inference(resolution,[status(thm)],[f2471,f2515]) ).
fof(f2673,plain,
! [X0,X1] : ~ output(n1,n0,n1,n0,n1,n0,n1,n0,add_inverter(add_inverter(add_inverter(X0,inverter_table(n1,n1,n0,n0,n1,n1,n0,n0)),X1),inverter_table(n1,n1,n1,n1,n0,n0,n0,n0))),
inference(paramodulation,[status(thm)],[f216,f2620]) ).
fof(f2807,plain,
$false,
inference(resolution,[status(thm)],[f2673,f2418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWC003-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 20 20:44:50 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 269.27/34.41 % Refutation found
% 269.27/34.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 269.27/34.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 228.92/34.46 % Elapsed time: 34.057832 seconds
% 228.92/34.46 % CPU time: 270.311639 seconds
% 228.92/34.46 % Total memory used: 473.165 MB
% 228.92/34.46 % Net memory used: 463.724 MB
%------------------------------------------------------------------------------