%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:39:53 PM UTC 2026
% Result : Unsatisfiable 6.06s 2.21s
% Output : CNFRefutation 6.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 53
% Syntax : Number of formulae : 326 ( 326 unt; 17 def)
% Number of atoms : 981 ( 318 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 18 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 19 con; 0-2 aty)
% Number of variables : 125 ( 0 sgn 125 !; 0 ?; 88 :)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0] : or(X0,n0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',or_definition1) ).
fof(f5,axiom,
! [X0] : or(X0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',or_definition2) ).
fof(f6,plain,
! [X0] : n1 = or(X0,n1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
not(n0) = n1,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',not_definition1) ).
fof(f8,plain,
n1 = not(n0),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
not(n1) = n0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWC002-0.ax',not_definition2) ).
fof(f10,plain,
n0 = not(n1),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0,X1] : and(X0,X1) = and(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_commutativity) ).
fof(f12,axiom,
! [X0,X1] : or(X0,X1) = or(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_commutativity) ).
fof(f13,axiom,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(and(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_associativity) ).
fof(f14,axiom,
! [X2,X0,X1] : or(X0,or(X1,X2)) = or(or(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_associativity) ).
fof(f17,axiom,
! [X0,X1] : not(and(X0,X1)) = or(not(X0),not(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization1) ).
fof(f18,axiom,
! [X0,X1] : not(or(X0,X1)) = and(not(X0),not(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization2) ).
fof(f19,axiom,
! [X2,X0,X1] : and(or(X0,X1),X2) = or(and(X0,X2),and(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_canonicalization) ).
fof(f20,axiom,
! [X0] : and(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_simplification1) ).
fof(f25,axiom,
! [X0] : or(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_simplification1) ).
fof(f30,axiom,
! [X0] : and(X0,not(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_simplification1) ).
fof(f31,plain,
! [X0] : n0 = and(X0,not(X0)),
inference(reorient_equations,[],[f30]) ).
fof(f34,axiom,
! [X0,X1] : and(and(X0,X1),not(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_simplification3) ).
fof(f35,plain,
! [X0,X1] : n0 = and(and(X0,X1),not(X0)),
inference(reorient_equations,[],[f34]) ).
fof(f40,axiom,
! [X0,X1] : or(or(X0,X1),not(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_simplification3) ).
fof(f41,plain,
! [X0,X1] : n1 = or(or(X0,X1),not(X0)),
inference(reorient_equations,[],[f40]) ).
fof(f42,axiom,
! [X0] : not(not(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_simplification) ).
fof(f43,axiom,
! [X0,X1] : or(and(X0,X1),and(X0,not(X1))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification1) ).
fof(f44,axiom,
! [X0,X1] : or(and(X0,X1),and(X1,not(X0))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification2) ).
fof(f45,negated_conjecture,
a1 = and(b1,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor1) ).
fof(f46,negated_conjecture,
a2 = and(b2,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor2) ).
fof(f47,negated_conjecture,
b1 = not(d1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor3) ).
fof(f48,negated_conjecture,
b2 = not(d2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor4) ).
fof(f49,negated_conjecture,
b3 = or(c1,c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor5) ).
fof(f50,negated_conjecture,
c1 = or(d1,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor6) ).
fof(f51,negated_conjecture,
c2 = or(d2,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor7) ).
fof(f52,negated_conjecture,
d3 = f3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor8) ).
fof(f53,negated_conjecture,
d1 = not(e1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor9) ).
fof(f54,negated_conjecture,
d2 = not(e2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor10) ).
fof(f55,negated_conjecture,
e1 = or(f1,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor11) ).
fof(f56,negated_conjecture,
e2 = or(f2,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor12) ).
fof(f57,negated_conjecture,
f1 = not(i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor13) ).
fof(f58,negated_conjecture,
f2 = not(i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor14) ).
fof(f59,negated_conjecture,
f3 = and(i1,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor15) ).
fof(f60,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit_description) ).
fof(f61,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_interchange) ).
fof(f62,plain,
c1 = or(d1,f3),
inference(definition_unfolding,[],[f50,f52]) ).
fof(f63,plain,
c2 = or(d2,f3),
inference(definition_unfolding,[],[f51,f52]) ).
tcf(c_98,plain,
! [X0: $i] : or(X0,n0) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_99,plain,
! [X0: $i] : or(X0,n1) = n1,
inference(cnf_transformation,[],[f6]) ).
tcf(c_100,plain,
not(n0) = n1,
inference(cnf_transformation,[],[f8]) ).
tcf(c_101,plain,
not(n1) = n0,
inference(cnf_transformation,[],[f10]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] : and(X0,X1) = and(X1,X0),
inference(cnf_transformation,[],[f11]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i] : or(X0,X1) = or(X1,X0),
inference(cnf_transformation,[],[f12]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] : and(and(X0,X1),X2) = and(X0,and(X1,X2)),
inference(cnf_transformation,[],[f13]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : or(or(X0,X1),X2) = or(X0,or(X1,X2)),
inference(cnf_transformation,[],[f14]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] : or(not(X0),not(X1)) = not(and(X0,X1)),
inference(cnf_transformation,[],[f17]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i] : and(not(X0),not(X1)) = not(or(X0,X1)),
inference(cnf_transformation,[],[f18]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] : or(and(X0,X1),and(X2,X1)) = and(or(X0,X2),X1),
inference(cnf_transformation,[],[f19]) ).
tcf(c_111,plain,
! [X0: $i] : and(X0,X0) = X0,
inference(cnf_transformation,[],[f20]) ).
tcf(c_114,plain,
! [X0: $i] : or(X0,X0) = X0,
inference(cnf_transformation,[],[f25]) ).
tcf(c_117,plain,
! [X0: $i] : and(X0,not(X0)) = n0,
inference(cnf_transformation,[],[f31]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] : and(and(X0,X1),not(X0)) = n0,
inference(cnf_transformation,[],[f35]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : or(or(X0,X1),not(X0)) = n1,
inference(cnf_transformation,[],[f41]) ).
tcf(c_123,plain,
! [X0: $i] : not(not(X0)) = X0,
inference(cnf_transformation,[],[f42]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] : or(and(X0,X1),and(X0,not(X1))) = X0,
inference(cnf_transformation,[],[f43]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i] : or(and(X0,X1),and(X1,not(X0))) = X1,
inference(cnf_transformation,[],[f44]) ).
tcf(c_126,negated_conjecture,
and(b1,b3) = a1,
inference(cnf_transformation,[],[f45]) ).
tcf(c_127,negated_conjecture,
and(b2,b3) = a2,
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
not(d1) = b1,
inference(cnf_transformation,[],[f47]) ).
tcf(c_129,negated_conjecture,
not(d2) = b2,
inference(cnf_transformation,[],[f48]) ).
tcf(c_130,negated_conjecture,
or(c1,c2) = b3,
inference(cnf_transformation,[],[f49]) ).
tcf(c_131,negated_conjecture,
or(d1,f3) = c1,
inference(cnf_transformation,[],[f62]) ).
tcf(c_132,negated_conjecture,
or(d2,f3) = c2,
inference(cnf_transformation,[],[f63]) ).
tcf(c_133,negated_conjecture,
not(e1) = d1,
inference(cnf_transformation,[],[f53]) ).
tcf(c_134,negated_conjecture,
not(e2) = d2,
inference(cnf_transformation,[],[f54]) ).
tcf(c_135,negated_conjecture,
or(f1,f3) = e1,
inference(cnf_transformation,[],[f55]) ).
tcf(c_136,negated_conjecture,
or(f2,f3) = e2,
inference(cnf_transformation,[],[f56]) ).
tcf(c_137,negated_conjecture,
not(i1) = f1,
inference(cnf_transformation,[],[f57]) ).
tcf(c_138,negated_conjecture,
not(i2) = f2,
inference(cnf_transformation,[],[f58]) ).
tcf(c_139,negated_conjecture,
and(i1,i2) = f3,
inference(cnf_transformation,[],[f59]) ).
tcf(c_140,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
inference(cnf_transformation,[],[f60]) ).
tcf(c_141,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
inference(cnf_transformation,[],[f61]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i] : and(X0,and(X1,not(X0))) = n0,
inference(theory_normalisation,[status(thm)],[c_119,c_105,c_103,c_104,c_102]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i] : or(X0,or(X1,not(X0))) = n1,
inference(theory_normalisation,[status(thm)],[c_122,c_105,c_103,c_104,c_102]) ).
tcf(c_171,negated_conjecture,
and(b3,b1) = a1,
inference(theory_normalisation,[status(thm)],[c_126,c_105,c_103,c_104,c_102]) ).
tcf(c_172,negated_conjecture,
and(b3,b2) = a2,
inference(theory_normalisation,[status(thm)],[c_127,c_105,c_103,c_104,c_102]) ).
tcf(c_173,negated_conjecture,
or(f3,f1) = e1,
inference(theory_normalisation,[status(thm)],[c_135,c_105,c_103,c_104,c_102]) ).
tcf(c_174,negated_conjecture,
or(f3,f2) = e2,
inference(theory_normalisation,[status(thm)],[c_136,c_105,c_103,c_104,c_102]) ).
tcf(c_175,negated_conjecture,
or(f3,d1) = c1,
inference(theory_normalisation,[status(thm)],[c_131,c_105,c_103,c_104,c_102]) ).
tcf(c_176,negated_conjecture,
or(f3,d2) = c2,
inference(theory_normalisation,[status(thm)],[c_132,c_105,c_103,c_104,c_102]) ).
tcf(c_383,definition,
iPr_def_10 = or(f3,d2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_384,definition,
iPr_def_11 = or(f3,d1),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_385,definition,
iPr_def_12 = or(f3,f2),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_386,definition,
iPr_def_13 = or(f3,f1),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_387,definition,
iPr_def_14 = and(b3,b2),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_388,definition,
iPr_def_15 = and(b3,b1),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_389,definition,
iPr_def_16 = input(i1,i2),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_390,definition,
iPr_def_17 = output(i2,i1),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_391,definition,
iPr_def_18 = output(a1,a2),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_392,definition,
iPr_def_19 = and(i1,i2),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_393,definition,
iPr_def_20 = not(i2),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_394,definition,
iPr_def_21 = not(i1),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_395,definition,
iPr_def_22 = not(e2),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_396,definition,
iPr_def_23 = not(e1),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_397,definition,
iPr_def_24 = or(c1,c2),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_398,definition,
iPr_def_25 = not(d2),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_399,definition,
iPr_def_26 = not(d1),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_400,negated_conjecture,
iPr_def_10 = c2,
inference(demodulation,[status(thm)],[c_176,c_383]) ).
tcf(c_401,negated_conjecture,
iPr_def_11 = c1,
inference(demodulation,[status(thm)],[c_175,c_384]) ).
tcf(c_402,negated_conjecture,
iPr_def_12 = e2,
inference(demodulation,[status(thm)],[c_174,c_385]) ).
tcf(c_403,negated_conjecture,
iPr_def_13 = e1,
inference(demodulation,[status(thm)],[c_173,c_386]) ).
tcf(c_404,negated_conjecture,
iPr_def_14 = a2,
inference(demodulation,[status(thm)],[c_172,c_387]) ).
tcf(c_405,negated_conjecture,
iPr_def_15 = a1,
inference(demodulation,[status(thm)],[c_171,c_388]) ).
tcf(c_406,negated_conjecture,
~ circuit(iPr_def_16,iPr_def_17),
inference(demodulation,[status(thm)],[c_141,c_390,c_389]) ).
tcf(c_407,negated_conjecture,
circuit(iPr_def_16,iPr_def_18),
inference(demodulation,[status(thm)],[c_140,c_391]) ).
tcf(c_408,negated_conjecture,
iPr_def_19 = f3,
inference(demodulation,[status(thm)],[c_139,c_392]) ).
tcf(c_409,negated_conjecture,
iPr_def_20 = f2,
inference(demodulation,[status(thm)],[c_138,c_393]) ).
tcf(c_410,negated_conjecture,
iPr_def_21 = f1,
inference(demodulation,[status(thm)],[c_137,c_394]) ).
tcf(c_411,negated_conjecture,
iPr_def_22 = d2,
inference(demodulation,[status(thm)],[c_134,c_395]) ).
tcf(c_412,negated_conjecture,
iPr_def_23 = d1,
inference(demodulation,[status(thm)],[c_133,c_396]) ).
tcf(c_413,negated_conjecture,
iPr_def_24 = b3,
inference(demodulation,[status(thm)],[c_130,c_397]) ).
tcf(c_414,negated_conjecture,
iPr_def_25 = b2,
inference(demodulation,[status(thm)],[c_129,c_398]) ).
tcf(c_415,negated_conjecture,
iPr_def_26 = b1,
inference(demodulation,[status(thm)],[c_128,c_399]) ).
tcf(c_740,plain,
! [X0: $i,X1: $i,X2: $i] : and(X0,and(X1,X2)) = and(X1,and(X0,X2)),
inference(superposition,[status(thm)],[c_104,c_102]) ).
tcf(c_741,plain,
! [X0: $i,X1: $i,X2: $i] : or(X0,or(X1,X2)) = or(X1,or(X0,X2)),
inference(superposition,[status(thm)],[c_105,c_103]) ).
tcf(c_757,plain,
not(iPr_def_12) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_395,c_402]) ).
tcf(c_758,plain,
! [X0: $i] : and(iPr_def_12,and(X0,iPr_def_22)) = n0,
inference(superposition,[status(thm)],[c_757,c_168]) ).
tcf(c_760,plain,
not(iPr_def_13) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_396,c_403]) ).
tcf(c_777,plain,
not(iPr_def_22) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_398,c_411]) ).
tcf(c_782,plain,
not(iPr_def_23) = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_399,c_412]) ).
tcf(c_799,plain,
or(iPr_def_19,iPr_def_22) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_383,c_408,c_411]) ).
tcf(c_802,plain,
not(iPr_def_21) = i1,
inference(superposition,[status(thm)],[c_394,c_123]) ).
tcf(c_803,plain,
not(iPr_def_20) = i2,
inference(superposition,[status(thm)],[c_393,c_123]) ).
tcf(c_806,plain,
not(iPr_def_22) = iPr_def_12,
inference(superposition,[status(thm)],[c_757,c_123]) ).
tcf(c_807,plain,
not(iPr_def_23) = iPr_def_13,
inference(superposition,[status(thm)],[c_760,c_123]) ).
tcf(c_816,plain,
iPr_def_12 = iPr_def_25,
inference(demodulation,[status(thm)],[c_777,c_806]) ).
tcf(c_819,plain,
b2 = iPr_def_12,
inference(demodulation,[status(thm)],[c_414,c_816]) ).
tcf(c_822,plain,
iPr_def_13 = iPr_def_26,
inference(demodulation,[status(thm)],[c_782,c_807]) ).
tcf(c_825,plain,
b1 = iPr_def_13,
inference(demodulation,[status(thm)],[c_415,c_822]) ).
tcf(c_828,plain,
or(iPr_def_19,iPr_def_23) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_384,c_408,c_412]) ).
tcf(c_831,plain,
or(iPr_def_19,iPr_def_20) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_385,c_408,c_409]) ).
tcf(c_832,plain,
or(iPr_def_19,iPr_def_21) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_386,c_408,c_410]) ).
tcf(c_849,plain,
and(iPr_def_24,iPr_def_12) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_387,c_413,c_819]) ).
tcf(c_850,plain,
and(iPr_def_12,iPr_def_24) = iPr_def_14,
inference(demodulation,[status(thm)],[c_849,c_102]) ).
tcf(c_851,plain,
and(iPr_def_24,iPr_def_13) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_388,c_413,c_825]) ).
tcf(c_852,plain,
and(iPr_def_13,iPr_def_24) = iPr_def_15,
inference(demodulation,[status(thm)],[c_851,c_102]) ).
tcf(c_854,plain,
output(not(iPr_def_20),not(iPr_def_21)) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_390,c_802,c_803]) ).
tcf(c_855,plain,
output(iPr_def_15,iPr_def_14) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_391,c_404,c_405]) ).
tcf(c_856,plain,
and(not(iPr_def_21),not(iPr_def_20)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_392,c_802,c_803]) ).
tcf(c_857,plain,
and(not(iPr_def_20),not(iPr_def_21)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_856,c_102]) ).
tcf(c_858,plain,
and(iPr_def_21,iPr_def_19) = n0,
inference(superposition,[status(thm)],[c_857,c_168]) ).
tcf(c_859,plain,
and(iPr_def_19,iPr_def_21) = n0,
inference(theory_normalisation,[status(thm)],[c_858,c_104,c_102,c_105,c_103]) ).
tcf(c_860,plain,
or(iPr_def_11,iPr_def_10) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_397,c_400,c_401]) ).
tcf(c_861,plain,
or(iPr_def_10,iPr_def_11) = iPr_def_24,
inference(demodulation,[status(thm)],[c_860,c_103]) ).
tcf(c_911,plain,
! [X0: $i] : and(iPr_def_12,and(X0,iPr_def_24)) = and(X0,iPr_def_14),
inference(superposition,[status(thm)],[c_850,c_740]) ).
tcf(c_912,plain,
! [X0: $i] : and(iPr_def_13,and(X0,iPr_def_24)) = and(X0,iPr_def_15),
inference(superposition,[status(thm)],[c_852,c_740]) ).
tcf(c_913,plain,
! [X0: $i] : and(not(iPr_def_20),and(X0,not(iPr_def_21))) = and(X0,iPr_def_19),
inference(superposition,[status(thm)],[c_857,c_740]) ).
tcf(c_974,plain,
! [X0: $i] : and(iPr_def_12,and(iPr_def_22,X0)) = n0,
inference(superposition,[status(thm)],[c_102,c_758]) ).
tcf(c_990,plain,
! [X0: $i] : or(n1,X0) = n1,
inference(superposition,[status(thm)],[c_103,c_99]) ).
tcf(c_1014,plain,
or(not(not(iPr_def_20)),not(not(iPr_def_21))) = not(iPr_def_19),
inference(superposition,[status(thm)],[c_857,c_108]) ).
tcf(c_1184,plain,
! [X0: $i] : or(iPr_def_19,or(X0,iPr_def_22)) = or(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_799,c_741]) ).
tcf(c_1186,plain,
! [X0: $i] : or(iPr_def_19,or(X0,iPr_def_23)) = or(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_828,c_741]) ).
tcf(c_1188,plain,
! [X0: $i] : or(iPr_def_19,or(X0,iPr_def_20)) = or(X0,iPr_def_12),
inference(superposition,[status(thm)],[c_831,c_741]) ).
tcf(c_1189,plain,
! [X0: $i] : or(iPr_def_19,or(X0,iPr_def_21)) = or(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_832,c_741]) ).
tcf(c_1255,plain,
and(not(iPr_def_19),not(iPr_def_22)) = not(iPr_def_10),
inference(superposition,[status(thm)],[c_799,c_109]) ).
tcf(c_1260,plain,
and(not(iPr_def_19),not(iPr_def_21)) = not(iPr_def_13),
inference(superposition,[status(thm)],[c_832,c_109]) ).
tcf(c_1261,plain,
and(not(iPr_def_10),not(iPr_def_11)) = not(iPr_def_24),
inference(superposition,[status(thm)],[c_861,c_109]) ).
tcf(c_1271,plain,
and(not(iPr_def_19),not(iPr_def_21)) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_1260,c_760]) ).
tcf(c_1279,plain,
and(not(iPr_def_19),iPr_def_12) = not(iPr_def_10),
inference(light_normalisation,[status(thm)],[c_1255,c_806]) ).
tcf(c_1280,plain,
and(iPr_def_12,not(iPr_def_19)) = not(iPr_def_10),
inference(theory_normalisation,[status(thm)],[c_1279,c_104,c_102,c_105,c_103]) ).
tcf(c_1376,plain,
! [X0: $i,X1: $i] : or(n0,and(X0,not(and(X1,not(X0))))) = X0,
inference(superposition,[status(thm)],[c_168,c_124]) ).
tcf(c_1481,plain,
! [X0: $i] : or(n0,and(and(X0,iPr_def_22),not(iPr_def_12))) = and(X0,iPr_def_22),
inference(superposition,[status(thm)],[c_758,c_125]) ).
tcf(c_1488,plain,
or(n0,and(iPr_def_21,not(iPr_def_19))) = iPr_def_21,
inference(superposition,[status(thm)],[c_859,c_125]) ).
tcf(c_1531,plain,
! [X0: $i] : or(n0,and(X0,and(iPr_def_22,not(iPr_def_12)))) = and(X0,iPr_def_22),
inference(theory_normalisation,[status(thm)],[c_1481,c_104,c_102,c_105,c_103]) ).
tcf(c_1532,plain,
! [X0: $i] : or(n0,and(X0,and(iPr_def_22,iPr_def_22))) = and(X0,iPr_def_22),
inference(light_normalisation,[status(thm)],[c_1531,c_757]) ).
tcf(c_1595,plain,
! [X0: $i,X1: $i] : and(X0,and(X0,X1)) = and(X0,X1),
inference(superposition,[status(thm)],[c_111,c_104]) ).
tcf(c_1606,plain,
! [X0: $i] : and(iPr_def_12,and(iPr_def_24,X0)) = and(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_850,c_104]) ).
tcf(c_1726,plain,
or(and(iPr_def_21,not(iPr_def_19)),iPr_def_23) = not(iPr_def_19),
inference(superposition,[status(thm)],[c_1271,c_125]) ).
tcf(c_1728,plain,
or(iPr_def_23,and(iPr_def_21,not(iPr_def_19))) = not(iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_1726,c_104,c_102,c_105,c_103]) ).
tcf(c_1787,plain,
or(iPr_def_19,iPr_def_22) = or(iPr_def_22,iPr_def_10),
inference(superposition,[status(thm)],[c_114,c_1184]) ).
tcf(c_1801,plain,
or(iPr_def_10,iPr_def_22) = or(iPr_def_19,iPr_def_22),
inference(theory_normalisation,[status(thm)],[c_1787,c_104,c_102,c_105,c_103]) ).
tcf(c_1802,plain,
or(iPr_def_10,iPr_def_22) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_1801,c_799]) ).
tcf(c_1810,plain,
! [X0: $i] : or(iPr_def_10,or(X0,iPr_def_22)) = or(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_1802,c_741]) ).
tcf(c_1851,plain,
! [X0: $i,X1: $i] : or(X0,or(X0,X1)) = or(X0,X1),
inference(superposition,[status(thm)],[c_114,c_105]) ).
tcf(c_1864,plain,
! [X0: $i] : or(iPr_def_19,or(iPr_def_22,X0)) = or(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_799,c_105]) ).
tcf(c_1868,plain,
! [X0: $i] : or(iPr_def_19,or(iPr_def_20,X0)) = or(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_831,c_105]) ).
tcf(c_1869,plain,
! [X0: $i] : or(iPr_def_19,or(iPr_def_21,X0)) = or(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_832,c_105]) ).
tcf(c_1978,plain,
! [X0: $i,X1: $i] : and(or(iPr_def_12,X0),and(iPr_def_22,X1)) = or(n0,and(X0,and(iPr_def_22,X1))),
inference(superposition,[status(thm)],[c_974,c_110]) ).
tcf(c_1988,plain,
! [X0: $i,X1: $i] : and(or(X0,X1),not(X1)) = or(and(X0,not(X1)),n0),
inference(superposition,[status(thm)],[c_117,c_110]) ).
tcf(c_2045,plain,
! [X0: $i,X1: $i] : and(or(X0,X1),not(X1)) = or(n0,and(X0,not(X1))),
inference(theory_normalisation,[status(thm)],[c_1988,c_104,c_102,c_105,c_103]) ).
tcf(c_2052,plain,
! [X0: $i,X1: $i] : and(iPr_def_22,and(X0,or(iPr_def_12,X1))) = or(n0,and(X1,and(iPr_def_22,X0))),
inference(theory_normalisation,[status(thm)],[c_1978,c_104,c_102,c_105,c_103]) ).
tcf(c_2444,plain,
or(iPr_def_19,iPr_def_23) = or(iPr_def_23,iPr_def_11),
inference(superposition,[status(thm)],[c_114,c_1186]) ).
tcf(c_2460,plain,
or(iPr_def_11,iPr_def_23) = or(iPr_def_19,iPr_def_23),
inference(theory_normalisation,[status(thm)],[c_2444,c_104,c_102,c_105,c_103]) ).
tcf(c_2461,plain,
or(iPr_def_11,iPr_def_23) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_2460,c_828]) ).
tcf(c_2473,plain,
or(iPr_def_11,iPr_def_11) = or(iPr_def_19,iPr_def_11),
inference(superposition,[status(thm)],[c_2461,c_1186]) ).
tcf(c_2475,plain,
or(iPr_def_11,iPr_def_11) = or(iPr_def_11,iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_2473,c_104,c_102,c_105,c_103]) ).
tcf(c_2494,plain,
or(iPr_def_19,iPr_def_20) = or(iPr_def_20,iPr_def_12),
inference(superposition,[status(thm)],[c_114,c_1188]) ).
tcf(c_2507,plain,
or(iPr_def_12,iPr_def_20) = or(iPr_def_19,iPr_def_20),
inference(theory_normalisation,[status(thm)],[c_2494,c_104,c_102,c_105,c_103]) ).
tcf(c_2508,plain,
or(iPr_def_12,iPr_def_20) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_2507,c_831]) ).
tcf(c_2532,plain,
or(iPr_def_12,iPr_def_12) = or(iPr_def_19,iPr_def_12),
inference(superposition,[status(thm)],[c_2508,c_1188]) ).
tcf(c_2533,plain,
or(iPr_def_12,iPr_def_12) = or(iPr_def_12,iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_2532,c_104,c_102,c_105,c_103]) ).
tcf(c_2583,plain,
or(iPr_def_19,iPr_def_21) = or(iPr_def_21,iPr_def_13),
inference(superposition,[status(thm)],[c_114,c_1189]) ).
tcf(c_2596,plain,
or(iPr_def_13,iPr_def_21) = or(iPr_def_19,iPr_def_21),
inference(theory_normalisation,[status(thm)],[c_2583,c_104,c_102,c_105,c_103]) ).
tcf(c_2597,plain,
or(iPr_def_13,iPr_def_21) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_2596,c_832]) ).
tcf(c_2646,plain,
and(not(iPr_def_13),not(iPr_def_21)) = not(iPr_def_13),
inference(superposition,[status(thm)],[c_2597,c_109]) ).
tcf(c_2651,plain,
and(iPr_def_23,not(iPr_def_21)) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_2646,c_760]) ).
tcf(c_2865,plain,
or(iPr_def_10,iPr_def_23) = or(iPr_def_22,iPr_def_11),
inference(superposition,[status(thm)],[c_1864,c_1186]) ).
tcf(c_2871,plain,
or(iPr_def_10,iPr_def_23) = or(iPr_def_11,iPr_def_22),
inference(theory_normalisation,[status(thm)],[c_2865,c_104,c_102,c_105,c_103]) ).
tcf(c_2987,plain,
or(iPr_def_12,not(iPr_def_19)) = n1,
inference(superposition,[status(thm)],[c_1868,c_170]) ).
tcf(c_2991,plain,
or(iPr_def_12,iPr_def_21) = or(iPr_def_20,iPr_def_13),
inference(superposition,[status(thm)],[c_1868,c_1189]) ).
tcf(c_2992,plain,
or(iPr_def_12,iPr_def_21) = or(iPr_def_13,iPr_def_20),
inference(theory_normalisation,[status(thm)],[c_2991,c_104,c_102,c_105,c_103]) ).
tcf(c_3213,plain,
or(iPr_def_13,not(iPr_def_19)) = n1,
inference(superposition,[status(thm)],[c_1869,c_170]) ).
tcf(c_3309,plain,
! [X0: $i] : and(iPr_def_22,or(iPr_def_12,X0)) = and(X0,iPr_def_22),
inference(demodulation,[status(thm)],[c_1532,c_1595,c_2052]) ).
tcf(c_3324,plain,
and(not(iPr_def_19),iPr_def_22) = and(iPr_def_22,n1),
inference(superposition,[status(thm)],[c_2987,c_3309]) ).
tcf(c_3337,plain,
and(iPr_def_22,not(iPr_def_19)) = and(iPr_def_22,n1),
inference(theory_normalisation,[status(thm)],[c_3324,c_104,c_102,c_105,c_103]) ).
tcf(c_3382,plain,
and(not(iPr_def_13),not(not(iPr_def_19))) = not(n1),
inference(superposition,[status(thm)],[c_3213,c_109]) ).
tcf(c_3389,plain,
and(iPr_def_23,not(not(iPr_def_19))) = n0,
inference(light_normalisation,[status(thm)],[c_3382,c_101,c_760]) ).
tcf(c_3406,plain,
and(iPr_def_19,iPr_def_23) = n0,
inference(demodulation,[status(thm)],[c_3389,c_102,c_123]) ).
tcf(c_3654,plain,
and(iPr_def_12,iPr_def_24) = and(iPr_def_24,iPr_def_14),
inference(superposition,[status(thm)],[c_111,c_911]) ).
tcf(c_3657,plain,
and(iPr_def_12,iPr_def_15) = and(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_852,c_911]) ).
tcf(c_3673,plain,
and(iPr_def_12,iPr_def_24) = and(iPr_def_14,iPr_def_24),
inference(theory_normalisation,[status(thm)],[c_3654,c_104,c_102,c_105,c_103]) ).
tcf(c_3674,plain,
and(iPr_def_14,iPr_def_24) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_3673,c_850]) ).
tcf(c_3911,plain,
and(iPr_def_13,iPr_def_24) = and(iPr_def_24,iPr_def_15),
inference(superposition,[status(thm)],[c_111,c_912]) ).
tcf(c_3915,plain,
and(iPr_def_13,iPr_def_14) = and(iPr_def_14,iPr_def_15),
inference(superposition,[status(thm)],[c_3674,c_912]) ).
tcf(c_3928,plain,
and(iPr_def_12,iPr_def_15) = and(iPr_def_14,iPr_def_15),
inference(light_normalisation,[status(thm)],[c_3915,c_3657]) ).
tcf(c_3932,plain,
and(iPr_def_13,iPr_def_24) = and(iPr_def_15,iPr_def_24),
inference(theory_normalisation,[status(thm)],[c_3911,c_104,c_102,c_105,c_103]) ).
tcf(c_3933,plain,
and(iPr_def_15,iPr_def_24) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_3932,c_852]) ).
tcf(c_3984,plain,
! [X0: $i] : and(iPr_def_15,and(X0,iPr_def_24)) = and(X0,iPr_def_15),
inference(superposition,[status(thm)],[c_3933,c_740]) ).
tcf(c_4010,plain,
and(not(iPr_def_20),iPr_def_23) = and(iPr_def_23,iPr_def_19),
inference(superposition,[status(thm)],[c_2651,c_913]) ).
tcf(c_4020,plain,
and(iPr_def_23,not(iPr_def_20)) = and(iPr_def_19,iPr_def_23),
inference(theory_normalisation,[status(thm)],[c_4010,c_104,c_102,c_105,c_103]) ).
tcf(c_4021,plain,
and(iPr_def_23,not(iPr_def_20)) = n0,
inference(light_normalisation,[status(thm)],[c_4020,c_3406]) ).
tcf(c_4223,plain,
or(not(iPr_def_23),not(not(iPr_def_20))) = not(n0),
inference(superposition,[status(thm)],[c_4021,c_108]) ).
tcf(c_4231,plain,
or(iPr_def_13,not(not(iPr_def_20))) = n1,
inference(light_normalisation,[status(thm)],[c_4223,c_100,c_807]) ).
tcf(c_4272,plain,
or(iPr_def_12,iPr_def_21) = n1,
inference(demodulation,[status(thm)],[c_4231,c_123,c_2992]) ).
tcf(c_4273,plain,
! [X0: $i] : or(iPr_def_12,or(iPr_def_21,X0)) = or(n1,X0),
inference(superposition,[status(thm)],[c_4272,c_105]) ).
tcf(c_4274,plain,
and(not(iPr_def_12),not(iPr_def_21)) = not(n1),
inference(superposition,[status(thm)],[c_4272,c_109]) ).
tcf(c_4277,plain,
or(iPr_def_12,iPr_def_13) = or(iPr_def_19,n1),
inference(superposition,[status(thm)],[c_4272,c_1189]) ).
tcf(c_4280,plain,
and(iPr_def_22,not(iPr_def_21)) = n0,
inference(light_normalisation,[status(thm)],[c_4274,c_101,c_757]) ).
tcf(c_4282,plain,
! [X0: $i] : or(iPr_def_12,or(iPr_def_21,X0)) = n1,
inference(light_normalisation,[status(thm)],[c_4273,c_990]) ).
tcf(c_4287,plain,
or(n0,and(iPr_def_22,not(not(iPr_def_21)))) = iPr_def_22,
inference(superposition,[status(thm)],[c_4280,c_124]) ).
tcf(c_4342,plain,
or(iPr_def_12,iPr_def_13) = n1,
inference(demodulation,[status(thm)],[c_4277,c_99]) ).
tcf(c_4349,plain,
and(iPr_def_13,iPr_def_22) = and(iPr_def_22,n1),
inference(superposition,[status(thm)],[c_4342,c_3309]) ).
tcf(c_4716,plain,
or(iPr_def_11,iPr_def_19) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2475,c_114]) ).
tcf(c_4718,plain,
and(not(iPr_def_11),not(iPr_def_19)) = not(iPr_def_11),
inference(superposition,[status(thm)],[c_4716,c_109]) ).
tcf(c_4934,plain,
or(iPr_def_12,iPr_def_19) = iPr_def_12,
inference(demodulation,[status(thm)],[c_2533,c_114]) ).
tcf(c_4936,plain,
and(not(iPr_def_12),not(iPr_def_19)) = not(iPr_def_12),
inference(superposition,[status(thm)],[c_4934,c_109]) ).
tcf(c_4943,plain,
and(iPr_def_13,iPr_def_22) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_4936,c_757,c_3337,c_4349]) ).
tcf(c_4947,plain,
! [X0: $i] : and(iPr_def_13,and(iPr_def_22,X0)) = and(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_4943,c_104]) ).
tcf(c_6413,plain,
or(iPr_def_10,or(iPr_def_10,iPr_def_23)) = or(iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_2871,c_1810]) ).
tcf(c_6420,plain,
or(iPr_def_10,or(iPr_def_10,iPr_def_23)) = or(iPr_def_10,iPr_def_11),
inference(theory_normalisation,[status(thm)],[c_6413,c_104,c_102,c_105,c_103]) ).
tcf(c_6421,plain,
or(iPr_def_10,or(iPr_def_10,iPr_def_23)) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_6420,c_861]) ).
tcf(c_6523,plain,
or(iPr_def_10,iPr_def_23) = iPr_def_24,
inference(demodulation,[status(thm)],[c_6421,c_1851]) ).
tcf(c_6524,plain,
or(iPr_def_11,iPr_def_22) = iPr_def_24,
inference(demodulation,[status(thm)],[c_2871,c_6523]) ).
tcf(c_6526,plain,
and(not(iPr_def_10),not(iPr_def_23)) = not(iPr_def_24),
inference(superposition,[status(thm)],[c_6523,c_109]) ).
tcf(c_6532,plain,
and(not(iPr_def_10),not(iPr_def_11)) = and(not(iPr_def_10),iPr_def_13),
inference(light_normalisation,[status(thm)],[c_6526,c_807,c_1261]) ).
tcf(c_6533,plain,
and(not(iPr_def_10),not(iPr_def_11)) = and(iPr_def_13,not(iPr_def_10)),
inference(theory_normalisation,[status(thm)],[c_6532,c_104,c_102,c_105,c_103]) ).
tcf(c_6535,plain,
and(iPr_def_13,not(iPr_def_10)) = not(iPr_def_24),
inference(demodulation,[status(thm)],[c_1261,c_6533]) ).
tcf(c_7216,plain,
! [X0: $i] : and(or(iPr_def_21,X0),iPr_def_22) = and(iPr_def_22,n1),
inference(superposition,[status(thm)],[c_4282,c_3309]) ).
tcf(c_7217,plain,
! [X0: $i] : and(iPr_def_22,or(iPr_def_21,X0)) = and(iPr_def_22,n1),
inference(theory_normalisation,[status(thm)],[c_7216,c_104,c_102,c_105,c_103]) ).
tcf(c_7218,plain,
! [X0: $i] : and(iPr_def_22,or(iPr_def_21,X0)) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_7217,c_4349,c_4943]) ).
tcf(c_7488,plain,
and(iPr_def_22,iPr_def_21) = iPr_def_22,
inference(superposition,[status(thm)],[c_98,c_7218]) ).
tcf(c_7505,plain,
and(iPr_def_21,iPr_def_22) = iPr_def_22,
inference(theory_normalisation,[status(thm)],[c_7488,c_104,c_102,c_105,c_103]) ).
tcf(c_7691,plain,
or(iPr_def_22,and(iPr_def_21,not(iPr_def_22))) = iPr_def_21,
inference(superposition,[status(thm)],[c_7505,c_124]) ).
tcf(c_7703,plain,
or(iPr_def_22,and(iPr_def_21,iPr_def_12)) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_7691,c_806]) ).
tcf(c_7704,plain,
or(iPr_def_22,and(iPr_def_12,iPr_def_21)) = iPr_def_21,
inference(theory_normalisation,[status(thm)],[c_7703,c_104,c_102,c_105,c_103]) ).
tcf(c_8266,plain,
or(iPr_def_20,iPr_def_21) = not(iPr_def_19),
inference(demodulation,[status(thm)],[c_1014,c_123]) ).
tcf(c_8270,plain,
and(iPr_def_12,or(iPr_def_20,iPr_def_21)) = not(iPr_def_10),
inference(demodulation,[status(thm)],[c_1280,c_8266]) ).
tcf(c_8315,plain,
and(iPr_def_19,or(iPr_def_20,iPr_def_21)) = n0,
inference(superposition,[status(thm)],[c_8266,c_117]) ).
tcf(c_9560,plain,
and(iPr_def_13,and(iPr_def_12,or(iPr_def_20,iPr_def_21))) = not(iPr_def_24),
inference(light_normalisation,[status(thm)],[c_6535,c_8270]) ).
tcf(c_9561,plain,
and(iPr_def_12,and(iPr_def_13,or(iPr_def_20,iPr_def_21))) = not(iPr_def_24),
inference(demodulation,[status(thm)],[c_9560,c_740]) ).
tcf(c_11266,plain,
and(not(iPr_def_22),not(and(iPr_def_12,iPr_def_21))) = not(iPr_def_21),
inference(superposition,[status(thm)],[c_7704,c_109]) ).
tcf(c_11273,plain,
and(iPr_def_12,not(and(iPr_def_12,iPr_def_21))) = not(iPr_def_21),
inference(light_normalisation,[status(thm)],[c_11266,c_806]) ).
tcf(c_11511,plain,
and(iPr_def_21,or(iPr_def_22,not(iPr_def_21))) = iPr_def_22,
inference(demodulation,[status(thm)],[c_4287,c_102,c_123,c_2045]) ).
tcf(c_12047,plain,
! [X0: $i] : and(or(iPr_def_19,X0),or(iPr_def_20,iPr_def_21)) = or(n0,and(X0,or(iPr_def_20,iPr_def_21))),
inference(superposition,[status(thm)],[c_8315,c_110]) ).
tcf(c_12239,plain,
and(iPr_def_22,iPr_def_15) = and(iPr_def_22,iPr_def_24),
inference(superposition,[status(thm)],[c_4947,c_912]) ).
tcf(c_12243,plain,
and(iPr_def_15,iPr_def_22) = and(iPr_def_22,iPr_def_24),
inference(theory_normalisation,[status(thm)],[c_12239,c_104,c_102,c_105,c_103]) ).
tcf(c_12809,plain,
or(n0,and(iPr_def_21,or(iPr_def_20,iPr_def_21))) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_1488,c_8266]) ).
tcf(c_12810,plain,
and(iPr_def_13,or(iPr_def_20,iPr_def_21)) = iPr_def_21,
inference(demodulation,[status(thm)],[c_12809,c_832,c_12047]) ).
tcf(c_12816,plain,
and(iPr_def_12,iPr_def_21) = not(iPr_def_24),
inference(demodulation,[status(thm)],[c_9561,c_12810]) ).
tcf(c_12827,plain,
or(not(iPr_def_13),not(or(iPr_def_20,iPr_def_21))) = not(iPr_def_21),
inference(superposition,[status(thm)],[c_12810,c_108]) ).
tcf(c_12831,plain,
or(iPr_def_23,not(or(iPr_def_20,iPr_def_21))) = not(iPr_def_21),
inference(light_normalisation,[status(thm)],[c_12827,c_760]) ).
tcf(c_12852,plain,
not(and(iPr_def_12,iPr_def_21)) = iPr_def_24,
inference(superposition,[status(thm)],[c_12816,c_123]) ).
tcf(c_12938,plain,
or(iPr_def_22,not(iPr_def_21)) = iPr_def_24,
inference(demodulation,[status(thm)],[c_12852,c_108,c_757]) ).
tcf(c_12939,plain,
and(iPr_def_21,iPr_def_24) = iPr_def_22,
inference(demodulation,[status(thm)],[c_11511,c_12938]) ).
tcf(c_12976,plain,
and(iPr_def_13,iPr_def_22) = and(iPr_def_21,iPr_def_15),
inference(superposition,[status(thm)],[c_12939,c_912]) ).
tcf(c_12981,plain,
and(iPr_def_13,iPr_def_22) = and(iPr_def_15,iPr_def_21),
inference(theory_normalisation,[status(thm)],[c_12976,c_104,c_102,c_105,c_103]) ).
tcf(c_12982,plain,
and(iPr_def_15,iPr_def_21) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_12981,c_4943]) ).
tcf(c_13074,plain,
! [X0: $i] : and(iPr_def_15,and(iPr_def_21,X0)) = and(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_12982,c_104]) ).
tcf(c_13150,plain,
not(iPr_def_21) = iPr_def_11,
inference(demodulation,[status(thm)],[c_12831,c_103,c_109,c_828,c_857]) ).
tcf(c_13161,plain,
and(not(iPr_def_20),iPr_def_11) = iPr_def_19,
inference(demodulation,[status(thm)],[c_857,c_13150]) ).
tcf(c_13163,plain,
output(not(iPr_def_20),iPr_def_11) = iPr_def_17,
inference(demodulation,[status(thm)],[c_854,c_13150]) ).
tcf(c_13170,plain,
and(iPr_def_11,not(iPr_def_20)) = iPr_def_19,
inference(theory_normalisation,[status(thm)],[c_13161,c_104,c_102,c_105,c_103]) ).
tcf(c_13187,plain,
not(iPr_def_11) = iPr_def_21,
inference(superposition,[status(thm)],[c_13150,c_123]) ).
tcf(c_14771,plain,
and(iPr_def_15,iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_12243,c_102,c_3984,c_12982,c_13074]) ).
tcf(c_14776,plain,
or(iPr_def_22,and(iPr_def_15,not(iPr_def_22))) = iPr_def_15,
inference(superposition,[status(thm)],[c_14771,c_124]) ).
tcf(c_14791,plain,
or(iPr_def_22,and(iPr_def_15,iPr_def_12)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_14776,c_806]) ).
tcf(c_14792,plain,
or(iPr_def_22,and(iPr_def_12,iPr_def_15)) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_14791,c_104,c_102,c_105,c_103]) ).
tcf(c_15364,plain,
and(iPr_def_12,not(and(iPr_def_12,iPr_def_21))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_11273,c_13150]) ).
tcf(c_15365,plain,
iPr_def_11 = iPr_def_14,
inference(demodulation,[status(thm)],[c_15364,c_103,c_108,c_757,c_850,c_6524,c_13150]) ).
tcf(c_15374,plain,
and(iPr_def_11,iPr_def_15) = and(iPr_def_12,iPr_def_15),
inference(demodulation,[status(thm)],[c_3928,c_15365]) ).
tcf(c_15377,plain,
! [X0: $i] : and(iPr_def_12,and(iPr_def_24,X0)) = and(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_1606,c_15365]) ).
tcf(c_15380,plain,
and(iPr_def_11,iPr_def_24) = iPr_def_11,
inference(demodulation,[status(thm)],[c_3674,c_15365]) ).
tcf(c_15381,plain,
! [X0: $i] : and(iPr_def_12,and(X0,iPr_def_24)) = and(X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_911,c_15365]) ).
tcf(c_15382,plain,
output(iPr_def_15,iPr_def_11) = iPr_def_18,
inference(demodulation,[status(thm)],[c_855,c_15365]) ).
tcf(c_15386,plain,
or(iPr_def_22,and(iPr_def_11,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_14792,c_15374]) ).
tcf(c_15398,plain,
and(iPr_def_11,iPr_def_15) = and(iPr_def_13,iPr_def_11),
inference(superposition,[status(thm)],[c_15380,c_912]) ).
tcf(c_15399,plain,
and(iPr_def_11,iPr_def_13) = and(iPr_def_11,iPr_def_15),
inference(theory_normalisation,[status(thm)],[c_15398,c_104,c_102,c_105,c_103]) ).
tcf(c_15568,plain,
or(iPr_def_22,and(iPr_def_11,iPr_def_13)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_15386,c_15399]) ).
tcf(c_15945,plain,
! [X0: $i] : and(iPr_def_12,and(iPr_def_24,X0)) = and(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_102,c_15381]) ).
tcf(c_16480,plain,
and(iPr_def_21,or(iPr_def_20,iPr_def_21)) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_4718,c_8266,c_13187]) ).
tcf(c_21592,plain,
or(iPr_def_20,iPr_def_21) = or(iPr_def_23,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_1728,c_8266,c_16480]) ).
tcf(c_21593,plain,
or(iPr_def_20,iPr_def_21) = or(iPr_def_21,iPr_def_23),
inference(demodulation,[status(thm)],[c_21592,c_103]) ).
tcf(c_21598,plain,
and(not(iPr_def_21),not(iPr_def_23)) = not(or(iPr_def_20,iPr_def_21)),
inference(superposition,[status(thm)],[c_21593,c_109]) ).
tcf(c_21618,plain,
not(or(iPr_def_20,iPr_def_21)) = and(iPr_def_11,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_21598,c_807,c_13150]) ).
tcf(c_21629,plain,
and(iPr_def_11,iPr_def_13) = iPr_def_19,
inference(demodulation,[status(thm)],[c_21618,c_109,c_13150,c_13170,c_15377,c_15945]) ).
tcf(c_21632,plain,
or(iPr_def_22,iPr_def_19) = iPr_def_15,
inference(demodulation,[status(thm)],[c_15568,c_21629]) ).
tcf(c_21636,plain,
or(iPr_def_19,iPr_def_22) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_21632,c_104,c_102,c_105,c_103]) ).
tcf(c_21637,plain,
iPr_def_10 = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_21636,c_799]) ).
tcf(c_21644,plain,
output(iPr_def_10,iPr_def_11) = iPr_def_18,
inference(demodulation,[status(thm)],[c_15382,c_21637]) ).
tcf(c_23673,plain,
! [X0: $i,X1: $i] : and(or(X0,and(X1,not(X0))),or(not(X1),X0)) = X0,
inference(demodulation,[status(thm)],[c_1376,c_108,c_123,c_2045]) ).
tcf(c_23697,plain,
and(or(iPr_def_20,iPr_def_19),or(not(iPr_def_11),iPr_def_20)) = iPr_def_20,
inference(superposition,[status(thm)],[c_13170,c_23673]) ).
tcf(c_23783,plain,
and(or(iPr_def_19,iPr_def_20),or(iPr_def_20,not(iPr_def_11))) = iPr_def_20,
inference(theory_normalisation,[status(thm)],[c_23697,c_104,c_102,c_105,c_103]) ).
tcf(c_23784,plain,
and(iPr_def_12,or(iPr_def_20,iPr_def_21)) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_23783,c_831,c_13187]) ).
tcf(c_23859,plain,
not(iPr_def_10) = iPr_def_20,
inference(demodulation,[status(thm)],[c_8270,c_23784]) ).
tcf(c_26154,plain,
not(iPr_def_20) = iPr_def_10,
inference(superposition,[status(thm)],[c_23859,c_123]) ).
tcf(c_26231,plain,
output(iPr_def_10,iPr_def_11) = iPr_def_17,
inference(demodulation,[status(thm)],[c_13163,c_26154]) ).
tcf(c_26242,plain,
iPr_def_17 = iPr_def_18,
inference(demodulation,[status(thm)],[c_21644,c_26231]) ).
tcf(c_26243,plain,
circuit(iPr_def_16,iPr_def_17),
inference(demodulation,[status(thm)],[c_407,c_26242]) ).
tcf(c_26244,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_26243,c_406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.37 % Computer : n007.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Wed Sep 23 16:17:22 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.41 Running first-order theorem proving
% 0.08/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.42
% 0.08/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.42
% 0.08/0.42 % Detected problem language: tptp
% 0.08/0.43 % Proving...
% 6.06/2.21 % SZS status Started for theBenchmark.p
% 6.06/2.21 % SZS status Unsatisfiable for theBenchmark.p
% 6.06/2.21
% 6.06/2.21 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.06/2.21
% 6.06/2.21 % ------ iProver source info
% 6.06/2.21
% 6.06/2.21 % git: date: 2026-07-19 20:42:38 +0200
% 6.06/2.21 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.06/2.21 % git: non_committed_changes: false
% 6.06/2.21
% 6.06/2.21 % ------ Parsing...% successful
% 6.06/2.21
% 6.06/2.21
% 6.06/2.21 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.06/2.21
% 6.06/2.21 % ------ Preprocessing... sup_sim: 6 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 6.06/2.21
% 6.06/2.21 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.06/2.21
% 6.06/2.21 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 6.06/2.21 % ------ Proving...
% 6.06/2.21 % ------ Problem Properties
% 6.06/2.21
% 6.06/2.21 %
% 6.06/2.21 % clauses 55
% 6.06/2.21 % conjectures 16
% 6.06/2.21 % EPR 16
% 6.06/2.21 % Horn 55
% 6.06/2.21 % unary 55
% 6.06/2.21 % binary 0
% 6.06/2.21 % lits 55
% 6.06/2.21 % lits eq 53
% 6.06/2.21 % fd_pure 0
% 6.06/2.21 % fd_pseudo 0
% 6.06/2.21 % fd_cond 0
% 6.06/2.21 % fd_pseudo_cond 0
% 6.06/2.21 % AC symbols 2
% 6.06/2.21
% 6.06/2.21 % ------ Schedule dynamic 5 is on
% 6.06/2.21
% 6.06/2.21 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.06/2.21
% 6.06/2.21
% 6.06/2.21 % ------
% 6.06/2.21 % Current options:
% 6.06/2.21 % ------
% 6.06/2.21
% 6.06/2.21
% 6.06/2.21 %
% 6.06/2.21
% 6.06/2.21 % ------ Proving...
% 6.06/2.21 %
% 6.06/2.21
% 6.06/2.21 % SZS status Unsatisfiable for theBenchmark.p
% 6.06/2.21
% 6.06/2.21 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.06/2.22
% 6.06/2.22
%------------------------------------------------------------------------------