%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWC003-2 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:51 PM UTC 2026
% Result : Unsatisfiable 28.76s 4.23s
% Output : CNFRefutation 7.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 12
% Syntax : Number of formulae : 90 ( 74 unt; 0 def)
% Number of atoms : 111 ( 12 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 49 ( 28 ~; 21 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-10 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-8 aty)
% Number of variables : 192 ( 192 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
not(n0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
not(n1) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] : add_inverter(list(X,Y),Z) = list(X,add_inverter(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : add_inverter(X,Y) = list(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [V] : make_reverse_list(V) = end,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X1,X2,X3,X4,X5,X6,X7,X8,V] :
( output(X1,X2,X3,X4,X5,X6,X7,X8,V)
| ~ basic_output(X1,X2,X3,X4,X5,X6,X7,X8,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X1,X2,X3,X4,X5,X6,X7,X8,V,Xrevlist] :
( basic_output(X1,X2,X3,X4,X5,X6,X7,X8,V)
| ~ test(X1,X2,X3,X4,X5,X6,X7,X8,V,Xrevlist) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [X] : output(n0,n0,n0,n0,n1,n1,n1,n1,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [X] : output(n0,n0,n1,n1,n0,n0,n1,n1,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [X] : output(n0,n1,n0,n1,n0,n1,n0,n1,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,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/sandbox/benchmark/theBenchmark.p') ).
fof(f30,plain,
not(n0) = n1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f31,plain,
not(n1) = n0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f32,plain,
! [X0,X1,X2] : add_inverter(list(X0,X1),X2) = list(X0,add_inverter(X1,X2)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f33,plain,
! [X0,X1] : add_inverter(X0,X1) = list(X1,X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f35,plain,
! [X0] : make_reverse_list(X0) = end,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f44,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(f45,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( output(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| ~ basic_output(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f46,plain,
! [X1,X2,X3,X4,X5,X6,X7,X8,V] :
( basic_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)],[f21]) ).
fof(f47,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( basic_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)],[f46]) ).
fof(f48,plain,
! [X0] : output(n0,n0,n0,n0,n1,n1,n1,n1,X0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f49,plain,
! [X0] : output(n0,n0,n1,n1,n0,n0,n1,n1,X0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f50,plain,
! [X0] : output(n0,n1,n0,n1,n0,n1,n0,n1,X0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f51,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)],[f25]) ).
fof(f56,plain,
! [X0,X1,X2] : list(X0,list(X1,X2)) = list(X1,add_inverter(X2,X0)),
inference(forward_demodulation,[status(thm)],[f33,f32]) ).
fof(f57,plain,
! [X0,X1,X2] : list(X0,list(X1,X2)) = list(X1,list(X0,X2)),
inference(forward_demodulation,[status(thm)],[f33,f56]) ).
fof(f306,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),list(inverter_table(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7)),X8),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(forward_demodulation,[status(thm)],[f33,f44]) ).
fof(f307,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),list(inverter_table(not(X0),not(X1),not(X2),not(X3),not(X4),not(X5),not(X6),not(X7)),X8),end)
| ~ output(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(forward_demodulation,[status(thm)],[f35,f306]) ).
fof(f308,plain,
! [X0] : test(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(resolution,[status(thm)],[f307,f50]) ).
fof(f309,plain,
! [X0] : test(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(resolution,[status(thm)],[f307,f49]) ).
fof(f310,plain,
! [X0] : test(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(resolution,[status(thm)],[f307,f48]) ).
fof(f311,plain,
! [X0] : test(n1,not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f308]) ).
fof(f312,plain,
! [X0] : test(n1,n0,not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f311]) ).
fof(f313,plain,
! [X0] : test(n1,n0,n1,not(n1),not(n0),not(n1),not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f312]) ).
fof(f314,plain,
! [X0] : test(n1,n0,n1,n0,not(n0),not(n1),not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f313]) ).
fof(f315,plain,
! [X0] : test(n1,n0,n1,n0,n1,not(n1),not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f314]) ).
fof(f316,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,not(n0),not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f315]) ).
fof(f317,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,not(n1),list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f316]) ).
fof(f318,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(not(n0),not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f317]) ).
fof(f319,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,not(n1),not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f318]) ).
fof(f320,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,not(n0),not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f319]) ).
fof(f321,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,n1,not(n1),not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f320]) ).
fof(f322,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,n1,n0,not(n0),not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f321]) ).
fof(f323,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,n1,n0,n1,not(n1),not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f322]) ).
fof(f324,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,n1,n0,n1,n0,not(n0),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f323]) ).
fof(f325,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,n1,n0,n1,n0,n1,not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f324]) ).
fof(f326,plain,
! [X0] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n0,n1,n0,n1,n0,n1,n0),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f325]) ).
fof(f327,plain,
! [X0] : test(n1,not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f309]) ).
fof(f328,plain,
! [X0] : test(n1,n1,not(n1),not(n1),not(n0),not(n0),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f327]) ).
fof(f329,plain,
! [X0] : test(n1,n1,n0,not(n1),not(n0),not(n0),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f328]) ).
fof(f330,plain,
! [X0] : test(n1,n1,n0,n0,not(n0),not(n0),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f329]) ).
fof(f331,plain,
! [X0] : test(n1,n1,n0,n0,n1,not(n0),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f330]) ).
fof(f332,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f331]) ).
fof(f333,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,not(n1),list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f332]) ).
fof(f334,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(not(n0),not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f333]) ).
fof(f335,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,not(n0),not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f334]) ).
fof(f336,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,not(n1),not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f335]) ).
fof(f337,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n0,not(n1),not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f336]) ).
fof(f338,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n0,n0,not(n0),not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f337]) ).
fof(f339,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n0,n0,n1,not(n0),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f338]) ).
fof(f340,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n0,n0,n1,n1,not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f339]) ).
fof(f341,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n0,n0,n1,n1,n0,not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f340]) ).
fof(f342,plain,
! [X0] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n0,n0,n1,n1,n0,n0),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f341]) ).
fof(f343,plain,
! [X0] : test(n1,not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f310]) ).
fof(f344,plain,
! [X0] : test(n1,n1,not(n0),not(n0),not(n1),not(n1),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f343]) ).
fof(f345,plain,
! [X0] : test(n1,n1,n1,not(n0),not(n1),not(n1),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f344]) ).
fof(f346,plain,
! [X0] : test(n1,n1,n1,n1,not(n1),not(n1),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f345]) ).
fof(f347,plain,
! [X0] : test(n1,n1,n1,n1,n0,not(n1),not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f346]) ).
fof(f348,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,not(n1),not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f347]) ).
fof(f349,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,not(n1),list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f348]) ).
fof(f350,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(not(n0),not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f349]) ).
fof(f351,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,not(n0),not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f350]) ).
fof(f352,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,not(n0),not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f351]) ).
fof(f353,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,n1,not(n0),not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f352]) ).
fof(f354,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,n1,n1,not(n1),not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f30,f353]) ).
fof(f355,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,n1,n1,n0,not(n1),not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f354]) ).
fof(f356,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,n1,n1,n0,n0,not(n1),not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f355]) ).
fof(f357,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,n1,n1,n0,n0,n0,not(n1)),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f356]) ).
fof(f358,plain,
! [X0] : test(n1,n1,n1,n1,n0,n0,n0,n0,list(inverter_table(n1,n1,n1,n1,n0,n0,n0,n0),X0),end),
inference(forward_demodulation,[status(thm)],[f31,f357]) ).
fof(f359,plain,
! [X0,X1] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(X0,list(inverter_table(n1,n0,n1,n0,n1,n0,n1,n0),X1)),end),
inference(paramodulation,[status(thm)],[f57,f326]) ).
fof(f361,plain,
! [X0,X1] : test(n1,n1,n0,n0,n1,n1,n0,n0,list(X0,list(inverter_table(n1,n1,n0,n0,n1,n1,n0,n0),X1)),end),
inference(paramodulation,[status(thm)],[f57,f342]) ).
fof(f367,plain,
! [X0,X1,X2] : test(n1,n0,n1,n0,n1,n0,n1,n0,list(X0,list(X1,list(inverter_table(n1,n0,n1,n0,n1,n0,n1,n0),X2))),end),
inference(paramodulation,[status(thm)],[f57,f359]) ).
fof(f843,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(resolution,[status(thm)],[f47,f45]) ).
fof(f4158,plain,
! [X0,X1] :
( ~ output(n1,n0,n1,n0,n1,n0,n1,n0,X0)
| ~ output(n1,n1,n0,n0,n1,n1,n0,n0,X0)
| ~ test(n1,n1,n1,n1,n0,n0,n0,n0,X0,X1) ),
inference(resolution,[status(thm)],[f843,f51]) ).
fof(f4661,plain,
! [X0,X1,X2] :
( ~ test(n1,n1,n0,n0,n1,n1,n0,n0,X0,X2)
| ~ output(n1,n0,n1,n0,n1,n0,n1,n0,X0)
| ~ test(n1,n1,n1,n1,n0,n0,n0,n0,X0,X1) ),
inference(resolution,[status(thm)],[f4158,f843]) ).
fof(f4662,plain,
! [X0,X1,X2,X3] :
( ~ test(n1,n0,n1,n0,n1,n0,n1,n0,X0,X3)
| ~ test(n1,n1,n0,n0,n1,n1,n0,n0,X0,X2)
| ~ test(n1,n1,n1,n1,n0,n0,n0,n0,X0,X1) ),
inference(resolution,[status(thm)],[f4661,f843]) ).
fof(f4663,plain,
! [X0,X1,X2] :
( ~ test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n1,n1,n1,n0,n0,n0,n0),X0),X2)
| ~ test(n1,n1,n0,n0,n1,n1,n0,n0,list(inverter_table(n1,n1,n1,n1,n0,n0,n0,n0),X0),X1) ),
inference(resolution,[status(thm)],[f4662,f358]) ).
fof(f4744,plain,
! [X0,X1] : ~ test(n1,n0,n1,n0,n1,n0,n1,n0,list(inverter_table(n1,n1,n1,n1,n0,n0,n0,n0),list(inverter_table(n1,n1,n0,n0,n1,n1,n0,n0),X0)),X1),
inference(resolution,[status(thm)],[f4663,f361]) ).
fof(f4760,plain,
$false,
inference(resolution,[status(thm)],[f4744,f367]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : HWC003-2 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n008.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Sun Sep 20 20:47:40 UTC 2026
% 0.15/0.44 % CPUTime :
% 0.15/0.45 % Drodi V4.1.1
% 28.76/4.23 % Refutation found
% 28.76/4.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.76/4.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.81/4.27 % Elapsed time: 3.817288 seconds
% 7.81/4.27 % CPU time: 29.606078 seconds
% 7.81/4.27 % Total memory used: 148.682 MB
% 7.81/4.27 % Net memory used: 147.691 MB
%------------------------------------------------------------------------------