%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL006+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n002.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 02:36:32 PM UTC 2026
% Result : Theorem 18.60s 3.26s
% Output : CNFRefutation 18.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 19
% Syntax : Number of formulae : 264 ( 260 unt; 10 def)
% Number of atoms : 852 ( 267 equ)
% Maximal formula atoms : 2 ( 3 avg)
% Number of connectives : 12 ( 8 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 11 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 197 ( 0 sgn 195 !; 2 ?; 162 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux2_join_associativity) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
fof(f4,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
fof(f8,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
fof(f9,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
fof(f12,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_top) ).
fof(f13,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_zero) ).
fof(f14,conjecture,
! [X0,X1] :
( meet(converse(X0),X1) = zero
=> meet(X0,converse(X1)) = zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f15,negated_conjecture,
~ ! [X0,X1] :
( meet(converse(X0),X1) = zero
=> meet(X0,converse(X1)) = zero ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
? [X0,X1] :
( meet(converse(X0),X1) = zero
& zero != meet(X0,converse(X1)) ),
inference(ennf_transformation,[],[f15]) ).
fof(f17,plain,
( zero = meet(converse(sK0),sK1)
& zero != meet(sK0,converse(sK1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f16]) ).
fof(f18,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f19,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f21,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(cnf_transformation,[],[f4]) ).
fof(f25,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[],[f9]) ).
fof(f29,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f30,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f31,plain,
zero = meet(converse(sK0),sK1),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
zero != meet(sK0,converse(sK1)),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f30,f21]) ).
fof(f34,plain,
zero != complement(join(complement(sK0),complement(converse(sK1)))),
inference(definition_unfolding,[],[f32,f21]) ).
fof(f35,plain,
zero = complement(join(complement(converse(sK0)),complement(sK1))),
inference(definition_unfolding,[],[f31,f21]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f18]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f19]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f20]) ).
tcf(c_55,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f25]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(cnf_transformation,[],[f26]) ).
tcf(c_59,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(cnf_transformation,[],[f29]) ).
tcf(c_60,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(cnf_transformation,[],[f33]) ).
tcf(c_61,negated_conjecture,
complement(join(complement(sK0),complement(converse(sK1)))) != zero,
inference(cnf_transformation,[],[f34]) ).
tcf(c_62,negated_conjecture,
complement(join(complement(converse(sK0)),complement(sK1))) = zero,
inference(cnf_transformation,[],[f35]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(theory_normalisation,[status(thm)],[c_51,c_50,c_49]) ).
tcf(c_77,negated_conjecture,
complement(join(complement(sK1),complement(converse(sK0)))) = zero,
inference(theory_normalisation,[status(thm)],[c_62,c_50,c_49]) ).
tcf(c_108,plain,
complement(top) = zero,
inference(ac_demodulation,[status(thm)],[c_60,c_59,c_50,c_49]) ).
tcf(c_115,definition,
iPr_def_10 = complement(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_116,definition,
iPr_def_11 = converse(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_117,definition,
iPr_def_12 = complement(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_118,definition,
iPr_def_13 = join(iPr_def_10,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_119,definition,
iPr_def_14 = complement(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_120,definition,
iPr_def_15 = complement(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_121,definition,
iPr_def_16 = converse(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_122,definition,
iPr_def_17 = complement(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_123,definition,
iPr_def_18 = join(iPr_def_15,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_124,definition,
iPr_def_19 = complement(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_125,negated_conjecture,
iPr_def_14 = zero,
inference(demodulation,[status(thm)],[c_77,c_116,c_117,c_115,c_118,c_119]) ).
tcf(c_126,negated_conjecture,
iPr_def_19 != zero,
inference(demodulation,[status(thm)],[c_61,c_121,c_122,c_120,c_123,c_124]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_50,c_49]) ).
tcf(c_214,plain,
iPr_def_14 != iPr_def_19,
inference(light_normalisation,[status(thm)],[c_126,c_125]) ).
tcf(c_215,plain,
complement(top) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_108,c_125]) ).
tcf(c_223,plain,
! [X0: $i] : join(complement(join(iPr_def_15,X0)),complement(join(iPr_def_15,complement(X0)))) = sK0,
inference(superposition,[status(thm)],[c_120,c_75]) ).
tcf(c_224,plain,
! [X0: $i] : join(complement(join(iPr_def_10,X0)),complement(join(iPr_def_10,complement(X0)))) = sK1,
inference(superposition,[status(thm)],[c_115,c_75]) ).
tcf(c_225,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(iPr_def_14,complement(X0)))) = top,
inference(superposition,[status(thm)],[c_215,c_75]) ).
tcf(c_226,plain,
! [X0: $i] : join(complement(join(iPr_def_12,X0)),complement(join(iPr_def_12,complement(X0)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_117,c_75]) ).
tcf(c_227,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(iPr_def_14,complement(X0)))) = iPr_def_13,
inference(superposition,[status(thm)],[c_119,c_75]) ).
tcf(c_228,plain,
! [X0: $i] : join(complement(join(complement(X0),sK0)),complement(join(complement(X0),iPr_def_15))) = X0,
inference(superposition,[status(thm)],[c_120,c_75]) ).
tcf(c_229,plain,
! [X0: $i] : join(complement(join(complement(X0),sK1)),complement(join(complement(X0),iPr_def_10))) = X0,
inference(superposition,[status(thm)],[c_115,c_75]) ).
tcf(c_232,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_13)),complement(join(complement(X0),iPr_def_14))) = X0,
inference(superposition,[status(thm)],[c_119,c_75]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)) = join(complement(X0),X1),
inference(superposition,[status(thm)],[c_75,c_75]) ).
tcf(c_234,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(complement(join(complement(X0),X1)),complement(complement(join(complement(X0),complement(X1))))))) = join(complement(X0),X1),
inference(superposition,[status(thm)],[c_75,c_75]) ).
tcf(c_235,plain,
! [X0: $i] : join(complement(join(iPr_def_13,complement(X0))),complement(join(iPr_def_14,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_232,c_50,c_49]) ).
tcf(c_238,plain,
! [X0: $i] : join(complement(join(iPr_def_10,complement(X0))),complement(join(sK1,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_229,c_50,c_49]) ).
tcf(c_239,plain,
! [X0: $i] : join(complement(join(iPr_def_15,complement(X0))),complement(join(sK0,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_228,c_50,c_49]) ).
tcf(c_240,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(complement(X0),X1)))))) = join(complement(X0),X1),
inference(theory_normalisation,[status(thm)],[c_233,c_50,c_49]) ).
tcf(c_248,plain,
converse(iPr_def_16) = sK1,
inference(superposition,[status(thm)],[c_121,c_55]) ).
tcf(c_249,plain,
converse(iPr_def_11) = sK0,
inference(superposition,[status(thm)],[c_116,c_55]) ).
tcf(c_251,plain,
converse(sK0) = iPr_def_11,
inference(superposition,[status(thm)],[c_249,c_55]) ).
tcf(c_254,plain,
top = iPr_def_13,
inference(demodulation,[status(thm)],[c_225,c_227]) ).
tcf(c_255,plain,
complement(iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_215,c_254]) ).
tcf(c_262,plain,
! [X0: $i] : join(X0,complement(X0)) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_59,c_254]) ).
tcf(c_264,plain,
join(sK1,iPr_def_10) = iPr_def_13,
inference(superposition,[status(thm)],[c_115,c_262]) ).
tcf(c_265,plain,
join(iPr_def_11,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_117,c_262]) ).
tcf(c_266,plain,
join(iPr_def_13,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_255,c_262]) ).
tcf(c_270,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(iPr_def_13)) = X0,
inference(superposition,[status(thm)],[c_262,c_75]) ).
tcf(c_271,plain,
! [X0: $i] : join(complement(iPr_def_13),complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(superposition,[status(thm)],[c_262,c_75]) ).
tcf(c_272,plain,
join(iPr_def_10,sK1) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_264,c_50,c_49]) ).
tcf(c_274,plain,
! [X0: $i] : join(complement(iPr_def_13),complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_270,c_50,c_49]) ).
tcf(c_275,plain,
! [X0: $i] : join(iPr_def_14,complement(join(complement(X0),complement(X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_274,c_255]) ).
tcf(c_276,plain,
! [X0: $i] : join(iPr_def_14,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(light_normalisation,[status(thm)],[c_271,c_255]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X1),complement(X0)))) = X0,
inference(superposition,[status(thm)],[c_49,c_75]) ).
tcf(c_299,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_55,c_56]) ).
tcf(c_304,plain,
! [X0: $i] : join(sK1,converse(X0)) = converse(join(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_248,c_56]) ).
tcf(c_309,plain,
! [X0: $i] : join(converse(X0),iPr_def_11) = converse(join(X0,sK0)),
inference(superposition,[status(thm)],[c_251,c_56]) ).
tcf(c_317,plain,
! [X0: $i] : join(iPr_def_11,converse(X0)) = converse(join(X0,sK0)),
inference(theory_normalisation,[status(thm)],[c_309,c_50,c_49]) ).
tcf(c_336,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = join(iPr_def_13,X1),
inference(superposition,[status(thm)],[c_262,c_50]) ).
tcf(c_339,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_12,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_118,c_50]) ).
tcf(c_341,plain,
! [X0: $i] : join(iPr_def_13,join(iPr_def_14,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_266,c_50]) ).
tcf(c_342,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(join(X0,X1)))) = iPr_def_13,
inference(superposition,[status(thm)],[c_50,c_262]) ).
tcf(c_343,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_12,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_265,c_50]) ).
tcf(c_346,plain,
! [X0: $i] : join(iPr_def_10,join(sK1,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_272,c_50]) ).
tcf(c_356,plain,
join(iPr_def_14,complement(join(iPr_def_10,iPr_def_10))) = sK1,
inference(superposition,[status(thm)],[c_115,c_275]) ).
tcf(c_358,plain,
join(iPr_def_14,complement(join(iPr_def_14,iPr_def_14))) = iPr_def_13,
inference(superposition,[status(thm)],[c_255,c_275]) ).
tcf(c_363,plain,
! [X0: $i] : join(iPr_def_14,join(complement(join(iPr_def_14,iPr_def_14)),X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_358,c_50]) ).
tcf(c_415,plain,
! [X0: $i,X1: $i,X2: $i] : join(complement(join(complement(X0),X1)),join(X2,complement(join(complement(X0),complement(X1))))) = join(X2,X0),
inference(superposition,[status(thm)],[c_75,c_213]) ).
tcf(c_417,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_12)) = join(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_118,c_213]) ).
tcf(c_420,plain,
! [X0: $i] : join(iPr_def_13,join(X0,iPr_def_14)) = join(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_266,c_213]) ).
tcf(c_423,plain,
! [X0: $i] : join(iPr_def_10,join(X0,sK1)) = join(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_272,c_213]) ).
tcf(c_506,plain,
join(iPr_def_13,complement(iPr_def_14)) = join(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_262,c_341]) ).
tcf(c_508,plain,
! [X0: $i] : join(iPr_def_13,complement(join(complement(X0),complement(X0)))) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_275,c_341]) ).
tcf(c_509,plain,
! [X0: $i] : join(iPr_def_13,complement(join(complement(X0),complement(complement(complement(X0)))))) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_276,c_341]) ).
tcf(c_514,plain,
join(iPr_def_13,complement(join(iPr_def_14,iPr_def_14))) = join(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_358,c_341]) ).
tcf(c_528,plain,
! [X0: $i] : join(iPr_def_13,join(iPr_def_14,X0)) = join(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_49,c_420]) ).
tcf(c_582,plain,
join(complement(join(iPr_def_15,iPr_def_16)),complement(join(iPr_def_15,iPr_def_17))) = sK0,
inference(superposition,[status(thm)],[c_122,c_223]) ).
tcf(c_593,plain,
join(complement(join(iPr_def_15,iPr_def_16)),iPr_def_19) = sK0,
inference(light_normalisation,[status(thm)],[c_582,c_123,c_124]) ).
tcf(c_594,plain,
join(iPr_def_19,complement(join(iPr_def_15,iPr_def_16))) = sK0,
inference(theory_normalisation,[status(thm)],[c_593,c_50,c_49]) ).
tcf(c_734,plain,
join(complement(join(iPr_def_10,sK0)),complement(join(iPr_def_10,iPr_def_15))) = sK1,
inference(superposition,[status(thm)],[c_120,c_224]) ).
tcf(c_755,plain,
join(complement(join(iPr_def_10,iPr_def_15)),complement(join(iPr_def_10,sK0))) = sK1,
inference(theory_normalisation,[status(thm)],[c_734,c_50,c_49]) ).
tcf(c_1004,plain,
join(iPr_def_13,complement(complement(join(iPr_def_14,iPr_def_14)))) = join(iPr_def_14,iPr_def_13),
inference(superposition,[status(thm)],[c_262,c_363]) ).
tcf(c_1011,plain,
join(iPr_def_13,complement(complement(join(iPr_def_14,iPr_def_14)))) = join(iPr_def_13,iPr_def_14),
inference(theory_normalisation,[status(thm)],[c_1004,c_50,c_49]) ).
tcf(c_1012,plain,
join(iPr_def_13,complement(complement(join(iPr_def_14,iPr_def_14)))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1011,c_266]) ).
tcf(c_1023,plain,
join(complement(join(iPr_def_12,sK1)),complement(join(iPr_def_12,iPr_def_10))) = iPr_def_11,
inference(superposition,[status(thm)],[c_115,c_226]) ).
tcf(c_1038,plain,
join(complement(join(iPr_def_10,iPr_def_12)),complement(join(iPr_def_12,sK1))) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1023,c_50,c_49]) ).
tcf(c_1039,plain,
join(iPr_def_14,complement(join(iPr_def_12,sK1))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_1038,c_118,c_255]) ).
tcf(c_1258,plain,
join(complement(iPr_def_13),complement(join(iPr_def_14,complement(complement(join(iPr_def_14,iPr_def_14)))))) = iPr_def_13,
inference(superposition,[status(thm)],[c_358,c_227]) ).
tcf(c_1284,plain,
join(complement(join(iPr_def_14,join(iPr_def_14,iPr_def_14))),complement(iPr_def_13)) = iPr_def_13,
inference(superposition,[status(thm)],[c_358,c_227]) ).
tcf(c_1305,plain,
! [X0: $i] : join(complement(join(complement(join(iPr_def_14,X0)),join(iPr_def_14,complement(X0)))),complement(iPr_def_13)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_227,c_75]) ).
tcf(c_1326,plain,
join(complement(iPr_def_13),complement(join(iPr_def_14,join(iPr_def_14,iPr_def_14)))) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1284,c_50,c_49]) ).
tcf(c_1327,plain,
join(iPr_def_14,complement(join(iPr_def_14,join(iPr_def_14,iPr_def_14)))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1326,c_255]) ).
tcf(c_1354,plain,
join(iPr_def_14,complement(join(iPr_def_14,complement(complement(join(iPr_def_14,iPr_def_14)))))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1258,c_255]) ).
tcf(c_1366,plain,
! [X0: $i] : join(complement(iPr_def_13),complement(join(iPr_def_14,join(complement(X0),complement(join(iPr_def_14,X0)))))) = join(iPr_def_14,X0),
inference(theory_normalisation,[status(thm)],[c_1305,c_50,c_49]) ).
tcf(c_1367,plain,
! [X0: $i] : join(iPr_def_14,complement(join(iPr_def_14,join(complement(X0),complement(join(iPr_def_14,X0)))))) = join(iPr_def_14,X0),
inference(light_normalisation,[status(thm)],[c_1366,c_255]) ).
tcf(c_1423,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_12)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_49,c_339]) ).
tcf(c_1426,plain,
join(iPr_def_13,complement(iPr_def_12)) = join(iPr_def_10,iPr_def_13),
inference(superposition,[status(thm)],[c_262,c_339]) ).
tcf(c_1456,plain,
join(iPr_def_13,complement(join(iPr_def_14,join(iPr_def_14,iPr_def_14)))) = join(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_1327,c_341]) ).
tcf(c_1559,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(complement(iPr_def_13),complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))) = iPr_def_13,
inference(superposition,[status(thm)],[c_227,c_234]) ).
tcf(c_1573,plain,
! [X0: $i] : join(complement(X0),complement(join(complement(join(complement(X0),complement(X0))),complement(complement(iPr_def_13))))) = join(complement(X0),complement(X0)),
inference(superposition,[status(thm)],[c_262,c_234]) ).
tcf(c_1607,plain,
! [X0: $i] : join(complement(X0),complement(join(complement(complement(iPr_def_13)),complement(join(complement(X0),complement(X0)))))) = join(complement(X0),complement(X0)),
inference(theory_normalisation,[status(thm)],[c_1573,c_50,c_49]) ).
tcf(c_1608,plain,
! [X0: $i] : join(complement(X0),complement(join(complement(iPr_def_14),complement(join(complement(X0),complement(X0)))))) = join(complement(X0),complement(X0)),
inference(light_normalisation,[status(thm)],[c_1607,c_255]) ).
tcf(c_1619,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1559,c_255]) ).
tcf(c_1647,plain,
join(iPr_def_13,complement(iPr_def_12)) = join(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_262,c_343]) ).
tcf(c_1653,plain,
join(iPr_def_10,iPr_def_13) = join(iPr_def_11,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_1647,c_1426]) ).
tcf(c_1727,plain,
join(iPr_def_14,complement(join(iPr_def_13,complement(join(iPr_def_14,join(iPr_def_14,iPr_def_14)))))) = join(iPr_def_14,join(iPr_def_14,iPr_def_14)),
inference(superposition,[status(thm)],[c_363,c_1367]) ).
tcf(c_1838,plain,
join(iPr_def_14,complement(join(iPr_def_13,iPr_def_13))) = join(iPr_def_14,join(iPr_def_14,iPr_def_14)),
inference(light_normalisation,[status(thm)],[c_1727,c_1456]) ).
tcf(c_1967,plain,
join(complement(iPr_def_13),complement(join(iPr_def_14,complement(complement(join(iPr_def_14,iPr_def_14)))))) = complement(join(iPr_def_14,iPr_def_14)),
inference(superposition,[status(thm)],[c_1012,c_235]) ).
tcf(c_1978,plain,
join(complement(join(iPr_def_13,complement(iPr_def_14))),complement(iPr_def_13)) = iPr_def_14,
inference(superposition,[status(thm)],[c_262,c_235]) ).
tcf(c_1980,plain,
! [X0: $i] : join(complement(join(iPr_def_13,complement(join(complement(X0),complement(complement(complement(X0))))))),complement(X0)) = join(complement(X0),complement(complement(complement(X0)))),
inference(superposition,[status(thm)],[c_276,c_235]) ).
tcf(c_1984,plain,
join(complement(join(iPr_def_13,complement(join(iPr_def_14,iPr_def_14)))),complement(iPr_def_13)) = join(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_358,c_235]) ).
tcf(c_2026,plain,
join(complement(iPr_def_13),complement(join(iPr_def_13,complement(iPr_def_14)))) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_1978,c_50,c_49]) ).
tcf(c_2027,plain,
join(iPr_def_14,join(iPr_def_14,iPr_def_14)) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_2026,c_255,c_506,c_1838]) ).
tcf(c_2041,plain,
join(complement(iPr_def_13),complement(join(iPr_def_13,complement(join(iPr_def_14,iPr_def_14))))) = join(iPr_def_14,iPr_def_14),
inference(theory_normalisation,[status(thm)],[c_1984,c_50,c_49]) ).
tcf(c_2042,plain,
join(iPr_def_14,join(iPr_def_14,iPr_def_14)) = join(iPr_def_14,iPr_def_14),
inference(light_normalisation,[status(thm)],[c_2041,c_255,c_514,c_1838]) ).
tcf(c_2051,plain,
complement(join(iPr_def_14,iPr_def_14)) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1967,c_255,c_1354]) ).
tcf(c_2083,plain,
! [X0: $i] : join(complement(X0),complement(join(iPr_def_13,complement(join(complement(X0),complement(complement(complement(X0)))))))) = join(complement(X0),complement(complement(complement(X0)))),
inference(theory_normalisation,[status(thm)],[c_1980,c_50,c_49]) ).
tcf(c_2084,plain,
! [X0: $i] : join(complement(X0),complement(join(iPr_def_13,X0))) = join(complement(X0),complement(complement(complement(X0)))),
inference(light_normalisation,[status(thm)],[c_2083,c_509]) ).
tcf(c_2163,plain,
join(sK1,iPr_def_13) = join(iPr_def_13,iPr_def_12),
inference(superposition,[status(thm)],[c_417,c_346]) ).
tcf(c_2164,plain,
join(iPr_def_12,iPr_def_13) = join(iPr_def_13,sK1),
inference(theory_normalisation,[status(thm)],[c_2163,c_50,c_49]) ).
tcf(c_2266,plain,
join(iPr_def_14,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_2042,c_2027]) ).
tcf(c_2268,plain,
complement(iPr_def_14) = iPr_def_13,
inference(demodulation,[status(thm)],[c_2051,c_2266]) ).
tcf(c_2270,plain,
! [X0: $i] : join(iPr_def_14,join(iPr_def_14,X0)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_2266,c_50]) ).
tcf(c_2861,plain,
join(complement(join(iPr_def_15,iPr_def_17)),complement(join(sK0,iPr_def_17))) = iPr_def_16,
inference(superposition,[status(thm)],[c_122,c_239]) ).
tcf(c_2876,plain,
join(complement(join(iPr_def_15,iPr_def_17)),complement(join(iPr_def_17,sK0))) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_2861,c_50,c_49]) ).
tcf(c_2877,plain,
join(iPr_def_19,complement(join(iPr_def_17,sK0))) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_2876,c_123,c_124]) ).
tcf(c_3103,plain,
! [X0: $i] : join(complement(X0),complement(complement(complement(X0)))) = join(complement(X0),complement(X0)),
inference(light_normalisation,[status(thm)],[c_1608,c_508,c_2084,c_2268]) ).
tcf(c_3472,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(complement(join(iPr_def_14,X0)),join(complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))),complement(iPr_def_13))))) = iPr_def_13,
inference(superposition,[status(thm)],[c_1619,c_240]) ).
tcf(c_3534,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(complement(iPr_def_13),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))))))) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_3472,c_50,c_49]) ).
tcf(c_3535,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))))))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_3534,c_255]) ).
tcf(c_3878,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(complement(join(complement(join(iPr_def_14,X0)),join(iPr_def_14,join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))))))),complement(complement(iPr_def_13))))) = join(complement(join(iPr_def_14,X0)),join(iPr_def_14,join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))),
inference(superposition,[status(thm)],[c_3535,c_234]) ).
tcf(c_3879,plain,
! [X0: $i] : join(complement(join(complement(join(iPr_def_14,X0)),join(iPr_def_14,join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0)))))))))))))),complement(iPr_def_13)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_3535,c_75]) ).
tcf(c_3949,plain,
! [X0: $i] : join(complement(iPr_def_13),complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))))) = join(iPr_def_14,X0),
inference(theory_normalisation,[status(thm)],[c_3879,c_50,c_49]) ).
tcf(c_3950,plain,
! [X0: $i] : join(iPr_def_14,complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))))) = join(iPr_def_14,X0),
inference(light_normalisation,[status(thm)],[c_3949,c_255]) ).
tcf(c_3965,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(complement(complement(iPr_def_13)),complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))))))) = join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))),
inference(theory_normalisation,[status(thm)],[c_3878,c_50,c_49]) ).
tcf(c_3966,plain,
! [X0: $i] : join(complement(join(iPr_def_14,X0)),complement(join(iPr_def_13,complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))))))) = join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))),
inference(light_normalisation,[status(thm)],[c_3965,c_255,c_2268]) ).
tcf(c_4117,plain,
! [X0: $i] : join(iPr_def_13,complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))))) = join(iPr_def_13,join(iPr_def_14,X0)),
inference(superposition,[status(thm)],[c_3950,c_341]) ).
tcf(c_4175,plain,
! [X0: $i] : join(iPr_def_13,complement(join(iPr_def_14,join(complement(join(iPr_def_14,X0)),join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(complement(join(complement(join(iPr_def_14,X0)),complement(complement(join(iPr_def_14,complement(X0))))))))))))))) = join(X0,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_4117,c_528]) ).
tcf(c_5969,plain,
! [X0: $i] : join(iPr_def_14,X0) = X0,
inference(superposition,[status(thm)],[c_275,c_2270]) ).
tcf(c_6032,plain,
! [X0: $i] : complement(join(complement(X0),complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_275,c_5969]) ).
tcf(c_6035,plain,
complement(join(iPr_def_10,iPr_def_10)) = sK1,
inference(demodulation,[status(thm)],[c_356,c_5969]) ).
tcf(c_6046,plain,
complement(join(iPr_def_12,sK1)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_1039,c_5969]) ).
tcf(c_6149,plain,
! [X0: $i] : join(X0,iPr_def_14) = X0,
inference(superposition,[status(thm)],[c_5969,c_49]) ).
tcf(c_6688,plain,
join(complement(join(iPr_def_10,sK1)),complement(join(sK1,sK1))) = join(iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_6035,c_238]) ).
tcf(c_6695,plain,
join(join(iPr_def_10,iPr_def_10),sK1) = iPr_def_13,
inference(superposition,[status(thm)],[c_6035,c_262]) ).
tcf(c_6701,plain,
join(iPr_def_10,join(iPr_def_10,sK1)) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_6695,c_50,c_49]) ).
tcf(c_6702,plain,
join(iPr_def_10,iPr_def_13) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_6701,c_272]) ).
tcf(c_6711,plain,
join(iPr_def_14,complement(join(sK1,sK1))) = join(iPr_def_10,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_6688,c_255,c_272]) ).
tcf(c_6718,plain,
join(iPr_def_11,iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_1653,c_6702]) ).
tcf(c_6732,plain,
join(complement(iPr_def_13),complement(join(iPr_def_10,complement(iPr_def_13)))) = sK1,
inference(superposition,[status(thm)],[c_6702,c_224]) ).
tcf(c_6733,plain,
join(iPr_def_14,complement(join(iPr_def_10,iPr_def_14))) = sK1,
inference(light_normalisation,[status(thm)],[c_6732,c_255]) ).
tcf(c_6734,plain,
complement(iPr_def_10) = sK1,
inference(demodulation,[status(thm)],[c_6733,c_5969,c_6149]) ).
tcf(c_6742,plain,
join(complement(join(iPr_def_10,sK1)),complement(join(sK1,sK1))) = iPr_def_10,
inference(superposition,[status(thm)],[c_6734,c_238]) ).
tcf(c_6759,plain,
join(iPr_def_10,iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_6742,c_255,c_272,c_6711]) ).
tcf(c_6772,plain,
join(iPr_def_14,complement(join(sK1,sK1))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_6711,c_6759]) ).
tcf(c_6773,plain,
complement(join(sK1,sK1)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_6772,c_5969]) ).
tcf(c_6780,plain,
join(complement(join(iPr_def_15,iPr_def_10)),complement(join(sK0,iPr_def_10))) = join(sK1,sK1),
inference(superposition,[status(thm)],[c_6773,c_239]) ).
tcf(c_6805,plain,
join(complement(join(iPr_def_10,iPr_def_15)),complement(join(iPr_def_10,sK0))) = join(sK1,sK1),
inference(theory_normalisation,[status(thm)],[c_6780,c_50,c_49]) ).
tcf(c_6806,plain,
join(sK1,sK1) = sK1,
inference(light_normalisation,[status(thm)],[c_6805,c_755]) ).
tcf(c_6822,plain,
! [X0: $i] : join(iPr_def_14,join(complement(X0),join(complement(X0),complement(complement(join(iPr_def_14,complement(complement(join(complement(X0),complement(complement(join(iPr_def_14,complement(X0))))))))))))) = join(complement(X0),complement(join(X0,iPr_def_13))),
inference(light_normalisation,[status(thm)],[c_3966,c_4175,c_5969]) ).
tcf(c_6823,plain,
! [X0: $i] : join(complement(X0),join(complement(X0),complement(X0))) = join(complement(X0),complement(join(X0,iPr_def_13))),
inference(demodulation,[status(thm)],[c_6822,c_3103,c_5969,c_6032]) ).
tcf(c_6860,plain,
! [X0: $i] : join(complement(X0),complement(join(complement(join(complement(X0),complement(join(X0,iPr_def_13)))),complement(complement(join(complement(X0),complement(join(complement(X0),complement(X0))))))))) = join(complement(X0),complement(join(X0,iPr_def_13))),
inference(superposition,[status(thm)],[c_6823,c_234]) ).
tcf(c_6861,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(join(X0,iPr_def_13)))),complement(join(complement(X0),complement(join(complement(X0),complement(X0)))))) = X0,
inference(superposition,[status(thm)],[c_6823,c_75]) ).
tcf(c_6910,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(join(X0,iPr_def_13)))),complement(join(complement(X0),X0))) = X0,
inference(light_normalisation,[status(thm)],[c_6861,c_6032]) ).
tcf(c_6911,plain,
! [X0: $i] : join(complement(join(X0,complement(X0))),complement(join(complement(X0),complement(join(X0,iPr_def_13))))) = X0,
inference(theory_normalisation,[status(thm)],[c_6910,c_50,c_49]) ).
tcf(c_6912,plain,
! [X0: $i] : join(iPr_def_14,complement(join(complement(X0),complement(join(X0,iPr_def_13))))) = X0,
inference(light_normalisation,[status(thm)],[c_6911,c_255,c_262]) ).
tcf(c_6915,plain,
! [X0: $i] : join(complement(X0),complement(join(complement(join(complement(X0),complement(join(X0,iPr_def_13)))),complement(complement(join(complement(X0),X0)))))) = join(complement(X0),complement(join(X0,iPr_def_13))),
inference(light_normalisation,[status(thm)],[c_6860,c_6032]) ).
tcf(c_6916,plain,
! [X0: $i] : join(complement(X0),complement(join(complement(complement(join(X0,complement(X0)))),complement(join(complement(X0),complement(join(X0,iPr_def_13))))))) = join(complement(X0),complement(join(X0,iPr_def_13))),
inference(theory_normalisation,[status(thm)],[c_6915,c_50,c_49]) ).
tcf(c_6917,plain,
! [X0: $i] : join(complement(X0),complement(join(iPr_def_13,complement(join(complement(X0),complement(join(X0,iPr_def_13))))))) = join(complement(X0),complement(join(X0,iPr_def_13))),
inference(light_normalisation,[status(thm)],[c_6916,c_255,c_262,c_2268]) ).
tcf(c_6951,plain,
! [X0: $i] : complement(join(complement(X0),complement(join(X0,iPr_def_13)))) = X0,
inference(demodulation,[status(thm)],[c_6912,c_5969]) ).
tcf(c_6954,plain,
complement(join(iPr_def_12,complement(join(iPr_def_11,iPr_def_13)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_117,c_6951]) ).
tcf(c_6976,plain,
! [X0: $i] : join(X0,complement(complement(X0))) = join(X0,X0),
inference(superposition,[status(thm)],[c_6951,c_3103]) ).
tcf(c_7010,plain,
complement(join(iPr_def_12,iPr_def_14)) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_6954,c_255,c_6718]) ).
tcf(c_7098,plain,
join(sK1,iPr_def_13) = join(iPr_def_10,sK1),
inference(superposition,[status(thm)],[c_6806,c_423]) ).
tcf(c_7101,plain,
join(iPr_def_10,sK1) = join(iPr_def_13,sK1),
inference(theory_normalisation,[status(thm)],[c_7098,c_50,c_49]) ).
tcf(c_7102,plain,
join(iPr_def_13,sK1) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_7101,c_272,c_2164]) ).
tcf(c_7105,plain,
join(iPr_def_12,iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_2164,c_7102]) ).
tcf(c_7121,plain,
complement(iPr_def_12) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7010,c_6149]) ).
tcf(c_7137,plain,
! [X0: $i] : join(complement(X0),complement(join(X0,iPr_def_13))) = join(complement(X0),complement(complement(complement(X0)))),
inference(light_normalisation,[status(thm)],[c_6917,c_2084,c_6951]) ).
tcf(c_7138,plain,
! [X0: $i] : join(complement(X0),complement(join(X0,iPr_def_13))) = join(complement(X0),complement(X0)),
inference(demodulation,[status(thm)],[c_7137,c_6976]) ).
tcf(c_7151,plain,
join(iPr_def_11,complement(join(iPr_def_12,iPr_def_13))) = join(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_7121,c_7138]) ).
tcf(c_7164,plain,
join(iPr_def_11,iPr_def_11) = join(iPr_def_11,iPr_def_14),
inference(light_normalisation,[status(thm)],[c_7151,c_255,c_7105]) ).
tcf(c_7179,plain,
join(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7164,c_6149]) ).
tcf(c_7521,plain,
complement(join(iPr_def_11,iPr_def_11)) = join(iPr_def_12,sK1),
inference(superposition,[status(thm)],[c_6046,c_6032]) ).
tcf(c_7530,plain,
join(iPr_def_12,sK1) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_7521,c_117,c_7179]) ).
tcf(c_7856,plain,
! [X0: $i] : join(iPr_def_12,join(sK1,X0)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_7530,c_50]) ).
tcf(c_9209,plain,
! [X0: $i] : join(X0,converse(iPr_def_14)) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_6149,c_299]) ).
tcf(c_9254,plain,
! [X0: $i] : join(X0,converse(iPr_def_14)) = X0,
inference(light_normalisation,[status(thm)],[c_9209,c_55]) ).
tcf(c_9407,plain,
converse(iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_9254,c_5969]) ).
tcf(c_9600,plain,
! [X0: $i] : join(complement(join(complement(complement(X0)),X0)),complement(iPr_def_13)) = complement(X0),
inference(superposition,[status(thm)],[c_262,c_295]) ).
tcf(c_9650,plain,
! [X0: $i] : join(complement(iPr_def_13),complement(join(X0,complement(complement(X0))))) = complement(X0),
inference(theory_normalisation,[status(thm)],[c_9600,c_50,c_49]) ).
tcf(c_9651,plain,
! [X0: $i] : join(iPr_def_14,complement(join(X0,X0))) = complement(X0),
inference(light_normalisation,[status(thm)],[c_9650,c_255,c_6976]) ).
tcf(c_9822,plain,
! [X0: $i] : complement(join(X0,X0)) = complement(X0),
inference(demodulation,[status(thm)],[c_9651,c_5969]) ).
tcf(c_9830,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X1),complement(X0)))) = join(X0,X0),
inference(superposition,[status(thm)],[c_9822,c_295]) ).
tcf(c_9839,plain,
! [X0: $i] : join(join(X0,X0),complement(X0)) = iPr_def_13,
inference(superposition,[status(thm)],[c_9822,c_262]) ).
tcf(c_9842,plain,
! [X0: $i] : join(complement(join(complement(X0),X0)),complement(complement(X0))) = X0,
inference(superposition,[status(thm)],[c_9822,c_295]) ).
tcf(c_9843,plain,
! [X0: $i] : join(X0,join(X0,complement(X0))) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_9839,c_50,c_49]) ).
tcf(c_9844,plain,
! [X0: $i] : join(X0,iPr_def_13) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_9843,c_262]) ).
tcf(c_9845,plain,
! [X0: $i] : join(complement(complement(X0)),complement(join(X0,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_9842,c_50,c_49]) ).
tcf(c_9846,plain,
! [X0: $i] : join(complement(complement(X0)),iPr_def_14) = X0,
inference(light_normalisation,[status(thm)],[c_9845,c_255,c_262]) ).
tcf(c_9847,plain,
! [X0: $i] : join(iPr_def_14,complement(complement(X0))) = X0,
inference(theory_normalisation,[status(thm)],[c_9846,c_50,c_49]) ).
tcf(c_9852,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(light_normalisation,[status(thm)],[c_9830,c_295]) ).
tcf(c_9865,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_12)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_417,c_9844]) ).
tcf(c_9866,plain,
! [X0: $i] : join(iPr_def_13,X0) = iPr_def_13,
inference(demodulation,[status(thm)],[c_1423,c_9865]) ).
tcf(c_9897,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(demodulation,[status(thm)],[c_9847,c_5969]) ).
tcf(c_10441,plain,
! [X0: $i,X1: $i] : join(X0,join(X0,X1)) = join(X0,X1),
inference(superposition,[status(thm)],[c_9852,c_50]) ).
tcf(c_10714,plain,
join(iPr_def_19,sK0) = sK0,
inference(superposition,[status(thm)],[c_594,c_10441]) ).
tcf(c_10722,plain,
join(iPr_def_19,iPr_def_16) = iPr_def_16,
inference(superposition,[status(thm)],[c_2877,c_10441]) ).
tcf(c_10754,plain,
join(iPr_def_16,iPr_def_19) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_10722,c_50,c_49]) ).
tcf(c_10860,plain,
join(iPr_def_11,converse(iPr_def_19)) = converse(sK0),
inference(superposition,[status(thm)],[c_10714,c_317]) ).
tcf(c_10861,plain,
join(iPr_def_11,converse(iPr_def_19)) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_10860,c_251]) ).
tcf(c_10866,plain,
join(sK1,converse(iPr_def_19)) = converse(iPr_def_16),
inference(superposition,[status(thm)],[c_10754,c_304]) ).
tcf(c_10867,plain,
join(sK1,converse(iPr_def_19)) = sK1,
inference(light_normalisation,[status(thm)],[c_10866,c_248]) ).
tcf(c_10875,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_336,c_9866]) ).
tcf(c_11101,plain,
! [X0: $i] : join(iPr_def_11,join(converse(iPr_def_19),X0)) = join(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_10861,c_50]) ).
tcf(c_11116,plain,
join(iPr_def_12,converse(iPr_def_19)) = join(iPr_def_12,sK1),
inference(superposition,[status(thm)],[c_10867,c_7856]) ).
tcf(c_11122,plain,
join(iPr_def_12,converse(iPr_def_19)) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_11116,c_7530]) ).
tcf(c_12717,plain,
join(iPr_def_11,complement(converse(iPr_def_19))) = join(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_262,c_11101]) ).
tcf(c_13193,plain,
! [X0: $i,X1: $i,X2: $i] : join(complement(iPr_def_13),join(X0,complement(join(complement(X1),complement(join(X2,complement(join(complement(X1),X2)))))))) = join(X0,X1),
inference(superposition,[status(thm)],[c_342,c_415]) ).
tcf(c_13236,plain,
! [X0: $i,X1: $i,X2: $i] : join(complement(join(X0,X1)),join(X2,complement(join(X0,complement(X1))))) = join(X2,complement(X0)),
inference(superposition,[status(thm)],[c_9897,c_415]) ).
tcf(c_13327,plain,
! [X0: $i,X1: $i,X2: $i] : join(iPr_def_14,join(X0,complement(join(complement(X1),complement(join(X2,complement(join(complement(X1),X2)))))))) = join(X0,X1),
inference(light_normalisation,[status(thm)],[c_13193,c_255]) ).
tcf(c_13337,plain,
! [X0: $i,X1: $i] : join(X0,complement(complement(X1))) = join(X0,X1),
inference(demodulation,[status(thm)],[c_415,c_13236]) ).
tcf(c_13638,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,complement(join(complement(X1),complement(join(X2,complement(join(complement(X1),X2))))))) = join(X0,X1),
inference(demodulation,[status(thm)],[c_13327,c_5969]) ).
tcf(c_13682,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,complement(join(complement(X1),complement(join(join(complement(complement(X1)),X2),complement(iPr_def_13)))))) = join(X0,X1),
inference(superposition,[status(thm)],[c_10875,c_13638]) ).
tcf(c_13769,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,complement(join(complement(X1),complement(join(complement(iPr_def_13),join(X2,complement(complement(X1)))))))) = join(X0,X1),
inference(theory_normalisation,[status(thm)],[c_13682,c_50,c_49]) ).
tcf(c_13770,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,complement(join(complement(X1),complement(join(iPr_def_14,join(X2,complement(complement(X1)))))))) = join(X0,X1),
inference(light_normalisation,[status(thm)],[c_13769,c_255]) ).
tcf(c_13823,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,complement(join(complement(X1),complement(join(X2,X1))))) = join(X0,X1),
inference(demodulation,[status(thm)],[c_13770,c_5969,c_13337]) ).
tcf(c_13961,plain,
! [X0: $i,X1: $i] : complement(join(complement(X0),complement(join(X1,X0)))) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_13823,c_5969]) ).
tcf(c_13992,plain,
! [X0: $i,X1: $i] : complement(join(complement(X0),complement(join(X1,X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_13961,c_5969]) ).
tcf(c_34865,plain,
join(iPr_def_11,complement(converse(iPr_def_19))) = iPr_def_13,
inference(demodulation,[status(thm)],[c_12717,c_9844]) ).
tcf(c_36645,plain,
complement(join(complement(converse(iPr_def_19)),complement(iPr_def_12))) = converse(iPr_def_19),
inference(superposition,[status(thm)],[c_11122,c_13992]) ).
tcf(c_36880,plain,
complement(join(complement(iPr_def_12),complement(converse(iPr_def_19)))) = converse(iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_36645,c_50,c_49]) ).
tcf(c_36881,plain,
converse(iPr_def_19) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_36880,c_255,c_7121,c_34865]) ).
tcf(c_37540,plain,
converse(iPr_def_14) = iPr_def_19,
inference(superposition,[status(thm)],[c_36881,c_55]) ).
tcf(c_37560,plain,
iPr_def_14 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_37540,c_9407]) ).
tcf(c_37561,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_37560,c_214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL006+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 07:13:20 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.38 Running first-order theorem proving
% 0.13/0.38 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 18.60/3.26 % SZS status Started for theBenchmark.p
% 18.60/3.26 % SZS status Theorem for theBenchmark.p
% 18.60/3.26
% 18.60/3.26 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 18.60/3.26
% 18.60/3.26 % ------ iProver source info
% 18.60/3.26
% 18.60/3.26 % git: date: 2026-07-19 20:42:38 +0200
% 18.60/3.26 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 18.60/3.26 % git: non_committed_changes: false
% 18.60/3.26
% 18.60/3.26 % ------ Parsing...
% 18.60/3.26 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 18.60/3.26 %
% 18.60/3.26
% 18.60/3.26 % ------ Preprocessing... sup_sim: 1 sf_s rm: 0 0s sf_e pe_s pe_e %
% 18.60/3.26
% 18.60/3.26 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 18.60/3.26 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 18.60/3.26
% 18.60/3.26 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 18.60/3.26 % ------ Proving...
% 18.60/3.26 % ------ Problem Properties
% 18.60/3.26
% 18.60/3.26 %
% 18.60/3.26 % clauses 24
% 18.60/3.26 % conjectures 2
% 18.60/3.26 % EPR 2
% 18.60/3.26 % Horn 24
% 18.60/3.26 % unary 24
% 18.60/3.26 % binary 0
% 18.60/3.26 % lits 24
% 18.60/3.26 % lits eq 24
% 18.60/3.26 % fd_pure 0
% 18.60/3.26 % fd_pseudo 0
% 18.60/3.26 % fd_cond 0
% 18.60/3.26 % fd_pseudo_cond 0
% 18.60/3.26 % AC symbols 1
% 18.60/3.26
% 18.60/3.26 % ------ Schedule UEQ
% 18.60/3.26
% 18.60/3.26 % ------ Option_UEQ Time Limit: 10.
% 18.60/3.26
% 18.60/3.26
% 18.60/3.26 % ------
% 18.60/3.26 % Current options:
% 18.60/3.26 % ------
% 18.60/3.26
% 18.60/3.26
% 18.60/3.26 %
% 18.60/3.26
% 18.60/3.26 % ------ Proving...
% 18.60/3.26 %
% 18.60/3.26
% 18.60/3.26 % SZS status Theorem for theBenchmark.p
% 18.60/3.26
% 18.60/3.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 18.60/3.26
% 18.60/3.26
%------------------------------------------------------------------------------