%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : HWV001-1 : TPTP v9.2.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:28:41 PM UTC 2026
% Result : Unsatisfiable 1.40s 1.77s
% Output : CNFRefutation 1.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 31
% Syntax : Number of clauses : 152 ( 152 unt; 0 nHn; 116 RR)
% Number of literals : 152 ( 146 equ; 2 neg)
% Maximal clause size : 1 ( 1 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 : 60 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_canonicalization1,axiom,
not(and(X1,X2)) = or(not(X1),not(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization1) ).
cnf(constructor14,negated_conjecture,
f2 = not(i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor14) ).
cnf(or_commutativity,axiom,
or(X1,X2) = or(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_commutativity) ).
cnf(and_not_simplification3,axiom,
and(and(X1,X2),not(X1)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_simplification3) ).
cnf(and_associativity,axiom,
and(X1,and(X2,X3)) = and(and(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_associativity) ).
cnf(not_simplification,axiom,
not(not(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_simplification) ).
cnf(constructor13,negated_conjecture,
f1 = not(i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor13) ).
cnf(constructor15,negated_conjecture,
f3 = and(i1,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor15) ).
cnf(constructor12,negated_conjecture,
e2 = or(f2,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor12) ).
cnf(constructor10,negated_conjecture,
d2 = not(e2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor10) ).
cnf(constructor4,negated_conjecture,
b2 = not(d2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor4) ).
cnf(and_commutativity,axiom,
and(X1,X2) = and(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_commutativity) ).
cnf(or_definition1,axiom,
or(X1,n0) = X1,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',or_definition1) ).
cnf(and_or_not_simplification2,axiom,
or(and(X1,X2),and(X2,not(X1))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification2) ).
cnf(constructor11,negated_conjecture,
e1 = or(f1,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor11) ).
cnf(constructor9,negated_conjecture,
d1 = not(e1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor9) ).
cnf(constructor3,negated_conjecture,
b1 = not(d1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor3) ).
cnf(or_not_simplification1,axiom,
or(X1,not(X1)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_simplification1) ).
cnf(or_associativity,axiom,
or(X1,or(X2,X3)) = or(or(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_associativity) ).
cnf(and_simplification2,axiom,
and(and(X1,X2),X2) = and(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_simplification2) ).
cnf(not_definition2,axiom,
not(n1) = n0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',not_definition2) ).
cnf(and_or_not_simplification1,axiom,
or(and(X1,X2),and(X1,not(X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification1) ).
cnf(constructor7,negated_conjecture,
c2 = or(d2,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor7) ).
cnf(constructor8,negated_conjecture,
d3 = f3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor8) ).
cnf(not_definition1,axiom,
not(n0) = n1,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',not_definition1) ).
cnf(constructor6,negated_conjecture,
c1 = or(d1,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor6) ).
cnf(constructor5,negated_conjecture,
b3 = or(c1,c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor5) ).
cnf(constructor1,negated_conjecture,
a1 = and(b1,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor1) ).
cnf(constructor2,negated_conjecture,
a2 = and(b2,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor2) ).
cnf(circuit_description,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit_description) ).
cnf(prove_interchange,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_interchange) ).
cnf(c_0_31,axiom,
not(and(X1,X2)) = or(not(X1),not(X2)),
not_canonicalization1 ).
cnf(c_0_32,negated_conjecture,
f2 = not(i2),
constructor14 ).
cnf(c_0_33,axiom,
or(X1,X2) = or(X2,X1),
or_commutativity ).
cnf(c_0_34,axiom,
and(and(X1,X2),not(X1)) = n0,
and_not_simplification3 ).
cnf(c_0_35,axiom,
and(X1,and(X2,X3)) = and(and(X1,X2),X3),
and_associativity ).
cnf(c_0_36,axiom,
not(not(X1)) = X1,
not_simplification ).
cnf(c_0_37,negated_conjecture,
or(f2,not(X1)) = not(and(X1,i2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_32]),c_0_33]) ).
cnf(c_0_38,negated_conjecture,
f1 = not(i1),
constructor13 ).
cnf(c_0_39,negated_conjecture,
f3 = and(i1,i2),
constructor15 ).
cnf(c_0_40,negated_conjecture,
e2 = or(f2,f3),
constructor12 ).
cnf(c_0_41,negated_conjecture,
d2 = not(e2),
constructor10 ).
cnf(c_0_42,negated_conjecture,
b2 = not(d2),
constructor4 ).
cnf(c_0_43,plain,
and(X1,and(X2,not(X1))) = n0,
inference(rw,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_44,negated_conjecture,
not(f2) = i2,
inference(spm,[status(thm)],[c_0_36,c_0_32]) ).
cnf(c_0_45,negated_conjecture,
not(f3) = or(f1,f2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_39]),c_0_33]) ).
cnf(c_0_46,negated_conjecture,
or(f3,f2) = e2,
inference(rw,[status(thm)],[c_0_40,c_0_33]) ).
cnf(c_0_47,negated_conjecture,
e2 = b2,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_41]),c_0_42]) ).
cnf(c_0_48,negated_conjecture,
and(f2,and(X1,i2)) = n0,
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_49,axiom,
and(X1,X2) = and(X2,X1),
and_commutativity ).
cnf(c_0_50,axiom,
or(X1,n0) = X1,
or_definition1 ).
cnf(c_0_51,negated_conjecture,
not(or(f1,f2)) = f3,
inference(spm,[status(thm)],[c_0_36,c_0_45]) ).
cnf(c_0_52,negated_conjecture,
or(f3,f2) = b2,
inference(rw,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_53,axiom,
or(and(X1,X2),and(X2,not(X1))) = X2,
and_or_not_simplification2 ).
cnf(c_0_54,negated_conjecture,
and(f3,f2) = n0,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_39]),c_0_49]) ).
cnf(c_0_55,plain,
or(n0,X1) = X1,
inference(spm,[status(thm)],[c_0_50,c_0_33]) ).
cnf(c_0_56,negated_conjecture,
not(and(i2,or(f1,f2))) = b2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_51]),c_0_33]),c_0_52]),c_0_49]) ).
cnf(c_0_57,negated_conjecture,
not(b2) = d2,
inference(spm,[status(thm)],[c_0_36,c_0_42]) ).
cnf(c_0_58,negated_conjecture,
and(f2,or(f1,f2)) = f2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_45]),c_0_55]) ).
cnf(c_0_59,negated_conjecture,
and(i2,or(f1,f2)) = d2,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_56]),c_0_57]) ).
cnf(c_0_60,negated_conjecture,
not(and(i2,b2)) = or(d2,f2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_57]),c_0_49]),c_0_33]) ).
cnf(c_0_61,negated_conjecture,
or(f1,f2) = or(d2,f2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_58]),c_0_44]),c_0_49]),c_0_59]),c_0_33]) ).
cnf(c_0_62,negated_conjecture,
not(or(d2,f2)) = and(i2,b2),
inference(spm,[status(thm)],[c_0_36,c_0_60]) ).
cnf(c_0_63,negated_conjecture,
e1 = or(f1,f3),
constructor11 ).
cnf(c_0_64,negated_conjecture,
d1 = not(e1),
constructor9 ).
cnf(c_0_65,negated_conjecture,
b1 = not(d1),
constructor3 ).
cnf(c_0_66,axiom,
or(X1,not(X1)) = n1,
or_not_simplification1 ).
cnf(c_0_67,axiom,
or(X1,or(X2,X3)) = or(or(X1,X2),X3),
or_associativity ).
cnf(c_0_68,axiom,
and(and(X1,X2),X2) = and(X1,X2),
and_simplification2 ).
cnf(c_0_69,negated_conjecture,
and(i2,b2) = f3,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_51,c_0_61]),c_0_62]) ).
cnf(c_0_70,negated_conjecture,
or(f3,f1) = e1,
inference(rw,[status(thm)],[c_0_63,c_0_33]) ).
cnf(c_0_71,negated_conjecture,
e1 = b1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_64]),c_0_65]) ).
cnf(c_0_72,negated_conjecture,
or(f1,not(X1)) = not(and(X1,i1)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_38]),c_0_33]) ).
cnf(c_0_73,negated_conjecture,
or(b2,f1) = n1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_51]),c_0_67]),c_0_33]),c_0_52]),c_0_33]) ).
cnf(c_0_74,plain,
and(X1,and(X2,X1)) = and(X2,X1),
inference(rw,[status(thm)],[c_0_68,c_0_49]) ).
cnf(c_0_75,negated_conjecture,
not(or(d2,f2)) = f3,
inference(rw,[status(thm)],[c_0_62,c_0_69]) ).
cnf(c_0_76,negated_conjecture,
or(f3,f1) = b1,
inference(rw,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_77,negated_conjecture,
not(and(i1,d2)) = n1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_42]),c_0_33]),c_0_73]),c_0_49]) ).
cnf(c_0_78,axiom,
not(n1) = n0,
not_definition2 ).
cnf(c_0_79,negated_conjecture,
or(i2,not(X1)) = not(and(X1,f2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_44]),c_0_33]) ).
cnf(c_0_80,negated_conjecture,
not(f1) = i1,
inference(spm,[status(thm)],[c_0_36,c_0_38]) ).
cnf(c_0_81,axiom,
or(and(X1,X2),and(X1,not(X2))) = X1,
and_or_not_simplification1 ).
cnf(c_0_82,negated_conjecture,
and(i2,f3) = f3,
inference(spm,[status(thm)],[c_0_74,c_0_39]) ).
cnf(c_0_83,negated_conjecture,
c2 = or(d2,d3),
constructor7 ).
cnf(c_0_84,negated_conjecture,
d3 = f3,
constructor8 ).
cnf(c_0_85,negated_conjecture,
not(and(i2,d1)) = or(b1,f2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_65]),c_0_49]),c_0_33]) ).
cnf(c_0_86,negated_conjecture,
not(and(i1,or(d2,f2))) = b1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_75]),c_0_33]),c_0_76]),c_0_49]) ).
cnf(c_0_87,negated_conjecture,
and(i2,or(d2,f2)) = d2,
inference(rw,[status(thm)],[c_0_59,c_0_61]) ).
cnf(c_0_88,negated_conjecture,
and(i1,d2) = n0,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_77]),c_0_78]) ).
cnf(c_0_89,axiom,
not(n0) = n1,
not_definition1 ).
cnf(c_0_90,negated_conjecture,
not(and(i1,f2)) = or(i2,f1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_44]),c_0_49]),c_0_33]) ).
cnf(c_0_91,negated_conjecture,
and(f2,or(d2,f2)) = f2,
inference(rw,[status(thm)],[c_0_58,c_0_61]) ).
cnf(c_0_92,negated_conjecture,
not(and(d1,f2)) = or(i2,b1),
inference(spm,[status(thm)],[c_0_79,c_0_65]) ).
cnf(c_0_93,negated_conjecture,
and(f1,and(X1,i1)) = n0,
inference(spm,[status(thm)],[c_0_43,c_0_80]) ).
cnf(c_0_94,negated_conjecture,
or(f3,and(i2,not(f3))) = i2,
inference(spm,[status(thm)],[c_0_81,c_0_82]) ).
cnf(c_0_95,negated_conjecture,
or(d2,f3) = c2,
inference(rw,[status(thm)],[c_0_83,c_0_84]) ).
cnf(c_0_96,negated_conjecture,
not(or(b1,f2)) = and(i2,d1),
inference(spm,[status(thm)],[c_0_36,c_0_85]) ).
cnf(c_0_97,negated_conjecture,
or(b1,f2) = n1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_86]),c_0_33]),c_0_35]),c_0_49]),c_0_87]),c_0_88]),c_0_89]) ).
cnf(c_0_98,negated_conjecture,
not(or(i2,f1)) = and(i1,f2),
inference(spm,[status(thm)],[c_0_36,c_0_90]) ).
cnf(c_0_99,negated_conjecture,
or(i2,f1) = or(i2,b1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_86]),c_0_35]),c_0_49]),c_0_91]),c_0_90]) ).
cnf(c_0_100,negated_conjecture,
not(or(i2,b1)) = and(d1,f2),
inference(spm,[status(thm)],[c_0_36,c_0_92]) ).
cnf(c_0_101,negated_conjecture,
c1 = or(d1,d3),
constructor6 ).
cnf(c_0_102,negated_conjecture,
and(f1,and(i1,X1)) = n0,
inference(spm,[status(thm)],[c_0_93,c_0_49]) ).
cnf(c_0_103,negated_conjecture,
or(f3,and(i2,or(f1,f2))) = i2,
inference(rw,[status(thm)],[c_0_94,c_0_45]) ).
cnf(c_0_104,negated_conjecture,
or(f3,d2) = c2,
inference(rw,[status(thm)],[c_0_95,c_0_33]) ).
cnf(c_0_105,negated_conjecture,
and(i2,d1) = n0,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_96,c_0_97]),c_0_78]) ).
cnf(c_0_106,negated_conjecture,
and(d1,f2) = and(i1,f2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_98,c_0_99]),c_0_100]) ).
cnf(c_0_107,negated_conjecture,
or(d1,f3) = c1,
inference(rw,[status(thm)],[c_0_101,c_0_84]) ).
cnf(c_0_108,negated_conjecture,
and(f3,f1) = n0,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102,c_0_39]),c_0_49]) ).
cnf(c_0_109,negated_conjecture,
not(b1) = d1,
inference(spm,[status(thm)],[c_0_36,c_0_65]) ).
cnf(c_0_110,negated_conjecture,
b3 = or(c1,c2),
constructor5 ).
cnf(c_0_111,negated_conjecture,
c2 = i2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_103,c_0_59]),c_0_104]) ).
cnf(c_0_112,negated_conjecture,
or(f3,and(i1,f2)) = i1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_39]),c_0_32]) ).
cnf(c_0_113,negated_conjecture,
and(i1,f2) = d1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_105]),c_0_32]),c_0_106]),c_0_55]) ).
cnf(c_0_114,negated_conjecture,
or(f3,d1) = c1,
inference(rw,[status(thm)],[c_0_107,c_0_33]) ).
cnf(c_0_115,negated_conjecture,
and(f1,or(d2,f2)) = f1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_108]),c_0_45]),c_0_61]),c_0_55]) ).
cnf(c_0_116,negated_conjecture,
and(i1,or(d2,f2)) = d1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_86]),c_0_109]) ).
cnf(c_0_117,negated_conjecture,
not(and(i1,b1)) = or(d1,f1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_109]),c_0_49]),c_0_33]) ).
cnf(c_0_118,negated_conjecture,
not(and(f1,f2)) = or(i1,i2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_80]),c_0_33]) ).
cnf(c_0_119,negated_conjecture,
or(i2,c1) = b3,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_110,c_0_111]),c_0_33]) ).
cnf(c_0_120,negated_conjecture,
c1 = i1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_112,c_0_113]),c_0_114]) ).
cnf(c_0_121,negated_conjecture,
or(i1,not(X1)) = not(and(X1,f1)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_80]),c_0_33]) ).
cnf(c_0_122,negated_conjecture,
or(d2,f2) = or(d1,f1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_115]),c_0_80]),c_0_49]),c_0_116]),c_0_33]) ).
cnf(c_0_123,negated_conjecture,
not(or(d1,f1)) = and(i1,b1),
inference(spm,[status(thm)],[c_0_36,c_0_117]) ).
cnf(c_0_124,negated_conjecture,
not(or(i1,i2)) = and(f1,f2),
inference(spm,[status(thm)],[c_0_36,c_0_118]) ).
cnf(c_0_125,negated_conjecture,
or(i1,i2) = b3,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_119,c_0_120]),c_0_33]) ).
cnf(c_0_126,negated_conjecture,
a1 = and(b1,b3),
constructor1 ).
cnf(c_0_127,negated_conjecture,
not(and(b2,f1)) = or(i1,d2),
inference(spm,[status(thm)],[c_0_121,c_0_57]) ).
cnf(c_0_128,negated_conjecture,
and(d2,f1) = d2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_88]),c_0_38]),c_0_55]) ).
cnf(c_0_129,negated_conjecture,
and(i1,b1) = f3,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_75,c_0_122]),c_0_123]) ).
cnf(c_0_130,negated_conjecture,
or(d1,not(X1)) = not(and(X1,b1)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_109]),c_0_33]) ).
cnf(c_0_131,negated_conjecture,
not(b3) = and(f1,f2),
inference(rw,[status(thm)],[c_0_124,c_0_125]) ).
cnf(c_0_132,negated_conjecture,
and(b3,b1) = a1,
inference(rw,[status(thm)],[c_0_126,c_0_49]) ).
cnf(c_0_133,negated_conjecture,
or(d1,and(f1,f2)) = f2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_113]),c_0_38]),c_0_49]) ).
cnf(c_0_134,negated_conjecture,
or(d2,not(X1)) = not(and(X1,b2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_57]),c_0_33]) ).
cnf(c_0_135,negated_conjecture,
not(or(i1,d2)) = and(b2,f1),
inference(spm,[status(thm)],[c_0_36,c_0_127]) ).
cnf(c_0_136,negated_conjecture,
or(d2,and(b2,f1)) = f1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_128]),c_0_42]),c_0_49]) ).
cnf(c_0_137,negated_conjecture,
not(or(d1,f1)) = f3,
inference(rw,[status(thm)],[c_0_123,c_0_129]) ).
cnf(c_0_138,negated_conjecture,
not(a1) = f2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_131]),c_0_132]),c_0_133]) ).
cnf(c_0_139,negated_conjecture,
not(and(b2,or(i1,d2))) = f1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_135]),c_0_136]),c_0_49]) ).
cnf(c_0_140,negated_conjecture,
not(and(b2,or(d1,f1))) = i2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_137]),c_0_33]),c_0_104]),c_0_111]),c_0_49]) ).
cnf(c_0_141,negated_conjecture,
and(f1,or(d1,f1)) = f1,
inference(rw,[status(thm)],[c_0_115,c_0_122]) ).
cnf(c_0_142,negated_conjecture,
a2 = and(b2,b3),
constructor2 ).
cnf(c_0_143,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
circuit_description ).
cnf(c_0_144,negated_conjecture,
a1 = i2,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_138]),c_0_44]) ).
cnf(c_0_145,negated_conjecture,
and(b2,or(i1,d2)) = i1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_139]),c_0_80]) ).
cnf(c_0_146,negated_conjecture,
or(i1,d2) = b3,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_140]),c_0_125]),c_0_35]),c_0_49]),c_0_141]),c_0_127]) ).
cnf(c_0_147,negated_conjecture,
and(b3,b2) = a2,
inference(rw,[status(thm)],[c_0_142,c_0_49]) ).
cnf(c_0_148,negated_conjecture,
circuit(input(i1,i2),output(i2,a2)),
inference(rw,[status(thm)],[c_0_143,c_0_144]) ).
cnf(c_0_149,negated_conjecture,
a2 = i1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_145,c_0_146]),c_0_49]),c_0_147]) ).
cnf(c_0_150,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
prove_interchange ).
cnf(c_0_151,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_148,c_0_149]),c_0_150]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV001-1 : TPTP v9.2.1. Released v1.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n022.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon May 4 19:09:51 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 1.40/1.77 % Version : CSE_E---1.7
% 1.40/1.77 % Problem : theBenchmark.p
% 1.40/1.77 % SZS status Unsatisfiable for theBenchmark.p
% 1.40/1.77 % SZS output start CNFRefutation
% See solution above
% 1.40/1.77 % Total time : 1.369s
%------------------------------------------------------------------------------