%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.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:14 AM UTC 2026
% Result : Unsatisfiable 0.18s 5.64s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 35
% Syntax : Number of formulae : 264 ( 264 unt; 0 def)
% Number of atoms : 264 ( 257 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 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 : 147 ( 11 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(and_definition2,axiom,
! [VAR_0] : and(VAR_0,n1) = VAR_0,
file('theBenchmark.p',and_definition2) ).
cnf(c_2,plain,
and(A,n1) = A,
inference(clausify,[status(thm)],[and_definition2]) ).
fof(or_definition1,axiom,
! [VAR_0] : or(VAR_0,n0) = VAR_0,
file('theBenchmark.p',or_definition1) ).
cnf(c_3,plain,
or(A,n0) = A,
inference(clausify,[status(thm)],[or_definition1]) ).
fof(or_definition2,axiom,
! [VAR_0] : or(VAR_0,n1) = n1,
file('theBenchmark.p',or_definition2) ).
cnf(c_4,plain,
or(A,n1) = n1,
inference(clausify,[status(thm)],[or_definition2]) ).
fof(and_commutativity,axiom,
! [VAR_0,VAR_1] : and(VAR_0,VAR_1) = and(VAR_1,VAR_0),
file('theBenchmark.p',and_commutativity) ).
cnf(c_7,plain,
and(A,B) = and(B,A),
inference(clausify,[status(thm)],[and_commutativity]) ).
fof(or_commutativity,axiom,
! [VAR_0,VAR_1] : or(VAR_0,VAR_1) = or(VAR_1,VAR_0),
file('theBenchmark.p',or_commutativity) ).
cnf(c_8,plain,
or(A,B) = or(B,A),
inference(clausify,[status(thm)],[or_commutativity]) ).
fof(and_associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : and(VAR_0,and(VAR_1,VAR_2)) = and(and(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',and_associativity) ).
cnf(c_9,plain,
and(A,and(B,C)) = and(and(A,B),C),
inference(clausify,[status(thm)],[and_associativity]) ).
cnf(c_10,plain,
and(and(A,B),C) = and(A,and(B,C)),
inference(copy,[status(thm)],[c_9]) ).
fof(or_associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : or(VAR_0,or(VAR_1,VAR_2)) = or(or(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',or_associativity) ).
cnf(c_11,plain,
or(A,or(B,C)) = or(or(A,B),C),
inference(clausify,[status(thm)],[or_associativity]) ).
cnf(c_12,plain,
or(or(A,B),C) = or(A,or(B,C)),
inference(copy,[status(thm)],[c_11]) ).
fof(not_canonicalization1,axiom,
! [VAR_0,VAR_1] : not(and(VAR_0,VAR_1)) = or(not(VAR_0),not(VAR_1)),
file('theBenchmark.p',not_canonicalization1) ).
cnf(c_15,plain,
not(and(A,B)) = or(not(A),not(B)),
inference(clausify,[status(thm)],[not_canonicalization1]) ).
fof(not_canonicalization2,axiom,
! [VAR_0,VAR_1] : not(or(VAR_0,VAR_1)) = and(not(VAR_0),not(VAR_1)),
file('theBenchmark.p',not_canonicalization2) ).
cnf(c_16,plain,
not(or(A,B)) = and(not(A),not(B)),
inference(clausify,[status(thm)],[not_canonicalization2]) ).
fof(and_or_canonicalization,axiom,
! [VAR_0,VAR_1,VAR_2] : and(or(VAR_0,VAR_1),VAR_2) = or(and(VAR_0,VAR_2),and(VAR_1,VAR_2)),
file('theBenchmark.p',and_or_canonicalization) ).
cnf(c_17,plain,
and(or(A,B),C) = or(and(A,C),and(B,C)),
inference(clausify,[status(thm)],[and_or_canonicalization]) ).
cnf(c_18,plain,
or(and(A,B),and(C,B)) = and(or(A,C),B),
inference(copy,[status(thm)],[c_17]) ).
fof(and_simplification1,axiom,
! [VAR_0] : and(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',and_simplification1) ).
cnf(c_19,plain,
and(A,A) = A,
inference(clausify,[status(thm)],[and_simplification1]) ).
fof(and_simplification2,axiom,
! [VAR_0,VAR_1] : and(and(VAR_0,VAR_1),VAR_1) = and(VAR_0,VAR_1),
file('theBenchmark.p',and_simplification2) ).
cnf(c_20,plain,
and(and(A,B),B) = and(A,B),
inference(clausify,[status(thm)],[and_simplification2]) ).
cnf(c_21,plain,
and(A,and(B,A)) = and(B,A),
inference(paramod,[status(thm)],[c_7,c_20]) ).
fof(or_simplification2,axiom,
! [VAR_0,VAR_1] : or(or(VAR_0,VAR_1),VAR_1) = or(VAR_0,VAR_1),
file('theBenchmark.p',or_simplification2) ).
cnf(c_25,plain,
or(or(A,B),B) = or(A,B),
inference(clausify,[status(thm)],[or_simplification2]) ).
cnf(c_26,plain,
or(A,or(B,A)) = or(B,A),
inference(paramod,[status(thm)],[c_8,c_25]) ).
fof(or_simplification3,axiom,
! [VAR_0,VAR_1] : or(or(VAR_0,VAR_1),VAR_0) = or(VAR_0,VAR_1),
file('theBenchmark.p',or_simplification3) ).
cnf(c_27,plain,
or(or(A,B),A) = or(A,B),
inference(clausify,[status(thm)],[or_simplification3]) ).
cnf(c_28,plain,
or(A,or(A,B)) = or(A,B),
inference(paramod,[status(thm)],[c_8,c_27]) ).
fof(and_not_simplification1,axiom,
! [VAR_0] : and(VAR_0,not(VAR_0)) = n0,
file('theBenchmark.p',and_not_simplification1) ).
cnf(c_29,plain,
and(A,not(A)) = n0,
inference(clausify,[status(thm)],[and_not_simplification1]) ).
fof(or_not_simplification1,axiom,
! [VAR_0] : or(VAR_0,not(VAR_0)) = n1,
file('theBenchmark.p',or_not_simplification1) ).
cnf(c_33,plain,
or(A,not(A)) = n1,
inference(clausify,[status(thm)],[or_not_simplification1]) ).
fof(not_simplification,axiom,
! [VAR_0] : not(not(VAR_0)) = VAR_0,
file('theBenchmark.p',not_simplification) ).
cnf(c_37,plain,
not(not(A)) = A,
inference(clausify,[status(thm)],[not_simplification]) ).
fof(and_or_not_simplification1,axiom,
! [VAR_0,VAR_1] : or(and(VAR_0,VAR_1),and(VAR_0,not(VAR_1))) = VAR_0,
file('theBenchmark.p',and_or_not_simplification1) ).
cnf(c_38,plain,
or(and(A,B),and(A,not(B))) = A,
inference(clausify,[status(thm)],[and_or_not_simplification1]) ).
fof(constructor1,axiom,
a1 = and(b1,b3),
file('theBenchmark.p',constructor1) ).
cnf(c_40,plain,
a1 = and(b1,b3),
inference(clausify,[status(thm)],[constructor1]) ).
cnf(c_1130,plain,
a1 = and(b3,b1),
inference(paramod,[status(thm)],[c_7,c_40]) ).
cnf(c_41,plain,
and(b3,b1) = a1,
inference(copy,[status(thm)],[c_1130]) ).
fof(constructor2,axiom,
a2 = and(b2,b3),
file('theBenchmark.p',constructor2) ).
cnf(c_42,plain,
a2 = and(b2,b3),
inference(clausify,[status(thm)],[constructor2]) ).
cnf(c_1131,plain,
a2 = and(b3,b2),
inference(paramod,[status(thm)],[c_7,c_42]) ).
cnf(c_43,plain,
and(b3,b2) = a2,
inference(copy,[status(thm)],[c_1131]) ).
fof(constructor3,axiom,
b1 = not(d1),
file('theBenchmark.p',constructor3) ).
cnf(c_44,plain,
b1 = not(d1),
inference(clausify,[status(thm)],[constructor3]) ).
cnf(c_45,plain,
not(d1) = b1,
inference(copy,[status(thm)],[c_44]) ).
fof(constructor4,axiom,
b2 = not(d2),
file('theBenchmark.p',constructor4) ).
cnf(c_46,plain,
b2 = not(d2),
inference(clausify,[status(thm)],[constructor4]) ).
cnf(c_47,plain,
not(d2) = b2,
inference(copy,[status(thm)],[c_46]) ).
fof(constructor5,axiom,
b3 = or(c1,c2),
file('theBenchmark.p',constructor5) ).
cnf(c_48,plain,
b3 = or(c1,c2),
inference(clausify,[status(thm)],[constructor5]) ).
cnf(c_49,plain,
or(c1,c2) = b3,
inference(copy,[status(thm)],[c_48]) ).
fof(constructor6,axiom,
c1 = or(d1,d3),
file('theBenchmark.p',constructor6) ).
cnf(c_50,plain,
c1 = or(d1,d3),
inference(clausify,[status(thm)],[constructor6]) ).
cnf(c_51,plain,
or(d1,d3) = c1,
inference(copy,[status(thm)],[c_50]) ).
fof(constructor7,axiom,
c2 = or(d2,d3),
file('theBenchmark.p',constructor7) ).
cnf(c_52,plain,
c2 = or(d2,d3),
inference(clausify,[status(thm)],[constructor7]) ).
cnf(c_53,plain,
or(d2,d3) = c2,
inference(copy,[status(thm)],[c_52]) ).
fof(constructor8,axiom,
d3 = f3,
file('theBenchmark.p',constructor8) ).
cnf(c_54,plain,
d3 = f3,
inference(clausify,[status(thm)],[constructor8]) ).
fof(constructor9,axiom,
d1 = not(e1),
file('theBenchmark.p',constructor9) ).
cnf(c_55,plain,
d1 = not(e1),
inference(clausify,[status(thm)],[constructor9]) ).
cnf(c_56,plain,
not(e1) = d1,
inference(copy,[status(thm)],[c_55]) ).
fof(constructor10,axiom,
d2 = not(e2),
file('theBenchmark.p',constructor10) ).
cnf(c_57,plain,
d2 = not(e2),
inference(clausify,[status(thm)],[constructor10]) ).
cnf(c_58,plain,
not(e2) = d2,
inference(copy,[status(thm)],[c_57]) ).
fof(constructor11,axiom,
e1 = or(f1,f3),
file('theBenchmark.p',constructor11) ).
cnf(c_59,plain,
e1 = or(f1,f3),
inference(clausify,[status(thm)],[constructor11]) ).
cnf(c_1132,plain,
e1 = or(f3,f1),
inference(paramod,[status(thm)],[c_8,c_59]) ).
cnf(c_60,plain,
or(f3,f1) = e1,
inference(copy,[status(thm)],[c_1132]) ).
fof(constructor12,axiom,
e2 = or(f2,f3),
file('theBenchmark.p',constructor12) ).
cnf(c_61,plain,
e2 = or(f2,f3),
inference(clausify,[status(thm)],[constructor12]) ).
cnf(c_1133,plain,
e2 = or(f3,f2),
inference(paramod,[status(thm)],[c_8,c_61]) ).
cnf(c_62,plain,
or(f3,f2) = e2,
inference(copy,[status(thm)],[c_1133]) ).
fof(constructor13,axiom,
f1 = not(i1),
file('theBenchmark.p',constructor13) ).
cnf(c_63,plain,
f1 = not(i1),
inference(clausify,[status(thm)],[constructor13]) ).
cnf(c_64,plain,
not(i1) = f1,
inference(copy,[status(thm)],[c_63]) ).
fof(constructor14,axiom,
f2 = not(i2),
file('theBenchmark.p',constructor14) ).
cnf(c_65,plain,
f2 = not(i2),
inference(clausify,[status(thm)],[constructor14]) ).
cnf(c_66,plain,
not(i2) = f2,
inference(copy,[status(thm)],[c_65]) ).
fof(constructor15,axiom,
f3 = and(i1,i2),
file('theBenchmark.p',constructor15) ).
cnf(c_67,plain,
f3 = and(i1,i2),
inference(clausify,[status(thm)],[constructor15]) ).
cnf(c_68,plain,
and(i1,i2) = f3,
inference(copy,[status(thm)],[c_67]) ).
fof(circuit_description,axiom,
circuit(input(i1,i2),output(a1,a2)),
file('theBenchmark.p',circuit_description) ).
cnf(c_69,plain,
circuit(input(i1,i2),output(a1,a2)),
inference(clausify,[status(thm)],[circuit_description]) ).
fof(prove_interchange,axiom,
~ circuit(input(i1,i2),output(i2,i1)),
file('theBenchmark.p',prove_interchange) ).
cnf(c_70,plain,
~ circuit(input(i1,i2),output(i2,i1)),
inference(clausify,[status(thm)],[prove_interchange]) ).
cnf(c_1134,plain,
or(d2,f3) = c2,
inference(paramod,[status(thm)],[c_54,c_53]) ).
cnf(c_71,plain,
or(f3,d2) = c2,
inference(paramod,[status(thm)],[c_8,c_1134]) ).
cnf(c_1135,plain,
or(d1,f3) = c1,
inference(paramod,[status(thm)],[c_54,c_51]) ).
cnf(c_72,plain,
or(f3,d1) = c1,
inference(paramod,[status(thm)],[c_8,c_1135]) ).
cnf(c_74,plain,
and(n1,A) = A,
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_75,plain,
or(n0,A) = A,
inference(paramod,[status(thm)],[c_8,c_3]) ).
cnf(c_1136,plain,
and(and(A,B),C) = and(B,and(A,C)),
inference(paramod,[status(thm)],[c_7,c_10]) ).
cnf(c_78,plain,
and(A,and(B,C)) = and(B,and(A,C)),
inference(paramod,[status(thm)],[c_10,c_1136]) ).
cnf(c_1137,plain,
or(or(A,B),C) = or(B,or(A,C)),
inference(paramod,[status(thm)],[c_8,c_12]) ).
cnf(c_80,plain,
or(A,or(B,C)) = or(B,or(A,C)),
inference(paramod,[status(thm)],[c_12,c_1137]) ).
cnf(c_1138,plain,
or(and(A,B),and(n1,B)) = and(n1,B),
inference(paramod,[status(thm)],[c_4,c_18]) ).
cnf(c_1139,plain,
or(and(A,B),B) = and(n1,B),
inference(paramod,[status(thm)],[c_74,c_1138]) ).
cnf(c_1140,plain,
or(B,and(A,B)) = and(n1,B),
inference(paramod,[status(thm)],[c_8,c_1139]) ).
cnf(c_81,plain,
or(A,and(B,A)) = A,
inference(paramod,[status(thm)],[c_74,c_1140]) ).
cnf(c_82,plain,
or(and(A,B),and(C,A)) = and(or(B,C),A),
inference(paramod,[status(thm)],[c_7,c_18]) ).
cnf(c_83,plain,
or(and(A,B),and(B,C)) = and(or(A,C),B),
inference(paramod,[status(thm)],[c_7,c_18]) ).
cnf(c_1141,plain,
or(A,and(B,A)) = and(or(A,B),A),
inference(paramod,[status(thm)],[c_19,c_18]) ).
cnf(c_1142,plain,
A = and(or(A,B),A),
inference(paramod,[status(thm)],[c_81,c_1141]) ).
cnf(c_1143,plain,
A = and(A,or(A,B)),
inference(paramod,[status(thm)],[c_7,c_1142]) ).
cnf(c_88,plain,
and(A,or(A,B)) = A,
inference(copy,[status(thm)],[c_1143]) ).
cnf(c_1144,plain,
or(and(A,B),B) = and(or(A,B),B),
inference(paramod,[status(thm)],[c_19,c_18]) ).
cnf(c_1145,plain,
or(B,and(A,B)) = and(or(A,B),B),
inference(paramod,[status(thm)],[c_8,c_1144]) ).
cnf(c_1146,plain,
B = and(or(A,B),B),
inference(paramod,[status(thm)],[c_81,c_1145]) ).
cnf(c_1147,plain,
B = and(B,or(A,B)),
inference(paramod,[status(thm)],[c_7,c_1146]) ).
cnf(c_89,plain,
and(A,or(B,A)) = A,
inference(copy,[status(thm)],[c_1147]) ).
cnf(c_1148,plain,
or(n0,and(A,not(B))) = and(or(B,A),not(B)),
inference(paramod,[status(thm)],[c_29,c_18]) ).
cnf(c_1149,plain,
and(A,not(B)) = and(or(B,A),not(B)),
inference(paramod,[status(thm)],[c_75,c_1148]) ).
cnf(c_103,plain,
and(or(A,B),not(A)) = and(B,not(A)),
inference(copy,[status(thm)],[c_1149]) ).
cnf(c_1150,plain,
not(a2) = or(not(b3),not(b2)),
inference(paramod,[status(thm)],[c_43,c_15]) ).
cnf(c_140,plain,
or(not(b3),not(b2)) = not(a2),
inference(copy,[status(thm)],[c_1150]) ).
cnf(c_149,plain,
not(b1) = d1,
inference(paramod,[status(thm)],[c_45,c_37]) ).
cnf(c_155,plain,
or(d2,b2) = n1,
inference(paramod,[status(thm)],[c_47,c_33]) ).
cnf(c_157,plain,
not(b2) = d2,
inference(paramod,[status(thm)],[c_47,c_37]) ).
cnf(c_1151,plain,
or(not(b3),d2) = not(a2),
inference(paramod,[status(thm)],[c_157,c_140]) ).
cnf(c_1152,plain,
or(d2,not(b3)) = not(a2),
inference(paramod,[status(thm)],[c_8,c_1151]) ).
cnf(c_160,plain,
not(a2) = or(d2,not(b3)),
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_1153,plain,
not(b3) = and(not(c1),not(c2)),
inference(paramod,[status(thm)],[c_49,c_16]) ).
cnf(c_163,plain,
and(not(c1),not(c2)) = not(b3),
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_1154,plain,
or(c1,b3) = or(c1,c2),
inference(paramod,[status(thm)],[c_49,c_28]) ).
cnf(c_1155,plain,
or(b3,c1) = or(c1,c2),
inference(paramod,[status(thm)],[c_8,c_1154]) ).
cnf(c_165,plain,
or(b3,c1) = b3,
inference(paramod,[status(thm)],[c_49,c_1155]) ).
cnf(c_1156,plain,
not(d1) = e1,
inference(paramod,[status(thm)],[c_56,c_37]) ).
cnf(c_1157,plain,
b1 = e1,
inference(paramod,[status(thm)],[c_45,c_1156]) ).
cnf(c_170,plain,
e1 = b1,
inference(copy,[status(thm)],[c_1157]) ).
cnf(c_173,plain,
or(f3,f1) = b1,
inference(paramod,[status(thm)],[c_170,c_60]) ).
cnf(c_1158,plain,
not(d2) = e2,
inference(paramod,[status(thm)],[c_58,c_37]) ).
cnf(c_1159,plain,
b2 = e2,
inference(paramod,[status(thm)],[c_47,c_1158]) ).
cnf(c_178,plain,
e2 = b2,
inference(copy,[status(thm)],[c_1159]) ).
cnf(c_181,plain,
or(f3,f2) = b2,
inference(paramod,[status(thm)],[c_178,c_62]) ).
cnf(c_182,plain,
and(i1,f1) = n0,
inference(paramod,[status(thm)],[c_64,c_29]) ).
cnf(c_186,plain,
not(f1) = i1,
inference(paramod,[status(thm)],[c_64,c_37]) ).
cnf(c_188,plain,
and(i2,f2) = n0,
inference(paramod,[status(thm)],[c_66,c_29]) ).
cnf(c_192,plain,
not(f2) = i2,
inference(paramod,[status(thm)],[c_66,c_37]) ).
cnf(c_1160,plain,
not(f3) = or(not(i1),not(i2)),
inference(paramod,[status(thm)],[c_68,c_15]) ).
cnf(c_1161,plain,
not(f3) = or(f1,not(i2)),
inference(paramod,[status(thm)],[c_64,c_1160]) ).
cnf(c_196,plain,
not(f3) = or(f1,f2),
inference(paramod,[status(thm)],[c_66,c_1161]) ).
cnf(c_1162,plain,
or(f3,and(i1,not(i2))) = i1,
inference(paramod,[status(thm)],[c_68,c_38]) ).
cnf(c_201,plain,
or(f3,and(i1,f2)) = i1,
inference(paramod,[status(thm)],[c_66,c_1162]) ).
cnf(c_1163,plain,
not(c2) = and(not(f3),not(d2)),
inference(paramod,[status(thm)],[c_71,c_16]) ).
cnf(c_1164,plain,
not(c2) = and(or(f1,f2),not(d2)),
inference(paramod,[status(thm)],[c_196,c_1163]) ).
cnf(c_1165,plain,
not(c2) = and(or(f1,f2),b2),
inference(paramod,[status(thm)],[c_47,c_1164]) ).
cnf(c_204,plain,
not(c2) = and(b2,or(f1,f2)),
inference(paramod,[status(thm)],[c_7,c_1165]) ).
cnf(c_1166,plain,
or(f3,c2) = or(f3,d2),
inference(paramod,[status(thm)],[c_71,c_28]) ).
cnf(c_206,plain,
or(f3,c2) = c2,
inference(paramod,[status(thm)],[c_71,c_1166]) ).
cnf(c_1167,plain,
and(not(c1),and(b2,or(f1,f2))) = not(b3),
inference(paramod,[status(thm)],[c_204,c_163]) ).
cnf(c_1168,plain,
and(and(b2,or(f1,f2)),not(c1)) = not(b3),
inference(paramod,[status(thm)],[c_7,c_1167]) ).
cnf(c_209,plain,
and(b2,and(or(f1,f2),not(c1))) = not(b3),
inference(paramod,[status(thm)],[c_10,c_1168]) ).
cnf(c_210,plain,
or(c1,A) = or(f3,or(d1,A)),
inference(paramod,[status(thm)],[c_72,c_12]) ).
cnf(c_1169,plain,
not(c1) = and(not(f3),not(d1)),
inference(paramod,[status(thm)],[c_72,c_16]) ).
cnf(c_1170,plain,
not(c1) = and(or(f1,f2),not(d1)),
inference(paramod,[status(thm)],[c_196,c_1169]) ).
cnf(c_1171,plain,
not(c1) = and(or(f1,f2),b1),
inference(paramod,[status(thm)],[c_45,c_1170]) ).
cnf(c_212,plain,
not(c1) = and(b1,or(f1,f2)),
inference(paramod,[status(thm)],[c_7,c_1171]) ).
cnf(c_1172,plain,
or(d1,c1) = or(f3,d1),
inference(paramod,[status(thm)],[c_72,c_26]) ).
cnf(c_213,plain,
or(d1,c1) = c1,
inference(paramod,[status(thm)],[c_72,c_1172]) ).
cnf(c_216,plain,
or(f3,or(d1,c2)) = b3,
inference(paramod,[status(thm)],[c_210,c_49]) ).
cnf(c_1173,plain,
and(b2,and(or(f1,f2),and(b1,or(f1,f2)))) = not(b3),
inference(paramod,[status(thm)],[c_212,c_209]) ).
cnf(c_1174,plain,
and(b2,and(b1,or(f1,f2))) = not(b3),
inference(paramod,[status(thm)],[c_21,c_1173]) ).
cnf(c_1175,plain,
and(b1,and(b2,or(f1,f2))) = not(b3),
inference(paramod,[status(thm)],[c_78,c_1174]) ).
cnf(c_217,plain,
not(b3) = and(b1,and(b2,or(f1,f2))),
inference(copy,[status(thm)],[c_1175]) ).
cnf(c_218,plain,
not(a2) = or(d2,and(b1,and(b2,or(f1,f2)))),
inference(paramod,[status(thm)],[c_217,c_160]) ).
cnf(c_1176,plain,
not(b1) = and(not(f3),not(f1)),
inference(paramod,[status(thm)],[c_173,c_16]) ).
cnf(c_1177,plain,
d1 = and(not(f3),not(f1)),
inference(paramod,[status(thm)],[c_149,c_1176]) ).
cnf(c_1178,plain,
d1 = and(or(f1,f2),not(f1)),
inference(paramod,[status(thm)],[c_196,c_1177]) ).
cnf(c_1179,plain,
d1 = and(or(f1,f2),i1),
inference(paramod,[status(thm)],[c_186,c_1178]) ).
cnf(c_1180,plain,
d1 = and(i1,or(f1,f2)),
inference(paramod,[status(thm)],[c_7,c_1179]) ).
cnf(c_279,plain,
and(i1,or(f1,f2)) = d1,
inference(copy,[status(thm)],[c_1180]) ).
cnf(c_1181,plain,
not(b2) = and(not(f3),not(f2)),
inference(paramod,[status(thm)],[c_181,c_16]) ).
cnf(c_1182,plain,
d2 = and(not(f3),not(f2)),
inference(paramod,[status(thm)],[c_157,c_1181]) ).
cnf(c_1183,plain,
d2 = and(or(f1,f2),not(f2)),
inference(paramod,[status(thm)],[c_196,c_1182]) ).
cnf(c_1184,plain,
d2 = and(or(f1,f2),i2),
inference(paramod,[status(thm)],[c_192,c_1183]) ).
cnf(c_1185,plain,
d2 = and(i2,or(f1,f2)),
inference(paramod,[status(thm)],[c_7,c_1184]) ).
cnf(c_285,plain,
and(i2,or(f1,f2)) = d2,
inference(copy,[status(thm)],[c_1185]) ).
cnf(c_1186,plain,
or(n0,and(A,i1)) = and(or(f1,A),i1),
inference(paramod,[status(thm)],[c_182,c_82]) ).
cnf(c_1187,plain,
and(A,i1) = and(or(f1,A),i1),
inference(paramod,[status(thm)],[c_75,c_1186]) ).
cnf(c_1188,plain,
and(A,i1) = and(i1,or(f1,A)),
inference(paramod,[status(thm)],[c_7,c_1187]) ).
cnf(c_317,plain,
and(i1,or(f1,A)) = and(A,i1),
inference(copy,[status(thm)],[c_1188]) ).
cnf(c_1189,plain,
and(f2,i1) = d1,
inference(paramod,[status(thm)],[c_317,c_279]) ).
cnf(c_318,plain,
and(i1,f2) = d1,
inference(paramod,[status(thm)],[c_7,c_1189]) ).
cnf(c_1190,plain,
or(f3,d1) = i1,
inference(paramod,[status(thm)],[c_318,c_201]) ).
cnf(c_319,plain,
c1 = i1,
inference(paramod,[status(thm)],[c_72,c_1190]) ).
cnf(c_1191,plain,
or(d1,i1) = c1,
inference(paramod,[status(thm)],[c_319,c_213]) ).
cnf(c_323,plain,
or(d1,i1) = i1,
inference(paramod,[status(thm)],[c_319,c_1191]) ).
cnf(c_328,plain,
or(b3,i1) = b3,
inference(paramod,[status(thm)],[c_319,c_165]) ).
cnf(c_1192,plain,
or(and(A,i2),n0) = and(or(A,f2),i2),
inference(paramod,[status(thm)],[c_188,c_83]) ).
cnf(c_1193,plain,
or(n0,and(A,i2)) = and(or(A,f2),i2),
inference(paramod,[status(thm)],[c_8,c_1192]) ).
cnf(c_1194,plain,
and(A,i2) = and(or(A,f2),i2),
inference(paramod,[status(thm)],[c_75,c_1193]) ).
cnf(c_1195,plain,
and(A,i2) = and(i2,or(A,f2)),
inference(paramod,[status(thm)],[c_7,c_1194]) ).
cnf(c_356,plain,
and(i2,or(A,f2)) = and(A,i2),
inference(copy,[status(thm)],[c_1195]) ).
cnf(c_1196,plain,
and(f1,i2) = d2,
inference(paramod,[status(thm)],[c_356,c_285]) ).
cnf(c_357,plain,
and(i2,f1) = d2,
inference(paramod,[status(thm)],[c_7,c_1196]) ).
cnf(c_1197,plain,
or(A,c2) = or(f3,or(A,c2)),
inference(paramod,[status(thm)],[c_206,c_80]) ).
cnf(c_378,plain,
or(f3,or(A,c2)) = or(A,c2),
inference(copy,[status(thm)],[c_1197]) ).
cnf(c_379,plain,
or(d1,c2) = b3,
inference(paramod,[status(thm)],[c_378,c_216]) ).
cnf(c_1198,plain,
not(d1) = or(not(i1),not(f2)),
inference(paramod,[status(thm)],[c_318,c_15]) ).
cnf(c_1199,plain,
b1 = or(not(i1),not(f2)),
inference(paramod,[status(thm)],[c_45,c_1198]) ).
cnf(c_1200,plain,
b1 = or(f1,not(f2)),
inference(paramod,[status(thm)],[c_64,c_1199]) ).
cnf(c_1201,plain,
b1 = or(f1,i2),
inference(paramod,[status(thm)],[c_192,c_1200]) ).
cnf(c_1202,plain,
b1 = or(i2,f1),
inference(paramod,[status(thm)],[c_8,c_1201]) ).
cnf(c_465,plain,
or(i2,f1) = b1,
inference(copy,[status(thm)],[c_1202]) ).
cnf(c_1203,plain,
not(i1) = and(not(d1),not(i1)),
inference(paramod,[status(thm)],[c_323,c_16]) ).
cnf(c_1204,plain,
f1 = and(not(d1),not(i1)),
inference(paramod,[status(thm)],[c_64,c_1203]) ).
cnf(c_1205,plain,
f1 = and(b1,not(i1)),
inference(paramod,[status(thm)],[c_45,c_1204]) ).
cnf(c_1206,plain,
f1 = and(b1,f1),
inference(paramod,[status(thm)],[c_64,c_1205]) ).
cnf(c_517,plain,
and(b1,f1) = f1,
inference(copy,[status(thm)],[c_1206]) ).
cnf(c_1207,plain,
not(b3) = and(not(b3),not(i1)),
inference(paramod,[status(thm)],[c_328,c_16]) ).
cnf(c_1208,plain,
and(b1,and(b2,or(f1,f2))) = and(not(b3),not(i1)),
inference(paramod,[status(thm)],[c_217,c_1207]) ).
cnf(c_1209,plain,
and(b1,and(b2,or(f1,f2))) = and(and(b1,and(b2,or(f1,f2))),not(i1)),
inference(paramod,[status(thm)],[c_217,c_1208]) ).
cnf(c_1210,plain,
and(b1,and(b2,or(f1,f2))) = and(and(b1,and(b2,or(f1,f2))),f1),
inference(paramod,[status(thm)],[c_64,c_1209]) ).
cnf(c_1211,plain,
and(b1,and(b2,or(f1,f2))) = and(f1,and(b1,and(b2,or(f1,f2)))),
inference(paramod,[status(thm)],[c_7,c_1210]) ).
cnf(c_1212,plain,
and(b1,and(b2,or(f1,f2))) = and(b1,and(f1,and(b2,or(f1,f2)))),
inference(paramod,[status(thm)],[c_78,c_1211]) ).
cnf(c_1213,plain,
and(b1,and(b2,or(f1,f2))) = and(b1,and(b2,and(f1,or(f1,f2)))),
inference(paramod,[status(thm)],[c_78,c_1212]) ).
cnf(c_520,plain,
and(b1,and(b2,or(f1,f2))) = and(b1,and(b2,f1)),
inference(paramod,[status(thm)],[c_88,c_1213]) ).
cnf(c_525,plain,
not(a2) = or(d2,and(b1,and(b2,f1))),
inference(paramod,[status(thm)],[c_520,c_218]) ).
cnf(c_1214,plain,
and(f1,d2) = and(i2,f1),
inference(paramod,[status(thm)],[c_357,c_21]) ).
cnf(c_1215,plain,
and(d2,f1) = and(i2,f1),
inference(paramod,[status(thm)],[c_7,c_1214]) ).
cnf(c_560,plain,
and(d2,f1) = d2,
inference(paramod,[status(thm)],[c_357,c_1215]) ).
cnf(c_628,plain,
and(i2,b1) = i2,
inference(paramod,[status(thm)],[c_465,c_88]) ).
cnf(c_1216,plain,
and(A,f1) = and(b1,and(A,f1)),
inference(paramod,[status(thm)],[c_517,c_78]) ).
cnf(c_653,plain,
and(b1,and(A,f1)) = and(A,f1),
inference(copy,[status(thm)],[c_1216]) ).
cnf(c_658,plain,
not(a2) = or(d2,and(b2,f1)),
inference(paramod,[status(thm)],[c_653,c_525]) ).
cnf(c_1217,plain,
or(d2,and(A,f1)) = and(or(d2,A),f1),
inference(paramod,[status(thm)],[c_560,c_18]) ).
cnf(c_688,plain,
or(d2,and(A,f1)) = and(f1,or(d2,A)),
inference(paramod,[status(thm)],[c_7,c_1217]) ).
cnf(c_1218,plain,
not(a2) = and(f1,or(d2,b2)),
inference(paramod,[status(thm)],[c_688,c_658]) ).
cnf(c_1219,plain,
not(a2) = and(f1,n1),
inference(paramod,[status(thm)],[c_155,c_1218]) ).
cnf(c_1220,plain,
not(a2) = and(n1,f1),
inference(paramod,[status(thm)],[c_7,c_1219]) ).
cnf(c_698,plain,
not(a2) = f1,
inference(paramod,[status(thm)],[c_74,c_1220]) ).
cnf(c_1221,plain,
not(f1) = a2,
inference(paramod,[status(thm)],[c_698,c_37]) ).
cnf(c_1222,plain,
i1 = a2,
inference(paramod,[status(thm)],[c_186,c_1221]) ).
cnf(c_707,plain,
a2 = i1,
inference(copy,[status(thm)],[c_1222]) ).
cnf(c_742,plain,
circuit(input(i1,i2),output(a1,i1)),
inference(paramod,[status(thm)],[c_707,c_69]) ).
cnf(c_1223,plain,
and(b2,not(f3)) = and(f2,not(f3)),
inference(paramod,[status(thm)],[c_181,c_103]) ).
cnf(c_1224,plain,
and(b2,or(f1,f2)) = and(f2,not(f3)),
inference(paramod,[status(thm)],[c_196,c_1223]) ).
cnf(c_1225,plain,
and(b2,or(f1,f2)) = and(f2,or(f1,f2)),
inference(paramod,[status(thm)],[c_196,c_1224]) ).
cnf(c_1077,plain,
and(b2,or(f1,f2)) = f2,
inference(paramod,[status(thm)],[c_89,c_1225]) ).
cnf(c_1226,plain,
and(b3,not(d1)) = and(c2,not(d1)),
inference(paramod,[status(thm)],[c_379,c_103]) ).
cnf(c_1227,plain,
and(b3,b1) = and(c2,not(d1)),
inference(paramod,[status(thm)],[c_45,c_1226]) ).
cnf(c_1228,plain,
a1 = and(c2,not(d1)),
inference(paramod,[status(thm)],[c_41,c_1227]) ).
cnf(c_1229,plain,
a1 = and(c2,b1),
inference(paramod,[status(thm)],[c_45,c_1228]) ).
cnf(c_1230,plain,
a1 = and(b1,c2),
inference(paramod,[status(thm)],[c_7,c_1229]) ).
cnf(c_1086,plain,
and(b1,c2) = a1,
inference(copy,[status(thm)],[c_1230]) ).
cnf(c_1092,plain,
not(c2) = f2,
inference(paramod,[status(thm)],[c_1077,c_204]) ).
cnf(c_1231,plain,
not(f2) = c2,
inference(paramod,[status(thm)],[c_1092,c_37]) ).
cnf(c_1232,plain,
i2 = c2,
inference(paramod,[status(thm)],[c_192,c_1231]) ).
cnf(c_1103,plain,
c2 = i2,
inference(copy,[status(thm)],[c_1232]) ).
cnf(c_1233,plain,
and(b1,i2) = a1,
inference(paramod,[status(thm)],[c_1103,c_1086]) ).
cnf(c_1234,plain,
and(i2,b1) = a1,
inference(paramod,[status(thm)],[c_7,c_1233]) ).
cnf(c_1235,plain,
i2 = a1,
inference(paramod,[status(thm)],[c_628,c_1234]) ).
cnf(c_1104,plain,
a1 = i2,
inference(copy,[status(thm)],[c_1235]) ).
cnf(c_1128,plain,
circuit(input(i1,i2),output(i2,i1)),
inference(paramod,[status(thm)],[c_1104,c_742]) ).
cnf(c_1129,plain,
$false,
inference(resolve,[status(thm)],[c_1128,c_70]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n018.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Fri Sep 25 16:01:26 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.39 % Process 2375103 was started by sandbox on n018,
% 0.11/5.39 % Fri Sep 25 16:01:26 2026
% 0.11/5.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/5.39
% 0.11/5.39 % From the command line: assign(max_seconds, 300).
% 0.18/5.64
% 0.18/5.64 % SZS status Unsatisfiable for theBenchmark
% 0.18/5.64
% 0.18/5.64 % Proof 1 at 0.16 (+ 0.08) seconds.
% 0.18/5.64 % Length of proof is 123.
% 0.18/5.64 % Level of proof is 15.
% 0.18/5.64 % Maximum clause weight is 13.000.
% 0.18/5.64 % Given clauses 152.
% 0.18/5.64
% 0.18/5.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------