%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL005+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 : n009.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:31 PM UTC 2026
% Result : Theorem 30.17s 10.35s
% Output : CNFRefutation 30.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 25
% Syntax : Number of formulae : 353 ( 353 unt; 11 def)
% Number of atoms : 933 ( 352 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 11 usr; 12 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 182 ( 0 sgn 180 !; 2 ?; 125 :)
% 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(f5,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
fof(f6,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_identity) ).
fof(f7,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
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(f10,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
fof(f11,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
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] : converse(meet(X0,X1)) = meet(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f15,negated_conjecture,
~ ! [X0,X1] : converse(meet(X0,X1)) = meet(converse(X0),converse(X1)),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
? [X0,X1] : converse(meet(X0,X1)) != meet(converse(X0),converse(X1)),
inference(ennf_transformation,[],[f15]) ).
fof(f17,plain,
converse(meet(sK0,sK1)) != meet(converse(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(f22,plain,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f24,plain,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
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(f27,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[],[f10]) ).
fof(f28,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(cnf_transformation,[],[f11]) ).
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,
converse(meet(sK0,sK1)) != meet(converse(sK0),converse(sK1)),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f30,f21]) ).
fof(f33,plain,
converse(complement(join(complement(sK0),complement(sK1)))) != complement(join(complement(converse(sK0)),complement(converse(sK1)))),
inference(definition_unfolding,[],[f31,f21,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_52,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(cnf_transformation,[],[f22]) ).
tcf(c_53,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f23]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X0,X2),X1),
inference(cnf_transformation,[],[f24]) ).
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_57,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(cnf_transformation,[],[f27]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[],[f28]) ).
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,[],[f32]) ).
tcf(c_61,negated_conjecture,
complement(join(complement(converse(sK0)),complement(converse(sK1)))) != converse(complement(join(complement(sK0),complement(sK1)))),
inference(cnf_transformation,[],[f33]) ).
tcf(c_74,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_75,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(theory_normalisation,[status(thm)],[c_58,c_50,c_49]) ).
tcf(c_104,plain,
complement(top) = zero,
inference(ac_demodulation,[status(thm)],[c_60,c_59,c_50,c_49]) ).
tcf(c_111,definition,
iPr_def_10 = converse(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_112,definition,
iPr_def_11 = complement(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_113,definition,
iPr_def_12 = converse(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_114,definition,
iPr_def_13 = complement(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_115,definition,
iPr_def_14 = join(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_116,definition,
iPr_def_15 = complement(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_117,definition,
iPr_def_16 = complement(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_118,definition,
iPr_def_17 = complement(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_119,definition,
iPr_def_18 = join(iPr_def_16,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_120,definition,
iPr_def_19 = complement(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_121,definition,
iPr_def_20 = converse(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_122,negated_conjecture,
iPr_def_15 != iPr_def_20,
inference(demodulation,[status(thm)],[c_61,c_118,c_117,c_119,c_120,c_121,c_113,c_114,c_111,c_112,c_115,c_116]) ).
tcf(c_209,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_217,plain,
! [X0: $i] : join(complement(join(iPr_def_16,X0)),complement(join(iPr_def_16,complement(X0)))) = sK0,
inference(superposition,[status(thm)],[c_117,c_74]) ).
tcf(c_219,plain,
! [X0: $i] : join(complement(join(iPr_def_11,X0)),complement(join(iPr_def_11,complement(X0)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_112,c_74]) ).
tcf(c_220,plain,
! [X0: $i] : join(complement(join(iPr_def_13,X0)),complement(join(iPr_def_13,complement(X0)))) = iPr_def_12,
inference(superposition,[status(thm)],[c_114,c_74]) ).
tcf(c_221,plain,
! [X0: $i] : join(complement(join(iPr_def_15,X0)),complement(join(iPr_def_15,complement(X0)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_116,c_74]) ).
tcf(c_222,plain,
! [X0: $i] : join(complement(join(complement(X0),sK0)),complement(join(complement(X0),iPr_def_16))) = X0,
inference(superposition,[status(thm)],[c_117,c_74]) ).
tcf(c_223,plain,
! [X0: $i] : join(complement(join(complement(X0),top)),complement(join(complement(X0),zero))) = X0,
inference(superposition,[status(thm)],[c_104,c_74]) ).
tcf(c_224,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_10)),complement(join(complement(X0),iPr_def_11))) = X0,
inference(superposition,[status(thm)],[c_112,c_74]) ).
tcf(c_225,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_12)),complement(join(complement(X0),iPr_def_13))) = X0,
inference(superposition,[status(thm)],[c_114,c_74]) ).
tcf(c_226,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_14)),complement(join(complement(X0),iPr_def_15))) = X0,
inference(superposition,[status(thm)],[c_116,c_74]) ).
tcf(c_229,plain,
! [X0: $i] : join(complement(join(iPr_def_14,complement(X0))),complement(join(iPr_def_15,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_226,c_50,c_49]) ).
tcf(c_230,plain,
! [X0: $i] : join(complement(join(iPr_def_12,complement(X0))),complement(join(iPr_def_13,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_225,c_50,c_49]) ).
tcf(c_231,plain,
! [X0: $i] : join(complement(join(iPr_def_10,complement(X0))),complement(join(iPr_def_11,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_224,c_50,c_49]) ).
tcf(c_232,plain,
! [X0: $i] : join(complement(join(top,complement(X0))),complement(join(zero,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_223,c_50,c_49]) ).
tcf(c_233,plain,
! [X0: $i] : join(complement(join(iPr_def_16,complement(X0))),complement(join(sK0,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_222,c_50,c_49]) ).
tcf(c_236,plain,
! [X0: $i] : join(complement(join(iPr_def_17,X0)),complement(join(iPr_def_17,complement(X0)))) = sK1,
inference(superposition,[status(thm)],[c_118,c_74]) ).
tcf(c_242,plain,
converse(iPr_def_10) = sK0,
inference(superposition,[status(thm)],[c_111,c_55]) ).
tcf(c_243,plain,
converse(iPr_def_12) = sK1,
inference(superposition,[status(thm)],[c_113,c_55]) ).
tcf(c_244,plain,
converse(iPr_def_20) = iPr_def_19,
inference(superposition,[status(thm)],[c_121,c_55]) ).
tcf(c_245,plain,
converse(sK0) = iPr_def_10,
inference(superposition,[status(thm)],[c_242,c_55]) ).
tcf(c_246,plain,
converse(sK1) = iPr_def_12,
inference(superposition,[status(thm)],[c_243,c_55]) ).
tcf(c_247,plain,
converse(iPr_def_19) = iPr_def_20,
inference(superposition,[status(thm)],[c_244,c_55]) ).
tcf(c_251,plain,
join(sK0,iPr_def_16) = top,
inference(superposition,[status(thm)],[c_117,c_59]) ).
tcf(c_252,plain,
join(sK1,iPr_def_17) = top,
inference(superposition,[status(thm)],[c_118,c_59]) ).
tcf(c_253,plain,
join(top,zero) = top,
inference(superposition,[status(thm)],[c_104,c_59]) ).
tcf(c_254,plain,
join(iPr_def_10,iPr_def_11) = top,
inference(superposition,[status(thm)],[c_112,c_59]) ).
tcf(c_255,plain,
join(iPr_def_12,iPr_def_13) = top,
inference(superposition,[status(thm)],[c_114,c_59]) ).
tcf(c_256,plain,
join(iPr_def_14,iPr_def_15) = top,
inference(superposition,[status(thm)],[c_116,c_59]) ).
tcf(c_258,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_59,c_74]) ).
tcf(c_260,plain,
join(iPr_def_17,sK1) = top,
inference(theory_normalisation,[status(thm)],[c_252,c_50,c_49]) ).
tcf(c_261,plain,
join(iPr_def_16,sK0) = top,
inference(theory_normalisation,[status(thm)],[c_251,c_50,c_49]) ).
tcf(c_262,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_258,c_50,c_49]) ).
tcf(c_263,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_262,c_104]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(X1,complement(composition(converse(X1),X0)))) = complement(X0),
inference(superposition,[status(thm)],[c_55,c_75]) ).
tcf(c_286,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_74]) ).
tcf(c_290,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_55,c_56]) ).
tcf(c_295,plain,
! [X0: $i] : join(iPr_def_20,converse(X0)) = converse(join(iPr_def_19,X0)),
inference(superposition,[status(thm)],[c_247,c_56]) ).
tcf(c_297,plain,
! [X0: $i] : join(sK0,converse(X0)) = converse(join(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_242,c_56]) ).
tcf(c_300,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(superposition,[status(thm)],[c_55,c_56]) ).
tcf(c_301,plain,
! [X0: $i] : join(converse(X0),iPr_def_10) = converse(join(X0,sK0)),
inference(superposition,[status(thm)],[c_245,c_56]) ).
tcf(c_303,plain,
! [X0: $i] : join(converse(X0),iPr_def_12) = converse(join(X0,sK1)),
inference(superposition,[status(thm)],[c_246,c_56]) ).
tcf(c_309,plain,
! [X0: $i] : join(converse(X0),iPr_def_19) = converse(join(X0,iPr_def_20)),
inference(superposition,[status(thm)],[c_244,c_56]) ).
tcf(c_312,plain,
! [X0: $i] : join(iPr_def_19,converse(X0)) = converse(join(X0,iPr_def_20)),
inference(theory_normalisation,[status(thm)],[c_309,c_50,c_49]) ).
tcf(c_316,plain,
! [X0: $i] : join(iPr_def_12,converse(X0)) = converse(join(X0,sK1)),
inference(theory_normalisation,[status(thm)],[c_303,c_50,c_49]) ).
tcf(c_317,plain,
! [X0: $i] : join(iPr_def_10,converse(X0)) = converse(join(X0,sK0)),
inference(theory_normalisation,[status(thm)],[c_301,c_50,c_49]) ).
tcf(c_328,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_55,c_57]) ).
tcf(c_329,plain,
! [X0: $i] : composition(converse(X0),iPr_def_10) = converse(composition(sK0,X0)),
inference(superposition,[status(thm)],[c_245,c_57]) ).
tcf(c_331,plain,
! [X0: $i] : composition(converse(X0),iPr_def_12) = converse(composition(sK1,X0)),
inference(superposition,[status(thm)],[c_246,c_57]) ).
tcf(c_335,plain,
! [X0: $i] : composition(converse(X0),sK0) = converse(composition(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_242,c_57]) ).
tcf(c_336,plain,
! [X0: $i] : composition(converse(X0),sK1) = converse(composition(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_243,c_57]) ).
tcf(c_344,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_13,X0)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_115,c_50]) ).
tcf(c_345,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_17,X0)) = join(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_119,c_50]) ).
tcf(c_346,plain,
! [X0: $i] : join(top,join(zero,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_253,c_50]) ).
tcf(c_347,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_11,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_254,c_50]) ).
tcf(c_349,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_13,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_255,c_50]) ).
tcf(c_353,plain,
! [X0: $i] : join(iPr_def_16,join(sK0,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_261,c_50]) ).
tcf(c_405,plain,
join(sK0,converse(iPr_def_11)) = converse(top),
inference(superposition,[status(thm)],[c_254,c_297]) ).
tcf(c_440,plain,
! [X0: $i] : join(iPr_def_16,join(X0,iPr_def_17)) = join(X0,iPr_def_18),
inference(superposition,[status(thm)],[c_119,c_209]) ).
tcf(c_442,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_11)) = join(X0,top),
inference(superposition,[status(thm)],[c_254,c_209]) ).
tcf(c_462,plain,
! [X0: $i,X1: $i] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_722,plain,
join(complement(join(iPr_def_16,iPr_def_16)),complement(top)) = sK0,
inference(superposition,[status(thm)],[c_59,c_217]) ).
tcf(c_724,plain,
join(complement(join(iPr_def_16,sK1)),complement(join(iPr_def_16,iPr_def_17))) = sK0,
inference(superposition,[status(thm)],[c_118,c_217]) ).
tcf(c_735,plain,
join(complement(top),complement(join(iPr_def_16,iPr_def_16))) = sK0,
inference(theory_normalisation,[status(thm)],[c_722,c_50,c_49]) ).
tcf(c_736,plain,
join(zero,complement(join(iPr_def_16,iPr_def_16))) = sK0,
inference(light_normalisation,[status(thm)],[c_735,c_104]) ).
tcf(c_742,plain,
join(complement(join(iPr_def_16,iPr_def_17)),complement(join(iPr_def_16,sK1))) = sK0,
inference(theory_normalisation,[status(thm)],[c_724,c_50,c_49]) ).
tcf(c_743,plain,
join(iPr_def_19,complement(join(iPr_def_16,sK1))) = sK0,
inference(light_normalisation,[status(thm)],[c_742,c_119,c_120]) ).
tcf(c_765,plain,
join(iPr_def_20,converse(complement(join(iPr_def_16,sK1)))) = converse(sK0),
inference(superposition,[status(thm)],[c_743,c_295]) ).
tcf(c_766,plain,
join(iPr_def_20,converse(complement(join(iPr_def_16,sK1)))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_765,c_245]) ).
tcf(c_812,plain,
composition(converse(one),iPr_def_10) = converse(sK0),
inference(superposition,[status(thm)],[c_53,c_329]) ).
tcf(c_825,plain,
composition(converse(one),iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_812,c_245]) ).
tcf(c_835,plain,
join(complement(iPr_def_10),composition(converse(converse(one)),complement(iPr_def_10))) = complement(iPr_def_10),
inference(superposition,[status(thm)],[c_825,c_75]) ).
tcf(c_838,plain,
join(iPr_def_11,composition(converse(converse(one)),iPr_def_11)) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_835,c_112]) ).
tcf(c_847,plain,
composition(converse(one),iPr_def_12) = converse(sK1),
inference(superposition,[status(thm)],[c_53,c_331]) ).
tcf(c_860,plain,
composition(converse(one),iPr_def_12) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_847,c_246]) ).
tcf(c_882,plain,
join(complement(iPr_def_12),composition(converse(converse(one)),complement(iPr_def_12))) = complement(iPr_def_12),
inference(superposition,[status(thm)],[c_860,c_75]) ).
tcf(c_885,plain,
join(iPr_def_13,composition(converse(converse(one)),iPr_def_13)) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_882,c_114]) ).
tcf(c_928,plain,
composition(converse(one),sK0) = converse(iPr_def_10),
inference(superposition,[status(thm)],[c_53,c_335]) ).
tcf(c_941,plain,
composition(converse(one),sK0) = sK0,
inference(light_normalisation,[status(thm)],[c_928,c_242]) ).
tcf(c_989,plain,
join(complement(sK0),composition(converse(converse(one)),complement(sK0))) = complement(sK0),
inference(superposition,[status(thm)],[c_941,c_75]) ).
tcf(c_992,plain,
join(iPr_def_16,composition(converse(converse(one)),iPr_def_16)) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_989,c_117]) ).
tcf(c_1009,plain,
composition(converse(one),sK1) = converse(iPr_def_12),
inference(superposition,[status(thm)],[c_53,c_336]) ).
tcf(c_1022,plain,
composition(converse(one),sK1) = sK1,
inference(light_normalisation,[status(thm)],[c_1009,c_243]) ).
tcf(c_1032,plain,
join(complement(sK1),composition(converse(converse(one)),complement(sK1))) = complement(sK1),
inference(superposition,[status(thm)],[c_1022,c_75]) ).
tcf(c_1035,plain,
join(iPr_def_17,composition(converse(converse(one)),iPr_def_17)) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_1032,c_118]) ).
tcf(c_1126,plain,
join(top,complement(zero)) = join(top,top),
inference(superposition,[status(thm)],[c_59,c_346]) ).
tcf(c_1191,plain,
join(top,iPr_def_13) = join(iPr_def_10,iPr_def_14),
inference(superposition,[status(thm)],[c_115,c_347]) ).
tcf(c_1198,plain,
join(iPr_def_10,iPr_def_14) = join(iPr_def_13,top),
inference(theory_normalisation,[status(thm)],[c_1191,c_50,c_49]) ).
tcf(c_1287,plain,
join(top,converse(iPr_def_11)) = join(iPr_def_16,converse(top)),
inference(superposition,[status(thm)],[c_405,c_353]) ).
tcf(c_1396,plain,
join(top,iPr_def_17) = join(sK0,iPr_def_18),
inference(superposition,[status(thm)],[c_440,c_353]) ).
tcf(c_1397,plain,
join(iPr_def_17,top) = join(iPr_def_18,sK0),
inference(theory_normalisation,[status(thm)],[c_1396,c_50,c_49]) ).
tcf(c_1431,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_11,X0)) = join(X0,top),
inference(superposition,[status(thm)],[c_49,c_442]) ).
tcf(c_1580,plain,
join(complement(join(iPr_def_15,iPr_def_15)),complement(top)) = iPr_def_14,
inference(superposition,[status(thm)],[c_59,c_221]) ).
tcf(c_1595,plain,
join(complement(top),complement(join(iPr_def_15,iPr_def_15))) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_1580,c_50,c_49]) ).
tcf(c_1596,plain,
join(zero,complement(join(iPr_def_15,iPr_def_15))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_1595,c_104]) ).
tcf(c_1752,plain,
join(iPr_def_11,composition(one,iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_838,c_55]) ).
tcf(c_1756,plain,
join(top,composition(one,iPr_def_11)) = join(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_1752,c_347]) ).
tcf(c_1758,plain,
join(top,composition(one,iPr_def_11)) = top,
inference(light_normalisation,[status(thm)],[c_1756,c_254]) ).
tcf(c_1763,plain,
join(iPr_def_13,composition(one,iPr_def_13)) = iPr_def_13,
inference(demodulation,[status(thm)],[c_885,c_55]) ).
tcf(c_1768,plain,
join(top,composition(one,iPr_def_13)) = join(iPr_def_12,iPr_def_13),
inference(superposition,[status(thm)],[c_1763,c_349]) ).
tcf(c_1769,plain,
join(iPr_def_14,composition(one,iPr_def_13)) = join(iPr_def_11,iPr_def_13),
inference(superposition,[status(thm)],[c_1763,c_344]) ).
tcf(c_1770,plain,
join(iPr_def_14,composition(one,iPr_def_13)) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_1769,c_115]) ).
tcf(c_1771,plain,
join(top,composition(one,iPr_def_13)) = top,
inference(light_normalisation,[status(thm)],[c_1768,c_255]) ).
tcf(c_1780,plain,
join(iPr_def_16,composition(one,iPr_def_16)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_992,c_55]) ).
tcf(c_1839,plain,
join(iPr_def_17,composition(one,iPr_def_17)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_1035,c_55]) ).
tcf(c_1843,plain,
join(iPr_def_18,composition(one,iPr_def_17)) = join(iPr_def_16,iPr_def_17),
inference(superposition,[status(thm)],[c_1839,c_345]) ).
tcf(c_1844,plain,
join(iPr_def_18,composition(one,iPr_def_17)) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_1843,c_119]) ).
tcf(c_2451,plain,
join(zero,complement(join(iPr_def_17,iPr_def_17))) = sK1,
inference(superposition,[status(thm)],[c_118,c_263]) ).
tcf(c_2456,plain,
join(zero,complement(join(iPr_def_19,iPr_def_19))) = iPr_def_18,
inference(superposition,[status(thm)],[c_120,c_263]) ).
tcf(c_2501,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[status(thm)],[c_59,c_290]) ).
tcf(c_2952,plain,
join(complement(join(top,complement(zero))),complement(top)) = zero,
inference(superposition,[status(thm)],[c_59,c_232]) ).
tcf(c_2978,plain,
join(complement(top),complement(join(top,complement(zero)))) = zero,
inference(theory_normalisation,[status(thm)],[c_2952,c_50,c_49]) ).
tcf(c_2979,plain,
join(zero,complement(join(top,top))) = zero,
inference(light_normalisation,[status(thm)],[c_2978,c_104,c_1126]) ).
tcf(c_3023,plain,
join(top,complement(join(top,top))) = join(top,zero),
inference(superposition,[status(thm)],[c_2979,c_346]) ).
tcf(c_3027,plain,
join(top,complement(join(top,top))) = top,
inference(light_normalisation,[status(thm)],[c_3023,c_253]) ).
tcf(c_3041,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_53,c_328]) ).
tcf(c_3115,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(light_normalisation,[status(thm)],[c_3041,c_55]) ).
tcf(c_3146,plain,
converse(one) = one,
inference(superposition,[status(thm)],[c_3115,c_53]) ).
tcf(c_3159,plain,
! [X0: $i] : composition(converse(one),X0) = composition(one,X0),
inference(superposition,[status(thm)],[c_3115,c_462]) ).
tcf(c_3161,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(light_normalisation,[status(thm)],[c_3159,c_3115]) ).
tcf(c_3166,plain,
join(top,iPr_def_11) = top,
inference(demodulation,[status(thm)],[c_1758,c_3161]) ).
tcf(c_3167,plain,
join(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_1752,c_3161]) ).
tcf(c_3168,plain,
join(top,iPr_def_13) = top,
inference(demodulation,[status(thm)],[c_1771,c_3161]) ).
tcf(c_3169,plain,
join(iPr_def_14,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_1770,c_3161]) ).
tcf(c_3171,plain,
join(iPr_def_16,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_1780,c_3161]) ).
tcf(c_3172,plain,
join(iPr_def_18,iPr_def_17) = iPr_def_18,
inference(demodulation,[status(thm)],[c_1844,c_3161]) ).
tcf(c_3173,plain,
join(iPr_def_17,iPr_def_17) = iPr_def_17,
inference(demodulation,[status(thm)],[c_1839,c_3161]) ).
tcf(c_3174,plain,
join(zero,complement(iPr_def_17)) = sK1,
inference(demodulation,[status(thm)],[c_2451,c_3173]) ).
tcf(c_3175,plain,
join(iPr_def_17,iPr_def_18) = iPr_def_18,
inference(theory_normalisation,[status(thm)],[c_3172,c_50,c_49]) ).
tcf(c_3176,plain,
join(zero,complement(iPr_def_16)) = sK0,
inference(demodulation,[status(thm)],[c_736,c_3171]) ).
tcf(c_3178,plain,
join(iPr_def_13,iPr_def_14) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_3169,c_50,c_49]) ).
tcf(c_3179,plain,
join(iPr_def_13,top) = top,
inference(theory_normalisation,[status(thm)],[c_3168,c_50,c_49]) ).
tcf(c_3180,plain,
join(iPr_def_10,iPr_def_14) = top,
inference(demodulation,[status(thm)],[c_1198,c_3179]) ).
tcf(c_3182,plain,
join(iPr_def_11,top) = top,
inference(theory_normalisation,[status(thm)],[c_3166,c_50,c_49]) ).
tcf(c_3202,plain,
! [X0: $i,X1: $i] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(superposition,[status(thm)],[c_3161,c_54]) ).
tcf(c_3222,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_11,X0)) = join(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_3167,c_50]) ).
tcf(c_3257,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_16,X0)) = join(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_3171,c_50]) ).
tcf(c_3261,plain,
! [X0: $i] : join(iPr_def_17,join(iPr_def_17,X0)) = join(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_3173,c_50]) ).
tcf(c_3281,plain,
join(complement(iPr_def_14),complement(join(iPr_def_13,complement(iPr_def_14)))) = iPr_def_12,
inference(superposition,[status(thm)],[c_3178,c_220]) ).
tcf(c_3283,plain,
join(iPr_def_11,iPr_def_14) = join(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_3178,c_344]) ).
tcf(c_3286,plain,
join(iPr_def_15,complement(join(iPr_def_13,iPr_def_15))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_3281,c_116]) ).
tcf(c_3294,plain,
join(top,top) = join(iPr_def_12,top),
inference(superposition,[status(thm)],[c_3179,c_349]) ).
tcf(c_3300,plain,
join(zero,complement(join(iPr_def_12,top))) = zero,
inference(demodulation,[status(thm)],[c_2979,c_3294]) ).
tcf(c_3302,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_14,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_3180,c_50]) ).
tcf(c_3309,plain,
join(top,top) = join(iPr_def_10,top),
inference(superposition,[status(thm)],[c_3182,c_1431]) ).
tcf(c_3331,plain,
join(complement(join(iPr_def_16,iPr_def_17)),complement(join(sK0,iPr_def_17))) = sK1,
inference(superposition,[status(thm)],[c_118,c_233]) ).
tcf(c_3351,plain,
join(complement(join(iPr_def_16,iPr_def_17)),complement(join(iPr_def_17,sK0))) = sK1,
inference(theory_normalisation,[status(thm)],[c_3331,c_50,c_49]) ).
tcf(c_3352,plain,
join(iPr_def_19,complement(join(iPr_def_17,sK0))) = sK1,
inference(light_normalisation,[status(thm)],[c_3351,c_119,c_120]) ).
tcf(c_3372,plain,
join(iPr_def_20,converse(complement(join(iPr_def_17,sK0)))) = converse(sK1),
inference(superposition,[status(thm)],[c_3352,c_295]) ).
tcf(c_3373,plain,
join(iPr_def_20,converse(complement(join(iPr_def_17,sK0)))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_3372,c_246]) ).
tcf(c_3489,plain,
join(iPr_def_11,iPr_def_14) = iPr_def_14,
inference(superposition,[status(thm)],[c_115,c_3222]) ).
tcf(c_3495,plain,
join(iPr_def_11,converse(top)) = converse(top),
inference(superposition,[status(thm)],[c_2501,c_3222]) ).
tcf(c_3519,plain,
join(complement(iPr_def_14),complement(join(iPr_def_11,complement(iPr_def_14)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_3489,c_219]) ).
tcf(c_3522,plain,
join(iPr_def_15,complement(join(iPr_def_11,iPr_def_15))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_3519,c_116]) ).
tcf(c_3611,plain,
join(iPr_def_14,iPr_def_14) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_3283,c_3489]) ).
tcf(c_3765,plain,
join(iPr_def_16,iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_119,c_3257]) ).
tcf(c_3776,plain,
join(iPr_def_16,converse(top)) = converse(top),
inference(superposition,[status(thm)],[c_2501,c_3257]) ).
tcf(c_3800,plain,
join(top,converse(iPr_def_11)) = converse(top),
inference(demodulation,[status(thm)],[c_1287,c_3776]) ).
tcf(c_3804,plain,
join(complement(iPr_def_18),complement(join(iPr_def_16,complement(iPr_def_18)))) = sK0,
inference(superposition,[status(thm)],[c_3765,c_217]) ).
tcf(c_3805,plain,
join(iPr_def_19,complement(join(iPr_def_16,iPr_def_19))) = sK0,
inference(light_normalisation,[status(thm)],[c_3804,c_120]) ).
tcf(c_3814,plain,
join(iPr_def_17,top) = top,
inference(superposition,[status(thm)],[c_260,c_3261]) ).
tcf(c_3838,plain,
join(iPr_def_18,sK0) = top,
inference(demodulation,[status(thm)],[c_1397,c_3814]) ).
tcf(c_3885,plain,
join(iPr_def_10,top) = join(iPr_def_12,top),
inference(light_normalisation,[status(thm)],[c_3294,c_3309]) ).
tcf(c_3916,plain,
join(converse(iPr_def_11),top) = converse(converse(top)),
inference(superposition,[status(thm)],[c_3495,c_300]) ).
tcf(c_3917,plain,
join(top,converse(iPr_def_11)) = converse(converse(top)),
inference(theory_normalisation,[status(thm)],[c_3916,c_50,c_49]) ).
tcf(c_3918,plain,
converse(converse(top)) = converse(top),
inference(light_normalisation,[status(thm)],[c_3917,c_3800]) ).
tcf(c_3933,plain,
join(complement(iPr_def_18),complement(join(iPr_def_17,complement(iPr_def_18)))) = sK1,
inference(superposition,[status(thm)],[c_3175,c_236]) ).
tcf(c_3954,plain,
join(iPr_def_19,complement(join(iPr_def_17,iPr_def_19))) = sK1,
inference(light_normalisation,[status(thm)],[c_3933,c_120]) ).
tcf(c_4082,plain,
join(top,iPr_def_15) = join(iPr_def_10,top),
inference(superposition,[status(thm)],[c_256,c_3302]) ).
tcf(c_4103,plain,
join(iPr_def_10,top) = join(iPr_def_15,top),
inference(theory_normalisation,[status(thm)],[c_4082,c_50,c_49]) ).
tcf(c_4115,plain,
converse(top) = top,
inference(demodulation,[status(thm)],[c_3918,c_55]) ).
tcf(c_4119,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = top,
inference(demodulation,[status(thm)],[c_2501,c_4115]) ).
tcf(c_4667,plain,
join(top,complement(join(iPr_def_10,top))) = top,
inference(light_normalisation,[status(thm)],[c_3027,c_3309]) ).
tcf(c_4720,plain,
join(zero,complement(join(iPr_def_10,top))) = zero,
inference(light_normalisation,[status(thm)],[c_3300,c_3885]) ).
tcf(c_4727,plain,
join(complement(join(top,complement(join(iPr_def_10,top)))),complement(zero)) = join(iPr_def_10,top),
inference(superposition,[status(thm)],[c_4720,c_232]) ).
tcf(c_4734,plain,
join(complement(zero),complement(join(top,complement(join(iPr_def_10,top))))) = join(iPr_def_10,top),
inference(theory_normalisation,[status(thm)],[c_4727,c_50,c_49]) ).
tcf(c_4735,plain,
join(complement(zero),zero) = join(iPr_def_10,top),
inference(light_normalisation,[status(thm)],[c_4734,c_104,c_4667]) ).
tcf(c_4736,plain,
join(zero,complement(zero)) = join(iPr_def_10,top),
inference(theory_normalisation,[status(thm)],[c_4735,c_50,c_49]) ).
tcf(c_6128,plain,
join(iPr_def_10,top) = top,
inference(demodulation,[status(thm)],[c_4736,c_59]) ).
tcf(c_6137,plain,
join(zero,complement(top)) = zero,
inference(demodulation,[status(thm)],[c_4720,c_6128]) ).
tcf(c_6139,plain,
join(iPr_def_15,top) = top,
inference(demodulation,[status(thm)],[c_4103,c_6128]) ).
tcf(c_6141,plain,
join(iPr_def_12,top) = top,
inference(demodulation,[status(thm)],[c_3885,c_6128]) ).
tcf(c_6144,plain,
join(zero,zero) = zero,
inference(light_normalisation,[status(thm)],[c_6137,c_104]) ).
tcf(c_6227,plain,
! [X0: $i] : join(zero,join(zero,X0)) = join(zero,X0),
inference(superposition,[status(thm)],[c_6144,c_50]) ).
tcf(c_7123,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(superposition,[status(thm)],[c_263,c_6227]) ).
tcf(c_7156,plain,
! [X0: $i] : complement(join(complement(X0),complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_263,c_7123]) ).
tcf(c_7159,plain,
complement(iPr_def_16) = sK0,
inference(demodulation,[status(thm)],[c_3176,c_7123]) ).
tcf(c_7160,plain,
complement(iPr_def_17) = sK1,
inference(demodulation,[status(thm)],[c_3174,c_7123]) ).
tcf(c_7163,plain,
complement(join(iPr_def_15,iPr_def_15)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_1596,c_7123]) ).
tcf(c_7167,plain,
complement(join(iPr_def_19,iPr_def_19)) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2456,c_7123]) ).
tcf(c_7347,plain,
! [X0: $i] : join(X0,zero) = X0,
inference(superposition,[status(thm)],[c_7123,c_49]) ).
tcf(c_7352,plain,
complement(zero) = top,
inference(superposition,[status(thm)],[c_7123,c_59]) ).
tcf(c_7368,plain,
join(iPr_def_19,converse(zero)) = converse(iPr_def_20),
inference(superposition,[status(thm)],[c_7123,c_312]) ).
tcf(c_7383,plain,
converse(complement(converse(zero))) = top,
inference(superposition,[status(thm)],[c_7123,c_4119]) ).
tcf(c_7396,plain,
join(iPr_def_19,converse(zero)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_7368,c_244]) ).
tcf(c_7432,plain,
! [X0: $i] : join(complement(join(top,X0)),complement(join(top,complement(X0)))) = zero,
inference(superposition,[status(thm)],[c_7352,c_74]) ).
tcf(c_7485,plain,
join(complement(iPr_def_15),complement(join(iPr_def_15,complement(zero)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_7347,c_221]) ).
tcf(c_7546,plain,
join(complement(iPr_def_15),zero) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_7485,c_104,c_6139,c_7352]) ).
tcf(c_7547,plain,
join(zero,complement(iPr_def_15)) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_7546,c_50,c_49]) ).
tcf(c_7562,plain,
join(complement(join(iPr_def_14,iPr_def_14)),complement(join(iPr_def_15,iPr_def_14))) = join(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_7163,c_229]) ).
tcf(c_7583,plain,
join(complement(join(iPr_def_14,iPr_def_14)),complement(join(iPr_def_14,iPr_def_15))) = join(iPr_def_15,iPr_def_15),
inference(theory_normalisation,[status(thm)],[c_7562,c_50,c_49]) ).
tcf(c_7584,plain,
join(iPr_def_15,zero) = join(iPr_def_15,iPr_def_15),
inference(light_normalisation,[status(thm)],[c_7583,c_104,c_116,c_256,c_3611]) ).
tcf(c_7624,plain,
join(complement(join(iPr_def_16,iPr_def_18)),complement(join(sK0,iPr_def_18))) = join(iPr_def_19,iPr_def_19),
inference(superposition,[status(thm)],[c_7167,c_233]) ).
tcf(c_7646,plain,
join(complement(join(iPr_def_16,iPr_def_18)),complement(join(iPr_def_18,sK0))) = join(iPr_def_19,iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_7624,c_50,c_49]) ).
tcf(c_7647,plain,
join(iPr_def_19,zero) = join(iPr_def_19,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_7646,c_104,c_120,c_3765,c_3838]) ).
tcf(c_7668,plain,
complement(converse(zero)) = converse(top),
inference(superposition,[status(thm)],[c_7383,c_55]) ).
tcf(c_7675,plain,
complement(converse(zero)) = top,
inference(light_normalisation,[status(thm)],[c_7668,c_4115]) ).
tcf(c_7778,plain,
! [X0: $i] : join(complement(join(top,X0)),complement(join(top,complement(X0)))) = converse(zero),
inference(superposition,[status(thm)],[c_7675,c_74]) ).
tcf(c_7803,plain,
converse(zero) = zero,
inference(light_normalisation,[status(thm)],[c_7778,c_7432]) ).
tcf(c_7830,plain,
join(iPr_def_19,iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_7396,c_7647,c_7803]) ).
tcf(c_7831,plain,
complement(iPr_def_19) = iPr_def_18,
inference(demodulation,[status(thm)],[c_7167,c_7830]) ).
tcf(c_7836,plain,
! [X0: $i] : join(iPr_def_19,join(iPr_def_19,X0)) = join(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_7830,c_50]) ).
tcf(c_8045,plain,
join(iPr_def_19,sK0) = sK0,
inference(superposition,[status(thm)],[c_3805,c_7836]) ).
tcf(c_8046,plain,
join(iPr_def_19,sK1) = sK1,
inference(superposition,[status(thm)],[c_3954,c_7836]) ).
tcf(c_8070,plain,
join(iPr_def_10,converse(iPr_def_19)) = converse(sK0),
inference(superposition,[status(thm)],[c_8045,c_317]) ).
tcf(c_8071,plain,
join(iPr_def_10,iPr_def_20) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_8070,c_245,c_247]) ).
tcf(c_8093,plain,
join(iPr_def_12,converse(iPr_def_19)) = converse(sK1),
inference(superposition,[status(thm)],[c_8046,c_316]) ).
tcf(c_8094,plain,
join(iPr_def_12,iPr_def_20) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_8093,c_246,c_247]) ).
tcf(c_8112,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_20,X0)) = join(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_8071,c_50]) ).
tcf(c_8120,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_20,X0)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_8094,c_50]) ).
tcf(c_8130,plain,
complement(iPr_def_15) = iPr_def_14,
inference(demodulation,[status(thm)],[c_7547,c_7123]) ).
tcf(c_8142,plain,
join(complement(join(iPr_def_14,iPr_def_14)),complement(join(iPr_def_15,iPr_def_14))) = iPr_def_15,
inference(superposition,[status(thm)],[c_8130,c_229]) ).
tcf(c_8162,plain,
join(complement(join(iPr_def_14,iPr_def_14)),complement(join(iPr_def_14,iPr_def_15))) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_8142,c_50,c_49]) ).
tcf(c_8163,plain,
join(iPr_def_15,iPr_def_15) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_8162,c_104,c_116,c_256,c_3611,c_7584]) ).
tcf(c_8175,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_15,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_8163,c_50]) ).
tcf(c_8291,plain,
! [X0: $i] : join(complement(X0),complement(composition(converse(one),X0))) = complement(X0),
inference(superposition,[status(thm)],[c_3161,c_272]) ).
tcf(c_8347,plain,
! [X0: $i] : join(complement(X0),complement(X0)) = complement(X0),
inference(light_normalisation,[status(thm)],[c_8291,c_3146,c_3161]) ).
tcf(c_8630,plain,
join(iPr_def_10,complement(iPr_def_20)) = join(iPr_def_10,top),
inference(superposition,[status(thm)],[c_59,c_8112]) ).
tcf(c_8654,plain,
join(iPr_def_10,complement(iPr_def_20)) = top,
inference(light_normalisation,[status(thm)],[c_8630,c_6128]) ).
tcf(c_8667,plain,
join(iPr_def_12,complement(iPr_def_20)) = join(iPr_def_12,top),
inference(superposition,[status(thm)],[c_59,c_8120]) ).
tcf(c_8691,plain,
join(iPr_def_12,complement(iPr_def_20)) = top,
inference(light_normalisation,[status(thm)],[c_8667,c_6141]) ).
tcf(c_8708,plain,
join(iPr_def_15,iPr_def_12) = iPr_def_12,
inference(superposition,[status(thm)],[c_3286,c_8175]) ).
tcf(c_8709,plain,
join(iPr_def_15,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_3522,c_8175]) ).
tcf(c_8716,plain,
join(iPr_def_10,iPr_def_15) = iPr_def_10,
inference(theory_normalisation,[status(thm)],[c_8709,c_50,c_49]) ).
tcf(c_8717,plain,
join(iPr_def_12,iPr_def_15) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_8708,c_50,c_49]) ).
tcf(c_8812,plain,
join(complement(top),complement(join(iPr_def_11,complement(iPr_def_20)))) = iPr_def_20,
inference(superposition,[status(thm)],[c_8654,c_231]) ).
tcf(c_8815,plain,
join(zero,complement(join(iPr_def_11,complement(iPr_def_20)))) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_8812,c_104]) ).
tcf(c_8819,plain,
join(complement(top),complement(join(iPr_def_13,complement(iPr_def_20)))) = iPr_def_20,
inference(superposition,[status(thm)],[c_8691,c_230]) ).
tcf(c_8823,plain,
join(zero,complement(join(iPr_def_13,complement(iPr_def_20)))) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_8819,c_104]) ).
tcf(c_9348,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_7156,c_8347]) ).
tcf(c_9360,plain,
complement(iPr_def_18) = iPr_def_19,
inference(superposition,[status(thm)],[c_7831,c_9348]) ).
tcf(c_9361,plain,
complement(sK0) = iPr_def_16,
inference(superposition,[status(thm)],[c_7159,c_9348]) ).
tcf(c_9362,plain,
complement(sK1) = iPr_def_17,
inference(superposition,[status(thm)],[c_7160,c_9348]) ).
tcf(c_9955,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(superposition,[status(thm)],[c_9348,c_8347]) ).
tcf(c_9985,plain,
! [X0: $i,X1: $i] : join(X0,join(X0,X1)) = join(X0,X1),
inference(superposition,[status(thm)],[c_9955,c_50]) ).
tcf(c_12829,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[status(thm)],[c_286,c_9985]) ).
tcf(c_12837,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(theory_normalisation,[status(thm)],[c_12829,c_50,c_49]) ).
tcf(c_19941,plain,
complement(join(iPr_def_11,complement(iPr_def_20))) = iPr_def_20,
inference(demodulation,[status(thm)],[c_8815,c_7123]) ).
tcf(c_19952,plain,
join(iPr_def_11,complement(iPr_def_20)) = complement(iPr_def_20),
inference(superposition,[status(thm)],[c_19941,c_9348]) ).
tcf(c_19974,plain,
complement(join(iPr_def_13,complement(iPr_def_20))) = iPr_def_20,
inference(demodulation,[status(thm)],[c_8823,c_7123]) ).
tcf(c_19985,plain,
join(iPr_def_13,complement(iPr_def_20)) = complement(iPr_def_20),
inference(superposition,[status(thm)],[c_19974,c_9348]) ).
tcf(c_20007,plain,
join(iPr_def_11,complement(iPr_def_20)) = join(iPr_def_14,complement(iPr_def_20)),
inference(superposition,[status(thm)],[c_19985,c_344]) ).
tcf(c_20009,plain,
join(iPr_def_14,complement(iPr_def_20)) = complement(iPr_def_20),
inference(light_normalisation,[status(thm)],[c_20007,c_19952]) ).
tcf(c_24010,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(X0,X1))) = complement(X0),
inference(superposition,[status(thm)],[c_9348,c_12837]) ).
tcf(c_24022,plain,
! [X0: $i] : join(iPr_def_18,complement(join(iPr_def_19,X0))) = iPr_def_18,
inference(superposition,[status(thm)],[c_9360,c_12837]) ).
tcf(c_24030,plain,
! [X0: $i] : join(iPr_def_15,complement(join(iPr_def_14,X0))) = iPr_def_15,
inference(superposition,[status(thm)],[c_8130,c_12837]) ).
tcf(c_24057,plain,
! [X0: $i] : join(iPr_def_20,converse(complement(join(complement(iPr_def_19),X0)))) = converse(iPr_def_19),
inference(superposition,[status(thm)],[c_12837,c_295]) ).
tcf(c_24136,plain,
! [X0: $i] : join(iPr_def_20,converse(complement(join(iPr_def_18,X0)))) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_24057,c_247,c_7831]) ).
tcf(c_24922,plain,
join(iPr_def_15,complement(complement(iPr_def_20))) = iPr_def_15,
inference(superposition,[status(thm)],[c_20009,c_24030]) ).
tcf(c_24953,plain,
join(iPr_def_15,iPr_def_20) = iPr_def_15,
inference(demodulation,[status(thm)],[c_24922,c_9348]) ).
tcf(c_24956,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_20,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_24953,c_50]) ).
tcf(c_24967,plain,
join(iPr_def_19,converse(iPr_def_15)) = converse(iPr_def_15),
inference(superposition,[status(thm)],[c_24953,c_312]) ).
tcf(c_24980,plain,
join(iPr_def_18,complement(converse(iPr_def_15))) = iPr_def_18,
inference(superposition,[status(thm)],[c_24967,c_24022]) ).
tcf(c_25957,plain,
join(iPr_def_15,converse(complement(join(iPr_def_16,sK1)))) = join(iPr_def_15,iPr_def_10),
inference(superposition,[status(thm)],[c_766,c_24956]) ).
tcf(c_25959,plain,
join(iPr_def_15,converse(complement(join(iPr_def_17,sK0)))) = join(iPr_def_15,iPr_def_12),
inference(superposition,[status(thm)],[c_3373,c_24956]) ).
tcf(c_26058,plain,
join(iPr_def_15,converse(complement(join(iPr_def_17,sK0)))) = join(iPr_def_12,iPr_def_15),
inference(theory_normalisation,[status(thm)],[c_25959,c_50,c_49]) ).
tcf(c_26059,plain,
join(iPr_def_15,converse(complement(join(iPr_def_17,sK0)))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_26058,c_8717]) ).
tcf(c_26060,plain,
join(iPr_def_15,converse(complement(join(iPr_def_16,sK1)))) = join(iPr_def_10,iPr_def_15),
inference(theory_normalisation,[status(thm)],[c_25957,c_50,c_49]) ).
tcf(c_26061,plain,
join(iPr_def_15,converse(complement(join(iPr_def_16,sK1)))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_26060,c_8716]) ).
tcf(c_33186,plain,
! [X0: $i] : join(iPr_def_15,converse(complement(join(iPr_def_18,X0)))) = join(iPr_def_15,iPr_def_20),
inference(superposition,[status(thm)],[c_24136,c_24956]) ).
tcf(c_33207,plain,
! [X0: $i] : join(iPr_def_15,converse(complement(join(iPr_def_18,X0)))) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_33186,c_24953]) ).
tcf(c_34300,plain,
join(converse(iPr_def_15),complement(join(iPr_def_17,sK0))) = converse(iPr_def_12),
inference(superposition,[status(thm)],[c_26059,c_300]) ).
tcf(c_34303,plain,
join(converse(iPr_def_15),complement(join(iPr_def_17,sK0))) = sK1,
inference(light_normalisation,[status(thm)],[c_34300,c_243]) ).
tcf(c_34327,plain,
join(converse(iPr_def_15),complement(join(iPr_def_16,sK1))) = converse(iPr_def_10),
inference(superposition,[status(thm)],[c_26061,c_300]) ).
tcf(c_34330,plain,
join(converse(iPr_def_15),complement(join(iPr_def_16,sK1))) = sK0,
inference(light_normalisation,[status(thm)],[c_34327,c_242]) ).
tcf(c_41287,plain,
! [X0: $i] : join(X0,composition(complement(one),X0)) = composition(top,X0),
inference(superposition,[status(thm)],[c_59,c_3202]) ).
tcf(c_41543,plain,
join(iPr_def_15,converse(complement(composition(top,iPr_def_18)))) = iPr_def_15,
inference(superposition,[status(thm)],[c_41287,c_33207]) ).
tcf(c_41546,plain,
join(iPr_def_20,converse(complement(composition(top,iPr_def_18)))) = iPr_def_20,
inference(superposition,[status(thm)],[c_41287,c_24136]) ).
tcf(c_114370,plain,
join(complement(converse(iPr_def_15)),complement(sK1)) = complement(converse(iPr_def_15)),
inference(superposition,[status(thm)],[c_34303,c_24010]) ).
tcf(c_114371,plain,
join(complement(converse(iPr_def_15)),complement(sK0)) = complement(converse(iPr_def_15)),
inference(superposition,[status(thm)],[c_34330,c_24010]) ).
tcf(c_114796,plain,
join(complement(sK0),complement(converse(iPr_def_15))) = complement(converse(iPr_def_15)),
inference(theory_normalisation,[status(thm)],[c_114371,c_50,c_49]) ).
tcf(c_114797,plain,
join(iPr_def_16,complement(converse(iPr_def_15))) = complement(converse(iPr_def_15)),
inference(light_normalisation,[status(thm)],[c_114796,c_9361]) ).
tcf(c_114798,plain,
join(complement(sK1),complement(converse(iPr_def_15))) = complement(converse(iPr_def_15)),
inference(theory_normalisation,[status(thm)],[c_114370,c_50,c_49]) ).
tcf(c_114799,plain,
join(iPr_def_17,complement(converse(iPr_def_15))) = complement(converse(iPr_def_15)),
inference(light_normalisation,[status(thm)],[c_114798,c_9362]) ).
tcf(c_114943,plain,
join(iPr_def_16,complement(converse(iPr_def_15))) = join(iPr_def_18,complement(converse(iPr_def_15))),
inference(superposition,[status(thm)],[c_114799,c_345]) ).
tcf(c_114957,plain,
complement(converse(iPr_def_15)) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_114943,c_24980,c_114797]) ).
tcf(c_115017,plain,
complement(iPr_def_18) = converse(iPr_def_15),
inference(superposition,[status(thm)],[c_114957,c_9348]) ).
tcf(c_115030,plain,
converse(iPr_def_15) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_115017,c_9360]) ).
tcf(c_115135,plain,
! [X0: $i] : join(iPr_def_15,converse(X0)) = converse(join(iPr_def_19,X0)),
inference(superposition,[status(thm)],[c_115030,c_290]) ).
tcf(c_115253,plain,
! [X0: $i] : join(iPr_def_15,converse(X0)) = join(iPr_def_20,converse(X0)),
inference(demodulation,[status(thm)],[c_295,c_115135]) ).
tcf(c_115274,plain,
join(iPr_def_15,converse(complement(composition(top,iPr_def_18)))) = iPr_def_20,
inference(demodulation,[status(thm)],[c_41546,c_115253]) ).
tcf(c_115275,plain,
iPr_def_15 = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_115274,c_41543]) ).
tcf(c_115276,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_115275,c_122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL005+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.10/5.37 % Computer : n009.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Thu Sep 24 07:06:18 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.41 Running first-order theorem proving
% 0.15/5.41 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.15/5.43
% 0.15/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.43
% 0.15/5.43 % Detected problem language: tptp
% 0.15/5.44 % Proving...
% 30.17/10.35 % SZS status Started for theBenchmark.p
% 30.17/10.35 % SZS status Theorem for theBenchmark.p
% 30.17/10.35
% 30.17/10.35 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 30.17/10.35
% 30.17/10.35 % ------ iProver source info
% 30.17/10.35
% 30.17/10.35 % git: date: 2026-07-19 20:42:38 +0200
% 30.17/10.35 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 30.17/10.35 % git: non_committed_changes: false
% 30.17/10.35
% 30.17/10.35 % ------ Parsing...
% 30.17/10.35 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 30.17/10.35 %
% 30.17/10.35
% 30.17/10.35 % ------ Preprocessing... sup_sim: 1 sf_s rm: 0 0s sf_e pe_s pe_e %
% 30.17/10.35
% 30.17/10.35 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 30.17/10.35 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 30.17/10.35
% 30.17/10.35 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 30.17/10.35 % ------ Proving...
% 30.17/10.35 % ------ Problem Properties
% 30.17/10.35
% 30.17/10.35 %
% 30.17/10.35 % clauses 24
% 30.17/10.35 % conjectures 1
% 30.17/10.35 % EPR 1
% 30.17/10.35 % Horn 24
% 30.17/10.35 % unary 24
% 30.17/10.35 % binary 0
% 30.17/10.35 % lits 24
% 30.17/10.35 % lits eq 24
% 30.17/10.35 % fd_pure 0
% 30.17/10.35 % fd_pseudo 0
% 30.17/10.35 % fd_cond 0
% 30.17/10.35 % fd_pseudo_cond 0
% 30.17/10.35 % AC symbols 1
% 30.17/10.35
% 30.17/10.35 % ------ Schedule UEQ
% 30.17/10.35
% 30.17/10.35 % ------ Option_UEQ Time Limit: 10.
% 30.17/10.35
% 30.17/10.35
% 30.17/10.35 % ------
% 30.17/10.35 % Current options:
% 30.17/10.35 % ------
% 30.17/10.35
% 30.17/10.35
% 30.17/10.35 %
% 30.17/10.35
% 30.17/10.35 % ------ Proving...
% 30.17/10.35 %
% 30.17/10.35
% 30.17/10.35 % SZS status Theorem for theBenchmark.p
% 30.17/10.35
% 30.17/10.35 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 30.17/10.36
% 30.17/10.36
%------------------------------------------------------------------------------