%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:53 PM UTC 2026
% Result : Unsatisfiable 34.92s 4.82s
% Output : CNFRefutation 34.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 36
% Syntax : Number of formulae : 237 ( 237 unt; 0 def)
% Number of atoms : 237 ( 220 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 10 ( 10 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 19 con; 0-2 aty)
% Number of variables : 130 ( 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X] : and(X,n1) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : or(X,n0) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : or(X,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
not(n0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] : and(X,Y) = and(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : or(X,Y) = or(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y,Z] : and(X,and(Y,Z)) = and(and(X,Y),Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y,Z] : or(X,or(Y,Z)) = or(or(X,Y),Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y,Z] : or(or(X,Y),Z) = or(or(X,Z),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y,Z] : and(and(X,Y),Z) = and(and(X,Z),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y] : not(and(X,Y)) = or(not(X),not(Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,Y] : not(or(X,Y)) = and(not(X),not(Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,Y,Z] : and(or(X,Y),Z) = or(and(X,Z),and(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] : and(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] : or(X,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X] : and(X,not(X)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X,Y] : and(and(X,Y),not(X)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X] : not(not(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X,Y] : or(and(X,Y),and(X,not(Y))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
a1 = and(b1,b3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
a2 = and(b2,b3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
b1 = not(d1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
b2 = not(d2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
b3 = or(c1,c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
c1 = or(d1,d3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
c2 = or(d2,d3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
d3 = f3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
d1 = not(e1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
d2 = not(e2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
e1 = or(f1,f3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
e2 = or(f2,f3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
f1 = not(i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
f2 = not(i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
f3 = and(i1,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,plain,
! [X0] : and(X0,n1) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
! [X0] : or(X0,n0) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f51,plain,
! [X0] : or(X0,n1) = n1,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f52,plain,
not(n0) = n1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f54,plain,
! [X0,X1] : and(X0,X1) = and(X1,X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f55,plain,
! [X0,X1] : or(X0,X1) = or(X1,X0),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f56,plain,
! [X0,X1,X2] : and(X0,and(X1,X2)) = and(and(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f57,plain,
! [X0,X1,X2] : or(X0,or(X1,X2)) = or(or(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f58,plain,
! [X0,X1,X2] : or(or(X0,X1),X2) = or(or(X0,X2),X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f59,plain,
! [X0,X1,X2] : and(and(X0,X1),X2) = and(and(X0,X2),X1),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f60,plain,
! [X0,X1] : not(and(X0,X1)) = or(not(X0),not(X1)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f61,plain,
! [X0,X1] : not(or(X0,X1)) = and(not(X0),not(X1)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f62,plain,
! [X0,X1,X2] : and(or(X0,X1),X2) = or(and(X0,X2),and(X1,X2)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f63,plain,
! [X0] : and(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f66,plain,
! [X0] : or(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f69,plain,
! [X0] : and(X0,not(X0)) = n0,
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f71,plain,
! [X0,X1] : and(and(X0,X1),not(X0)) = n0,
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f75,plain,
! [X0] : not(not(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f76,plain,
! [X0,X1] : or(and(X0,X1),and(X0,not(X1))) = X0,
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f78,plain,
a1 = and(b1,b3),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f79,plain,
a2 = and(b2,b3),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f80,plain,
b1 = not(d1),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f81,plain,
b2 = not(d2),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f82,plain,
b3 = or(c1,c2),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f83,plain,
c1 = or(d1,d3),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f84,plain,
c2 = or(d2,d3),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f85,plain,
d3 = f3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f86,plain,
d1 = not(e1),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f87,plain,
d2 = not(e2),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f88,plain,
e1 = or(f1,f3),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f89,plain,
e2 = or(f2,f3),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f90,plain,
f1 = not(i1),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f91,plain,
f2 = not(i2),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f92,plain,
f3 = and(i1,i2),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f93,plain,
circuit(input(i1,i2),output(a1,a2)),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f94,plain,
~ circuit(input(i1,i2),output(i2,i1)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f95,plain,
! [X0,X1,X2] : or(X0,or(X1,X2)) = or(or(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f57,f58]) ).
fof(f96,plain,
! [X0,X1,X2] : and(X0,and(X1,X2)) = and(and(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f56,f59]) ).
fof(f102,plain,
! [X0,X1] : and(X0,and(not(X0),X1)) = n0,
inference(forward_demodulation,[status(thm)],[f96,f71]) ).
fof(f105,plain,
e1 = or(f1,d3),
inference(forward_demodulation,[status(thm)],[f85,f88]) ).
fof(f106,plain,
e2 = or(f2,d3),
inference(forward_demodulation,[status(thm)],[f85,f89]) ).
fof(f107,plain,
d3 = and(i1,i2),
inference(forward_demodulation,[status(thm)],[f85,f92]) ).
fof(f109,plain,
not(b1) = d1,
inference(paramodulation,[status(thm)],[f80,f75]) ).
fof(f119,plain,
! [X0] : and(n1,X0) = X0,
inference(paramodulation,[status(thm)],[f54,f49]) ).
fof(f133,plain,
not(d1) = e1,
inference(paramodulation,[status(thm)],[f86,f75]) ).
fof(f135,plain,
b1 = or(f1,d3),
inference(backward_demodulation,[status(thm)],[f136,f105]) ).
fof(f136,plain,
b1 = e1,
inference(forward_demodulation,[status(thm)],[f80,f133]) ).
fof(f143,plain,
! [X0] : or(n1,X0) = n1,
inference(paramodulation,[status(thm)],[f55,f51]) ).
fof(f172,plain,
not(d2) = e2,
inference(paramodulation,[status(thm)],[f87,f75]) ).
fof(f174,plain,
b2 = or(f2,d3),
inference(backward_demodulation,[status(thm)],[f175,f106]) ).
fof(f175,plain,
b2 = e2,
inference(forward_demodulation,[status(thm)],[f81,f172]) ).
fof(f176,plain,
a2 = and(b3,b2),
inference(paramodulation,[status(thm)],[f54,f79]) ).
fof(f178,plain,
! [X0] : and(b2,and(b3,X0)) = and(a2,X0),
inference(paramodulation,[status(thm)],[f79,f56]) ).
fof(f181,plain,
not(f1) = i1,
inference(paramodulation,[status(thm)],[f90,f75]) ).
fof(f182,plain,
not(f2) = i2,
inference(paramodulation,[status(thm)],[f91,f75]) ).
fof(f219,plain,
! [X0,X1] : or(X0,or(X1,X0)) = or(X0,X1),
inference(paramodulation,[status(thm)],[f66,f95]) ).
fof(f312,plain,
! [X0,X1] : and(X0,and(X1,X0)) = and(X0,X1),
inference(paramodulation,[status(thm)],[f63,f96]) ).
fof(f346,plain,
! [X0] : not(and(i2,X0)) = or(f2,not(X0)),
inference(paramodulation,[status(thm)],[f91,f60]) ).
fof(f375,plain,
! [X0,X1] : not(or(X0,X1)) = and(not(X1),not(X0)),
inference(paramodulation,[status(thm)],[f54,f61]) ).
fof(f379,plain,
! [X0] : not(or(f1,X0)) = and(i1,not(X0)),
inference(paramodulation,[status(thm)],[f181,f61]) ).
fof(f382,plain,
! [X0] : not(or(i2,X0)) = and(f2,not(X0)),
inference(paramodulation,[status(thm)],[f91,f61]) ).
fof(f383,plain,
! [X0] : not(or(i1,X0)) = and(f1,not(X0)),
inference(paramodulation,[status(thm)],[f90,f61]) ).
fof(f386,plain,
! [X0] : not(or(d2,X0)) = and(b2,not(X0)),
inference(paramodulation,[status(thm)],[f81,f61]) ).
fof(f393,plain,
! [X0] : not(or(X0,i2)) = and(not(X0),f2),
inference(paramodulation,[status(thm)],[f91,f61]) ).
fof(f397,plain,
! [X0] : not(or(X0,d2)) = and(not(X0),b2),
inference(paramodulation,[status(thm)],[f81,f61]) ).
fof(f413,plain,
! [X0] : or(d1,or(X0,d3)) = or(c1,X0),
inference(paramodulation,[status(thm)],[f83,f95]) ).
fof(f415,plain,
! [X0] : or(d2,or(X0,d3)) = or(c2,X0),
inference(paramodulation,[status(thm)],[f84,f95]) ).
fof(f419,plain,
b1 = or(d3,f1),
inference(paramodulation,[status(thm)],[f55,f135]) ).
fof(f421,plain,
! [X0] : or(f1,or(X0,d3)) = or(b1,X0),
inference(paramodulation,[status(thm)],[f135,f95]) ).
fof(f427,plain,
! [X0] : or(f2,or(X0,d3)) = or(b2,X0),
inference(paramodulation,[status(thm)],[f174,f95]) ).
fof(f440,plain,
! [X0,X1] : and(or(n1,X0),X1) = or(X1,and(X0,X1)),
inference(paramodulation,[status(thm)],[f119,f62]) ).
fof(f449,plain,
! [X0,X1] : and(or(X0,X1),X0) = or(X0,and(X1,X0)),
inference(paramodulation,[status(thm)],[f63,f62]) ).
fof(f454,plain,
! [X0,X1] : and(or(X0,n1),X1) = or(and(X0,X1),X1),
inference(paramodulation,[status(thm)],[f119,f62]) ).
fof(f463,plain,
! [X0,X1] : and(or(X0,X1),X1) = or(and(X0,X1),X1),
inference(paramodulation,[status(thm)],[f63,f62]) ).
fof(f470,plain,
! [X0,X1] : and(n1,X0) = or(X0,and(X1,X0)),
inference(forward_demodulation,[status(thm)],[f143,f440]) ).
fof(f471,plain,
! [X0,X1] : X0 = or(X0,and(X1,X0)),
inference(forward_demodulation,[status(thm)],[f119,f470]) ).
fof(f475,plain,
! [X0,X1] : and(or(X0,X1),X0) = X0,
inference(forward_demodulation,[status(thm)],[f471,f449]) ).
fof(f477,plain,
! [X0,X1] : and(n1,X0) = or(and(X1,X0),X0),
inference(forward_demodulation,[status(thm)],[f51,f454]) ).
fof(f478,plain,
! [X0,X1] : X0 = or(and(X1,X0),X0),
inference(forward_demodulation,[status(thm)],[f119,f477]) ).
fof(f483,plain,
! [X0,X1] : and(or(X0,X1),X1) = X1,
inference(forward_demodulation,[status(thm)],[f478,f463]) ).
fof(f573,plain,
! [X0,X1] : and(or(X0,X1),not(X1)) = or(and(X0,not(X1)),n0),
inference(paramodulation,[status(thm)],[f69,f62]) ).
fof(f581,plain,
! [X0,X1] : and(or(X0,X1),not(X1)) = and(X0,not(X1)),
inference(forward_demodulation,[status(thm)],[f50,f573]) ).
fof(f622,plain,
i2 = or(i2,d3),
inference(paramodulation,[status(thm)],[f107,f471]) ).
fof(f629,plain,
b3 = or(b3,a1),
inference(paramodulation,[status(thm)],[f78,f471]) ).
fof(f634,plain,
! [X0,X1] : X0 = or(X0,and(X0,X1)),
inference(paramodulation,[status(thm)],[f54,f471]) ).
fof(f647,plain,
! [X0,X1] : and(X0,or(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f54,f475]) ).
fof(f650,plain,
and(b1,d3) = d3,
inference(paramodulation,[status(thm)],[f419,f475]) ).
fof(f656,plain,
and(b3,c1) = c1,
inference(paramodulation,[status(thm)],[f82,f475]) ).
fof(f777,plain,
! [X0] : and(i2,and(f2,X0)) = n0,
inference(paramodulation,[status(thm)],[f91,f102]) ).
fof(f875,plain,
i2 = or(d3,i2),
inference(paramodulation,[status(thm)],[f107,f478]) ).
fof(f888,plain,
! [X0,X1] : X0 = or(and(X0,X1),X0),
inference(paramodulation,[status(thm)],[f54,f478]) ).
fof(f913,plain,
and(c2,d3) = d3,
inference(paramodulation,[status(thm)],[f84,f483]) ).
fof(f914,plain,
and(c1,d3) = d3,
inference(paramodulation,[status(thm)],[f83,f483]) ).
fof(f915,plain,
and(b3,c2) = c2,
inference(paramodulation,[status(thm)],[f82,f483]) ).
fof(f981,plain,
or(d3,and(i1,not(i2))) = i1,
inference(paramodulation,[status(thm)],[f107,f76]) ).
fof(f1032,plain,
or(d3,not(or(f1,i2))) = i1,
inference(forward_demodulation,[status(thm)],[f379,f981]) ).
fof(f3051,plain,
and(i2,d3) = d3,
inference(paramodulation,[status(thm)],[f622,f483]) ).
fof(f3150,plain,
and(b3,a1) = a1,
inference(paramodulation,[status(thm)],[f629,f483]) ).
fof(f3640,plain,
or(d3,c1) = or(d3,d1),
inference(paramodulation,[status(thm)],[f83,f219]) ).
fof(f3641,plain,
or(c2,b3) = or(c2,c1),
inference(paramodulation,[status(thm)],[f82,f219]) ).
fof(f3876,plain,
b1 = or(b1,d3),
inference(paramodulation,[status(thm)],[f650,f634]) ).
fof(f5273,plain,
and(b2,c1) = and(a2,c1),
inference(paramodulation,[status(thm)],[f656,f178]) ).
fof(f6349,plain,
and(d3,i2) = d3,
inference(paramodulation,[status(thm)],[f875,f647]) ).
fof(f6422,plain,
and(i2,d3) = and(i2,i1),
inference(paramodulation,[status(thm)],[f107,f312]) ).
fof(f6444,plain,
and(b3,a1) = and(b3,b1),
inference(paramodulation,[status(thm)],[f78,f312]) ).
fof(f6550,plain,
d3 = and(i2,i1),
inference(forward_demodulation,[status(thm)],[f3051,f6422]) ).
fof(f6585,plain,
a1 = and(b3,b1),
inference(forward_demodulation,[status(thm)],[f3150,f6444]) ).
fof(f7660,plain,
c2 = or(c2,d3),
inference(paramodulation,[status(thm)],[f913,f634]) ).
fof(f7689,plain,
not(and(i2,d1)) = or(f2,b1),
inference(paramodulation,[status(thm)],[f80,f346]) ).
fof(f7981,plain,
c1 = or(d3,c1),
inference(paramodulation,[status(thm)],[f914,f888]) ).
fof(f7988,plain,
c1 = or(c1,d3),
inference(paramodulation,[status(thm)],[f914,f634]) ).
fof(f8000,plain,
c1 = or(d3,d1),
inference(backward_demodulation,[status(thm)],[f7981,f3640]) ).
fof(f8009,plain,
b3 = or(c2,b3),
inference(paramodulation,[status(thm)],[f915,f888]) ).
fof(f8028,plain,
b3 = or(c2,c1),
inference(backward_demodulation,[status(thm)],[f8009,f3641]) ).
fof(f9769,plain,
not(or(i2,b1)) = and(f2,d1),
inference(paramodulation,[status(thm)],[f109,f382]) ).
fof(f9953,plain,
! [X0] : not(or(X0,f2)) = and(i2,not(X0)),
inference(paramodulation,[status(thm)],[f182,f375]) ).
fof(f10050,plain,
not(or(i1,f2)) = and(f1,i2),
inference(paramodulation,[status(thm)],[f182,f383]) ).
fof(f10156,plain,
! [X0] : and(or(d3,X0),i2) = or(d3,and(X0,i2)),
inference(paramodulation,[status(thm)],[f6349,f62]) ).
fof(f10181,plain,
or(d3,and(i2,not(i1))) = i2,
inference(paramodulation,[status(thm)],[f6550,f76]) ).
fof(f10193,plain,
or(d3,not(or(i1,f2))) = i2,
inference(forward_demodulation,[status(thm)],[f9953,f10181]) ).
fof(f10194,plain,
or(d3,and(f1,i2)) = i2,
inference(forward_demodulation,[status(thm)],[f10050,f10193]) ).
fof(f10195,plain,
and(or(d3,f1),i2) = i2,
inference(forward_demodulation,[status(thm)],[f10156,f10194]) ).
fof(f10197,plain,
and(b1,i2) = i2,
inference(forward_demodulation,[status(thm)],[f419,f10195]) ).
fof(f10293,plain,
not(or(d2,f1)) = and(b2,i1),
inference(paramodulation,[status(thm)],[f181,f386]) ).
fof(f10645,plain,
not(or(f1,i2)) = and(i1,f2),
inference(paramodulation,[status(thm)],[f181,f393]) ).
fof(f10689,plain,
or(d3,and(i1,f2)) = i1,
inference(backward_demodulation,[status(thm)],[f10645,f1032]) ).
fof(f10922,plain,
not(or(f1,d2)) = and(i1,b2),
inference(paramodulation,[status(thm)],[f181,f397]) ).
fof(f11706,plain,
b1 = or(i2,b1),
inference(paramodulation,[status(thm)],[f10197,f888]) ).
fof(f11709,plain,
and(i2,i2) = and(i2,b1),
inference(paramodulation,[status(thm)],[f10197,f312]) ).
fof(f11713,plain,
b1 = or(b1,i2),
inference(paramodulation,[status(thm)],[f10197,f634]) ).
fof(f11725,plain,
not(b1) = and(f2,d1),
inference(backward_demodulation,[status(thm)],[f11706,f9769]) ).
fof(f11729,plain,
i2 = and(i2,b1),
inference(forward_demodulation,[status(thm)],[f63,f11709]) ).
fof(f11737,plain,
d1 = and(f2,d1),
inference(forward_demodulation,[status(thm)],[f109,f11725]) ).
fof(f12527,plain,
or(d1,c2) = or(c1,c2),
inference(paramodulation,[status(thm)],[f7660,f413]) ).
fof(f12537,plain,
or(d1,c2) = or(c1,d2),
inference(paramodulation,[status(thm)],[f84,f413]) ).
fof(f12581,plain,
or(d1,c2) = b3,
inference(forward_demodulation,[status(thm)],[f82,f12527]) ).
fof(f12588,plain,
b3 = or(c1,d2),
inference(forward_demodulation,[status(thm)],[f12581,f12537]) ).
fof(f12778,plain,
or(d2,c1) = or(c2,d1),
inference(paramodulation,[status(thm)],[f83,f415]) ).
fof(f12779,plain,
or(d2,c1) = or(c2,c1),
inference(paramodulation,[status(thm)],[f7988,f415]) ).
fof(f12829,plain,
b3 = or(c2,d1),
inference(backward_demodulation,[status(thm)],[f12830,f12778]) ).
fof(f12830,plain,
or(d2,c1) = b3,
inference(forward_demodulation,[status(thm)],[f8028,f12779]) ).
fof(f13603,plain,
or(f1,i2) = or(b1,i2),
inference(paramodulation,[status(thm)],[f622,f421]) ).
fof(f13659,plain,
not(b1) = and(i1,f2),
inference(backward_demodulation,[status(thm)],[f13661,f10645]) ).
fof(f13661,plain,
or(f1,i2) = b1,
inference(forward_demodulation,[status(thm)],[f11713,f13603]) ).
fof(f13720,plain,
or(d3,d1) = i1,
inference(backward_demodulation,[status(thm)],[f13721,f10689]) ).
fof(f13721,plain,
d1 = and(i1,f2),
inference(forward_demodulation,[status(thm)],[f109,f13659]) ).
fof(f13737,plain,
~ circuit(input(i1,i2),output(i2,c1)),
inference(backward_demodulation,[status(thm)],[f13902,f94]) ).
fof(f13738,plain,
circuit(input(c1,i2),output(a1,a2)),
inference(backward_demodulation,[status(thm)],[f13902,f93]) ).
fof(f13741,plain,
not(f1) = c1,
inference(backward_demodulation,[status(thm)],[f13902,f181]) ).
fof(f13773,plain,
not(or(f1,d2)) = and(c1,b2),
inference(backward_demodulation,[status(thm)],[f13902,f10922]) ).
fof(f13793,plain,
not(or(d2,f1)) = and(b2,c1),
inference(backward_demodulation,[status(thm)],[f13902,f10293]) ).
fof(f13899,plain,
! [X0] : not(or(f1,X0)) = and(c1,not(X0)),
inference(backward_demodulation,[status(thm)],[f13902,f379]) ).
fof(f13902,plain,
c1 = i1,
inference(forward_demodulation,[status(thm)],[f8000,f13720]) ).
fof(f13905,plain,
~ circuit(input(c1,i2),output(i2,c1)),
inference(forward_demodulation,[status(thm)],[f13902,f13737]) ).
fof(f13918,plain,
not(or(d2,f1)) = and(a2,c1),
inference(forward_demodulation,[status(thm)],[f5273,f13793]) ).
fof(f14349,plain,
or(f2,b1) = or(b2,b1),
inference(paramodulation,[status(thm)],[f3876,f427]) ).
fof(f14354,plain,
or(f2,b1) = or(b2,f1),
inference(paramodulation,[status(thm)],[f135,f427]) ).
fof(f14405,plain,
not(and(i2,d1)) = or(b2,b1),
inference(backward_demodulation,[status(thm)],[f14349,f7689]) ).
fof(f14411,plain,
or(b2,b1) = or(b2,f1),
inference(forward_demodulation,[status(thm)],[f14349,f14354]) ).
fof(f15919,plain,
and(i2,d1) = n0,
inference(paramodulation,[status(thm)],[f11737,f777]) ).
fof(f15984,plain,
not(n0) = or(b2,b1),
inference(backward_demodulation,[status(thm)],[f15919,f14405]) ).
fof(f16045,plain,
n1 = or(b2,f1),
inference(backward_demodulation,[status(thm)],[f16048,f14411]) ).
fof(f16048,plain,
n1 = or(b2,b1),
inference(forward_demodulation,[status(thm)],[f52,f15984]) ).
fof(f25522,plain,
and(b3,not(d1)) = and(c2,not(d1)),
inference(paramodulation,[status(thm)],[f12829,f581]) ).
fof(f25557,plain,
and(n1,not(f1)) = and(b2,not(f1)),
inference(paramodulation,[status(thm)],[f16045,f581]) ).
fof(f25599,plain,
and(b2,not(d3)) = and(f2,not(d3)),
inference(paramodulation,[status(thm)],[f174,f581]) ).
fof(f25625,plain,
and(b3,not(d2)) = and(c1,not(d2)),
inference(paramodulation,[status(thm)],[f12588,f581]) ).
fof(f25735,plain,
and(b3,b1) = and(c2,not(d1)),
inference(forward_demodulation,[status(thm)],[f80,f25522]) ).
fof(f25736,plain,
a1 = and(c2,not(d1)),
inference(forward_demodulation,[status(thm)],[f6585,f25735]) ).
fof(f25737,plain,
a1 = and(c2,b1),
inference(forward_demodulation,[status(thm)],[f80,f25736]) ).
fof(f25794,plain,
not(f1) = and(b2,not(f1)),
inference(forward_demodulation,[status(thm)],[f119,f25557]) ).
fof(f25795,plain,
c1 = and(b2,not(f1)),
inference(forward_demodulation,[status(thm)],[f13741,f25794]) ).
fof(f25796,plain,
c1 = and(a2,c1),
inference(backward_demodulation,[status(thm)],[f25797,f13918]) ).
fof(f25797,plain,
c1 = not(or(d2,f1)),
inference(forward_demodulation,[status(thm)],[f386,f25795]) ).
fof(f25911,plain,
not(or(d2,d3)) = and(f2,not(d3)),
inference(forward_demodulation,[status(thm)],[f386,f25599]) ).
fof(f25912,plain,
not(c2) = and(f2,not(d3)),
inference(forward_demodulation,[status(thm)],[f84,f25911]) ).
fof(f25913,plain,
not(c2) = not(or(i2,d3)),
inference(forward_demodulation,[status(thm)],[f382,f25912]) ).
fof(f25914,plain,
not(c2) = not(i2),
inference(forward_demodulation,[status(thm)],[f622,f25913]) ).
fof(f25919,plain,
not(c2) = f2,
inference(forward_demodulation,[status(thm)],[f91,f25914]) ).
fof(f26010,plain,
and(b3,b2) = and(c1,not(d2)),
inference(forward_demodulation,[status(thm)],[f81,f25625]) ).
fof(f26011,plain,
a2 = and(c1,not(d2)),
inference(forward_demodulation,[status(thm)],[f176,f26010]) ).
fof(f26012,plain,
a2 = and(c1,b2),
inference(backward_demodulation,[status(thm)],[f26013,f13773]) ).
fof(f26013,plain,
a2 = not(or(f1,d2)),
inference(forward_demodulation,[status(thm)],[f13899,f26011]) ).
fof(f27218,plain,
not(f2) = c2,
inference(paramodulation,[status(thm)],[f25919,f75]) ).
fof(f27256,plain,
c2 = i2,
inference(backward_demodulation,[status(thm)],[f27218,f182]) ).
fof(f27347,plain,
circuit(input(c1,c2),output(a1,a2)),
inference(backward_demodulation,[status(thm)],[f27256,f13738]) ).
fof(f27348,plain,
~ circuit(input(c1,i2),output(c2,c1)),
inference(backward_demodulation,[status(thm)],[f27256,f13905]) ).
fof(f27350,plain,
i2 = and(c2,b1),
inference(backward_demodulation,[status(thm)],[f27256,f11729]) ).
fof(f27566,plain,
~ circuit(input(c1,c2),output(c2,c1)),
inference(forward_demodulation,[status(thm)],[f27256,f27348]) ).
fof(f27567,plain,
c2 = and(c2,b1),
inference(forward_demodulation,[status(thm)],[f27256,f27350]) ).
fof(f27596,plain,
~ circuit(input(c1,c2),output(a1,c1)),
inference(backward_demodulation,[status(thm)],[f27886,f27566]) ).
fof(f27597,plain,
circuit(input(c1,a1),output(a1,a2)),
inference(backward_demodulation,[status(thm)],[f27886,f27347]) ).
fof(f27886,plain,
c2 = a1,
inference(forward_demodulation,[status(thm)],[f25737,f27567]) ).
fof(f28290,plain,
~ circuit(input(c1,a1),output(a1,c1)),
inference(forward_demodulation,[status(thm)],[f27886,f27596]) ).
fof(f31361,plain,
a2 = or(a2,c1),
inference(paramodulation,[status(thm)],[f25796,f634]) ).
fof(f33787,plain,
c1 = or(a2,c1),
inference(paramodulation,[status(thm)],[f26012,f888]) ).
fof(f33844,plain,
circuit(input(a2,a1),output(a1,a2)),
inference(backward_demodulation,[status(thm)],[f34253,f27597]) ).
fof(f33845,plain,
~ circuit(input(c1,a1),output(a1,a2)),
inference(backward_demodulation,[status(thm)],[f34253,f28290]) ).
fof(f34253,plain,
c1 = a2,
inference(forward_demodulation,[status(thm)],[f31361,f33787]) ).
fof(f34281,plain,
~ circuit(input(a2,a1),output(a1,a2)),
inference(forward_demodulation,[status(thm)],[f34253,f33845]) ).
fof(f34282,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f34281,f33844]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.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 : Sun Sep 20 20:52:59 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 34.92/4.82 % Refutation found
% 34.92/4.82 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 34.92/4.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.31/4.91 % Elapsed time: 4.545958 seconds
% 2.31/4.91 % CPU time: 35.521249 seconds
% 2.31/4.91 % Total memory used: 173.287 MB
% 2.31/4.91 % Net memory used: 158.692 MB
%------------------------------------------------------------------------------