%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL034-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.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:57 PM UTC 2026
% Result : Unsatisfiable 244.02s 39.47s
% Output : CNFRefutation 244.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 41
% Syntax : Number of formulae : 471 ( 471 unt; 26 def)
% Number of atoms : 1356 ( 470 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 8 ( 8 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 28 ( 26 usr; 27 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 236 ( 0 sgn 236 !; 0 ?; 204 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',maddux2_join_associativity_2) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',maddux3_a_kind_of_de_Morgan_3) ).
fof(f4,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',maddux4_definiton_of_meet_4) ).
fof(f6,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001-0.ax',def_zero_13) ).
fof(f17,negated_conjecture,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
sk1 = composition(sk1,top),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
join(composition(sk2,meet(sk1,sk3)),composition(meet(sk2,converse(sk1)),meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) != join(composition(sk2,meet(sk1,sk3)),composition(meet(sk2,converse(sk1)),meet(sk1,sk3))),
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f22,plain,
composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))) != join(composition(sk2,complement(join(complement(sk1),complement(sk3)))),composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3))))),
inference(definition_unfolding,[],[f20,f6,f6,f6,f6,f6]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_68,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f8]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X0,X2),X1),
inference(cnf_transformation,[],[f9]) ).
tcf(c_70,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f10]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(cnf_transformation,[],[f11]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[],[f14]) ).
tcf(c_74,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(cnf_transformation,[],[f15]) ).
tcf(c_75,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(cnf_transformation,[],[f21]) ).
tcf(c_76,negated_conjecture,
composition(sk1,top) = sk1,
inference(cnf_transformation,[],[f18]) ).
tcf(c_77,negated_conjecture,
join(composition(sk2,complement(join(complement(sk1),complement(sk3)))),composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3))))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(cnf_transformation,[],[f22]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(theory_normalisation,[status(thm)],[c_66,c_65,c_64]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(theory_normalisation,[status(thm)],[c_73,c_65,c_64]) ).
tcf(c_128,definition,
iPr_def_10 = complement(sk1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_129,definition,
iPr_def_11 = complement(sk3),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_130,definition,
iPr_def_12 = join(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_131,definition,
iPr_def_13 = complement(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_132,definition,
iPr_def_14 = composition(sk2,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_133,definition,
iPr_def_15 = complement(sk2),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_134,definition,
iPr_def_16 = converse(sk1),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_135,definition,
iPr_def_17 = complement(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_136,definition,
iPr_def_18 = join(iPr_def_15,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_137,definition,
iPr_def_19 = complement(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_138,definition,
iPr_def_20 = composition(iPr_def_19,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_139,definition,
iPr_def_21 = join(iPr_def_14,iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_140,definition,
iPr_def_22 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_141,negated_conjecture,
iPr_def_21 != iPr_def_20,
inference(demodulation,[status(thm)],[c_77,c_134,c_135,c_133,c_136,c_137,c_138,c_129,c_128,c_130,c_131,c_132,c_139]) ).
tcf(c_142,negated_conjecture,
iPr_def_22 = sk1,
inference(demodulation,[status(thm)],[c_76,c_140]) ).
tcf(c_143,definition,
iPr_def_23 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_144,definition,
iPr_def_24 = converse(sk1),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_145,definition,
iPr_def_25 = complement(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_146,definition,
iPr_def_26 = complement(sk2),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_147,definition,
iPr_def_27 = join(iPr_def_15,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_148,definition,
iPr_def_28 = complement(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_149,definition,
iPr_def_29 = composition(iPr_def_19,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_150,definition,
iPr_def_30 = complement(sk3),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_151,definition,
iPr_def_31 = complement(sk1),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_152,definition,
iPr_def_32 = join(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_32])],[]) ).
tcf(c_153,definition,
iPr_def_33 = complement(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_33])],[]) ).
tcf(c_154,definition,
iPr_def_34 = composition(sk2,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_34])],[]) ).
tcf(c_155,definition,
iPr_def_35 = join(iPr_def_14,iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_35])],[]) ).
tcf(c_156,negated_conjecture,
iPr_def_22 = sk1,
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_157,negated_conjecture,
iPr_def_21 != iPr_def_20,
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_158,plain,
iPr_def_22 = iPr_def_23,
inference(demodulation,[status(thm)],[c_140,c_143]) ).
tcf(c_159,plain,
iPr_def_16 = iPr_def_24,
inference(demodulation,[status(thm)],[c_134,c_144]) ).
tcf(c_160,plain,
iPr_def_17 = iPr_def_25,
inference(demodulation,[status(thm)],[c_135,c_145]) ).
tcf(c_161,plain,
iPr_def_15 = iPr_def_26,
inference(demodulation,[status(thm)],[c_133,c_146]) ).
tcf(c_162,plain,
iPr_def_18 = iPr_def_27,
inference(demodulation,[status(thm)],[c_136,c_147]) ).
tcf(c_163,plain,
iPr_def_19 = iPr_def_28,
inference(demodulation,[status(thm)],[c_137,c_148]) ).
tcf(c_164,plain,
iPr_def_20 = iPr_def_29,
inference(demodulation,[status(thm)],[c_138,c_149]) ).
tcf(c_165,plain,
iPr_def_11 = iPr_def_30,
inference(demodulation,[status(thm)],[c_129,c_150]) ).
tcf(c_166,plain,
iPr_def_10 = iPr_def_31,
inference(demodulation,[status(thm)],[c_128,c_151]) ).
tcf(c_167,plain,
iPr_def_12 = iPr_def_32,
inference(demodulation,[status(thm)],[c_130,c_152]) ).
tcf(c_168,plain,
iPr_def_13 = iPr_def_33,
inference(demodulation,[status(thm)],[c_131,c_153]) ).
tcf(c_169,plain,
iPr_def_14 = iPr_def_34,
inference(demodulation,[status(thm)],[c_132,c_154]) ).
tcf(c_170,plain,
iPr_def_21 = iPr_def_35,
inference(demodulation,[status(thm)],[c_139,c_155]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_173,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(demodulation,[status(thm)],[c_75]) ).
tcf(c_174,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(demodulation,[status(thm)],[c_72]) ).
tcf(c_176,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_177,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_178,plain,
! [X0: $i,X1: $i,X2: $i] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X0,X2),X1),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_179,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_307,plain,
converse(iPr_def_22) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_144,c_156,c_159]) ).
tcf(c_327,plain,
! [X0: $i] : converse(join(iPr_def_22,X0)) = join(iPr_def_16,converse(X0)),
inference(superposition,[status(thm)],[c_307,c_176]) ).
tcf(c_335,plain,
converse(iPr_def_16) = iPr_def_22,
inference(superposition,[status(thm)],[c_307,c_177]) ).
tcf(c_341,plain,
! [X0: $i] : converse(join(iPr_def_16,X0)) = join(iPr_def_22,converse(X0)),
inference(superposition,[status(thm)],[c_335,c_176]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] : join(converse(X0),join(iPr_def_16,converse(X1))) = converse(join(X0,join(iPr_def_22,X1))),
inference(superposition,[status(thm)],[c_327,c_176]) ).
tcf(c_415,plain,
! [X0: $i,X1: $i] : join(iPr_def_16,join(converse(X0),converse(X1))) = converse(join(X0,join(iPr_def_22,X1))),
inference(theory_normalisation,[status(thm)],[c_412,c_181,c_182]) ).
tcf(c_416,plain,
! [X0: $i,X1: $i] : converse(join(X0,join(iPr_def_22,X1))) = join(iPr_def_16,converse(join(X0,X1))),
inference(demodulation,[status(thm)],[c_415,c_176]) ).
tcf(c_441,plain,
! [X0: $i,X1: $i] : join(converse(X0),join(iPr_def_22,converse(X1))) = converse(join(X0,join(iPr_def_16,X1))),
inference(superposition,[status(thm)],[c_341,c_176]) ).
tcf(c_445,plain,
! [X0: $i,X1: $i] : join(iPr_def_22,join(converse(X0),converse(X1))) = converse(join(X0,join(iPr_def_16,X1))),
inference(theory_normalisation,[status(thm)],[c_441,c_181,c_182]) ).
tcf(c_446,plain,
! [X0: $i,X1: $i] : converse(join(X0,join(iPr_def_16,X1))) = join(iPr_def_22,converse(join(X0,X1))),
inference(demodulation,[status(thm)],[c_445,c_176]) ).
tcf(c_2484,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_181,c_182]) ).
tcf(c_2488,plain,
complement(top) = zero,
inference(ac_demodulation,[status(thm)],[c_173,c_174,c_181,c_182]) ).
tcf(c_2490,plain,
converse(iPr_def_22) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_144,c_156,c_159]) ).
tcf(c_2491,plain,
complement(iPr_def_16) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_145,c_160]) ).
tcf(c_2492,plain,
join(iPr_def_16,iPr_def_17) = top,
inference(superposition,[status(thm)],[c_2491,c_174]) ).
tcf(c_2494,plain,
! [X0: $i] : composition(converse(X0),iPr_def_16) = converse(composition(iPr_def_22,X0)),
inference(superposition,[status(thm)],[c_2490,c_175]) ).
tcf(c_2495,plain,
complement(sk2) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_146,c_161]) ).
tcf(c_2497,plain,
complement(iPr_def_18) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_148,c_163]) ).
tcf(c_2498,plain,
join(iPr_def_18,iPr_def_19) = top,
inference(superposition,[status(thm)],[c_2497,c_174]) ).
tcf(c_2500,plain,
complement(sk3) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_150,c_165]) ).
tcf(c_2501,plain,
join(sk3,iPr_def_11) = top,
inference(superposition,[status(thm)],[c_2500,c_174]) ).
tcf(c_2502,plain,
complement(iPr_def_22) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_151,c_156,c_166]) ).
tcf(c_2503,plain,
join(iPr_def_22,iPr_def_10) = top,
inference(superposition,[status(thm)],[c_2502,c_174]) ).
tcf(c_2504,plain,
join(iPr_def_10,iPr_def_22) = top,
inference(theory_normalisation,[status(thm)],[c_2503,c_181,c_182]) ).
tcf(c_2505,plain,
join(iPr_def_11,sk3) = top,
inference(theory_normalisation,[status(thm)],[c_2501,c_181,c_182]) ).
tcf(c_2506,plain,
complement(iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_153,c_168]) ).
tcf(c_2507,plain,
join(iPr_def_12,iPr_def_13) = top,
inference(superposition,[status(thm)],[c_2506,c_174]) ).
tcf(c_2509,plain,
composition(iPr_def_22,top) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_143,c_156,c_158]) ).
tcf(c_2510,plain,
! [X0: $i] : converse(join(iPr_def_22,X0)) = join(iPr_def_16,converse(X0)),
inference(superposition,[status(thm)],[c_2490,c_176]) ).
tcf(c_2511,plain,
! [X0: $i] : converse(join(X0,iPr_def_22)) = join(converse(X0),iPr_def_16),
inference(superposition,[status(thm)],[c_2490,c_176]) ).
tcf(c_2512,plain,
! [X0: $i] : converse(join(X0,iPr_def_22)) = join(iPr_def_16,converse(X0)),
inference(theory_normalisation,[status(thm)],[c_2511,c_181,c_182]) ).
tcf(c_2513,plain,
join(iPr_def_15,iPr_def_17) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_147,c_162]) ).
tcf(c_2514,plain,
composition(iPr_def_19,iPr_def_13) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_149,c_164]) ).
tcf(c_2515,plain,
join(iPr_def_10,iPr_def_11) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_152,c_167]) ).
tcf(c_2516,plain,
composition(sk2,iPr_def_13) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_154,c_169]) ).
tcf(c_2517,plain,
join(iPr_def_14,iPr_def_20) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_155,c_170]) ).
tcf(c_2518,plain,
converse(iPr_def_16) = iPr_def_22,
inference(superposition,[status(thm)],[c_2490,c_177]) ).
tcf(c_2519,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_177,c_176]) ).
tcf(c_2520,plain,
! [X0: $i,X1: $i] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(superposition,[status(thm)],[c_177,c_175]) ).
tcf(c_2521,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(superposition,[status(thm)],[c_177,c_176]) ).
tcf(c_2522,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_177,c_175]) ).
tcf(c_2524,plain,
! [X0: $i] : converse(join(iPr_def_16,X0)) = join(iPr_def_22,converse(X0)),
inference(superposition,[status(thm)],[c_2518,c_176]) ).
tcf(c_2526,plain,
! [X0: $i] : converse(join(X0,iPr_def_16)) = join(converse(X0),iPr_def_22),
inference(superposition,[status(thm)],[c_2518,c_176]) ).
tcf(c_2527,plain,
! [X0: $i] : composition(converse(X0),iPr_def_22) = converse(composition(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_2518,c_175]) ).
tcf(c_2528,plain,
! [X0: $i] : converse(join(X0,iPr_def_16)) = join(iPr_def_22,converse(X0)),
inference(theory_normalisation,[status(thm)],[c_2526,c_181,c_182]) ).
tcf(c_2533,plain,
! [X0: $i] : composition(join(iPr_def_22,X0),top) = join(iPr_def_22,composition(X0,top)),
inference(superposition,[status(thm)],[c_2509,c_178]) ).
tcf(c_2536,plain,
! [X0: $i] : composition(join(X0,sk2),iPr_def_13) = join(composition(X0,iPr_def_13),iPr_def_14),
inference(superposition,[status(thm)],[c_2516,c_178]) ).
tcf(c_2537,plain,
! [X0: $i] : composition(join(X0,iPr_def_19),iPr_def_13) = join(composition(X0,iPr_def_13),iPr_def_20),
inference(superposition,[status(thm)],[c_2514,c_178]) ).
tcf(c_2540,plain,
! [X0: $i] : composition(join(X0,iPr_def_19),iPr_def_13) = join(iPr_def_20,composition(X0,iPr_def_13)),
inference(theory_normalisation,[status(thm)],[c_2537,c_181,c_182]) ).
tcf(c_2541,plain,
! [X0: $i] : composition(join(X0,sk2),iPr_def_13) = join(iPr_def_14,composition(X0,iPr_def_13)),
inference(theory_normalisation,[status(thm)],[c_2536,c_181,c_182]) ).
tcf(c_2551,plain,
! [X0: $i,X1: $i] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(superposition,[status(thm)],[c_179,c_180]) ).
tcf(c_2568,plain,
composition(converse(one),iPr_def_16) = converse(iPr_def_22),
inference(superposition,[status(thm)],[c_179,c_2494]) ).
tcf(c_2577,plain,
composition(converse(one),iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_2568,c_2490]) ).
tcf(c_2588,plain,
join(iPr_def_16,converse(complement(iPr_def_22))) = converse(top),
inference(superposition,[status(thm)],[c_174,c_2510]) ).
tcf(c_2594,plain,
join(iPr_def_16,converse(iPr_def_10)) = converse(top),
inference(demodulation,[status(thm)],[c_2588,c_2502]) ).
tcf(c_2601,plain,
! [X0: $i] : converse(join(iPr_def_16,converse(X0))) = join(X0,iPr_def_22),
inference(superposition,[status(thm)],[c_2512,c_177]) ).
tcf(c_2613,plain,
join(iPr_def_22,converse(iPr_def_17)) = converse(top),
inference(superposition,[status(thm)],[c_2492,c_2524]) ).
tcf(c_2627,plain,
! [X0: $i,X1: $i,X2: $i] : join(converse(X0),join(converse(X1),X2)) = join(converse(join(X0,X1)),X2),
inference(superposition,[status(thm)],[c_176,c_181]) ).
tcf(c_2628,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[status(thm)],[c_174,c_181]) ).
tcf(c_2629,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_11,X0)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_2515,c_181]) ).
tcf(c_2630,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_17,X0)) = join(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_2513,c_181]) ).
tcf(c_2632,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_17,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_2492,c_181]) ).
tcf(c_2633,plain,
! [X0: $i] : join(iPr_def_18,join(iPr_def_19,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_2498,c_181]) ).
tcf(c_2635,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_22,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_2504,c_181]) ).
tcf(c_2637,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_13,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_2507,c_181]) ).
tcf(c_2658,plain,
composition(converse(one),iPr_def_22) = converse(iPr_def_16),
inference(superposition,[status(thm)],[c_179,c_2527]) ).
tcf(c_2666,plain,
composition(converse(one),iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_2658,c_2518]) ).
tcf(c_2676,plain,
! [X0: $i] : converse(join(iPr_def_22,converse(X0))) = join(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_2528,c_177]) ).
tcf(c_2739,plain,
! [X0: $i,X1: $i] : join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1))))) = complement(converse(X0)),
inference(superposition,[status(thm)],[c_175,c_171]) ).
tcf(c_2742,plain,
join(complement(top),composition(converse(iPr_def_22),complement(iPr_def_22))) = complement(top),
inference(superposition,[status(thm)],[c_2509,c_171]) ).
tcf(c_2746,plain,
join(complement(iPr_def_16),composition(converse(converse(one)),complement(iPr_def_16))) = complement(iPr_def_16),
inference(superposition,[status(thm)],[c_2577,c_171]) ).
tcf(c_2748,plain,
join(complement(iPr_def_22),composition(converse(converse(one)),complement(iPr_def_22))) = complement(iPr_def_22),
inference(superposition,[status(thm)],[c_2666,c_171]) ).
tcf(c_2750,plain,
join(zero,composition(iPr_def_16,iPr_def_10)) = zero,
inference(demodulation,[status(thm)],[c_2742,c_2488,c_2490,c_2502]) ).
tcf(c_2751,plain,
join(iPr_def_10,composition(one,iPr_def_10)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_2748,c_177,c_2502]) ).
tcf(c_2753,plain,
join(iPr_def_17,composition(one,iPr_def_17)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_2746,c_177,c_2491]) ).
tcf(c_2754,plain,
! [X0: $i,X1: $i] : join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1))))) = complement(converse(X0)),
inference(demodulation,[status(thm)],[c_2739,c_177]) ).
tcf(c_2840,plain,
! [X0: $i,X1: $i] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[status(thm)],[c_182,c_172]) ).
tcf(c_2854,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_174,c_172]) ).
tcf(c_2863,plain,
! [X0: $i] : join(complement(join(complement(X0),sk2)),complement(join(complement(X0),iPr_def_15))) = X0,
inference(superposition,[status(thm)],[c_2495,c_172]) ).
tcf(c_2866,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_16)),complement(join(complement(X0),iPr_def_17))) = X0,
inference(superposition,[status(thm)],[c_2491,c_172]) ).
tcf(c_2867,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_18)),complement(join(complement(X0),iPr_def_19))) = X0,
inference(superposition,[status(thm)],[c_2497,c_172]) ).
tcf(c_2869,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_22)),complement(join(complement(X0),iPr_def_10))) = X0,
inference(superposition,[status(thm)],[c_2502,c_172]) ).
tcf(c_2873,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_2854,c_181,c_182]) ).
tcf(c_2874,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_2873,c_2488]) ).
tcf(c_2875,plain,
! [X0: $i] : join(complement(join(iPr_def_10,complement(X0))),complement(join(iPr_def_22,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_2869,c_181,c_182]) ).
tcf(c_2877,plain,
! [X0: $i] : join(complement(join(iPr_def_18,complement(X0))),complement(join(iPr_def_19,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_2867,c_181,c_182]) ).
tcf(c_2878,plain,
! [X0: $i] : join(complement(join(iPr_def_16,complement(X0))),complement(join(iPr_def_17,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_2866,c_181,c_182]) ).
tcf(c_2881,plain,
! [X0: $i] : join(complement(join(iPr_def_15,complement(X0))),complement(join(sk2,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_2863,c_181,c_182]) ).
tcf(c_2914,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_11)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_182,c_2629]) ).
tcf(c_2917,plain,
join(iPr_def_10,top) = join(iPr_def_12,sk3),
inference(superposition,[status(thm)],[c_2505,c_2629]) ).
tcf(c_2924,plain,
! [X0: $i] : join(iPr_def_15,join(X0,iPr_def_17)) = join(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_182,c_2630]) ).
tcf(c_2928,plain,
join(iPr_def_18,composition(one,iPr_def_17)) = join(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_2753,c_2630]) ).
tcf(c_2930,plain,
join(iPr_def_18,composition(one,iPr_def_17)) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2928,c_2513]) ).
tcf(c_2982,plain,
! [X0: $i] : join(iPr_def_16,join(X0,iPr_def_17)) = join(top,X0),
inference(superposition,[status(thm)],[c_182,c_2632]) ).
tcf(c_2986,plain,
join(top,composition(one,iPr_def_17)) = join(iPr_def_16,iPr_def_17),
inference(superposition,[status(thm)],[c_2753,c_2632]) ).
tcf(c_2989,plain,
join(top,composition(one,iPr_def_17)) = top,
inference(demodulation,[status(thm)],[c_2986,c_2492]) ).
tcf(c_3068,plain,
join(top,converse(iPr_def_17)) = join(iPr_def_10,converse(top)),
inference(superposition,[status(thm)],[c_2613,c_2635]) ).
tcf(c_3120,plain,
! [X0: $i] : join(iPr_def_16,join(X0,iPr_def_17)) = join(X0,top),
inference(superposition,[status(thm)],[c_2492,c_2484]) ).
tcf(c_3124,plain,
! [X0: $i] : join(iPr_def_11,join(X0,sk3)) = join(X0,top),
inference(superposition,[status(thm)],[c_2505,c_2484]) ).
tcf(c_3139,plain,
! [X0: $i] : join(iPr_def_10,join(X0,composition(one,iPr_def_10))) = join(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_2751,c_2484]) ).
tcf(c_3243,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(X1,converse(X0)),
inference(superposition,[status(thm)],[c_182,c_2519]) ).
tcf(c_3247,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[status(thm)],[c_174,c_2519]) ).
tcf(c_3416,plain,
join(iPr_def_16,converse(join(iPr_def_10,iPr_def_11))) = converse(join(iPr_def_12,iPr_def_22)),
inference(superposition,[status(thm)],[c_2914,c_416]) ).
tcf(c_3418,plain,
join(top,iPr_def_11) = join(iPr_def_12,iPr_def_22),
inference(superposition,[status(thm)],[c_2914,c_2635]) ).
tcf(c_3419,plain,
join(iPr_def_11,top) = join(iPr_def_12,iPr_def_22),
inference(theory_normalisation,[status(thm)],[c_3418,c_181,c_182]) ).
tcf(c_3421,plain,
join(iPr_def_16,converse(join(iPr_def_10,iPr_def_11))) = converse(join(iPr_def_11,top)),
inference(demodulation,[status(thm)],[c_3416,c_3419]) ).
tcf(c_3422,plain,
converse(join(iPr_def_11,top)) = join(iPr_def_16,converse(iPr_def_12)),
inference(demodulation,[status(thm)],[c_3421,c_2515]) ).
tcf(c_3424,plain,
! [X0: $i] : join(join(iPr_def_11,top),X0) = join(iPr_def_12,join(iPr_def_22,X0)),
inference(superposition,[status(thm)],[c_3419,c_181]) ).
tcf(c_3428,plain,
! [X0: $i] : join(iPr_def_11,join(top,X0)) = join(iPr_def_12,join(iPr_def_22,X0)),
inference(theory_normalisation,[status(thm)],[c_3424,c_181,c_182]) ).
tcf(c_3436,plain,
join(iPr_def_15,top) = join(iPr_def_18,iPr_def_16),
inference(superposition,[status(thm)],[c_2492,c_2924]) ).
tcf(c_3443,plain,
join(iPr_def_22,converse(join(iPr_def_15,iPr_def_17))) = converse(join(iPr_def_18,iPr_def_16)),
inference(superposition,[status(thm)],[c_2924,c_446]) ).
tcf(c_3446,plain,
join(iPr_def_15,top) = join(iPr_def_16,iPr_def_18),
inference(theory_normalisation,[status(thm)],[c_3436,c_181,c_182]) ).
tcf(c_3448,plain,
join(iPr_def_22,converse(join(iPr_def_15,iPr_def_17))) = converse(join(iPr_def_16,iPr_def_18)),
inference(theory_normalisation,[status(thm)],[c_3443,c_181,c_182]) ).
tcf(c_3449,plain,
join(iPr_def_22,converse(join(iPr_def_15,iPr_def_17))) = converse(join(iPr_def_15,top)),
inference(demodulation,[status(thm)],[c_3448,c_3446]) ).
tcf(c_3450,plain,
converse(join(iPr_def_15,top)) = join(iPr_def_22,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_3449,c_2513]) ).
tcf(c_3514,plain,
converse(join(iPr_def_16,join(iPr_def_16,converse(iPr_def_12)))) = join(join(iPr_def_11,top),iPr_def_22),
inference(superposition,[status(thm)],[c_3422,c_2601]) ).
tcf(c_3515,plain,
converse(join(iPr_def_16,converse(iPr_def_12))) = join(iPr_def_11,top),
inference(superposition,[status(thm)],[c_3422,c_177]) ).
tcf(c_3522,plain,
converse(join(iPr_def_16,join(iPr_def_16,converse(iPr_def_12)))) = join(iPr_def_11,join(iPr_def_22,top)),
inference(theory_normalisation,[status(thm)],[c_3514,c_181,c_182]) ).
tcf(c_3531,plain,
converse(join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18)))) = join(join(iPr_def_15,top),iPr_def_22),
inference(superposition,[status(thm)],[c_3450,c_2601]) ).
tcf(c_3532,plain,
converse(join(iPr_def_22,converse(iPr_def_18))) = join(iPr_def_15,top),
inference(superposition,[status(thm)],[c_3450,c_177]) ).
tcf(c_3539,plain,
converse(join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18)))) = join(iPr_def_15,join(iPr_def_22,top)),
inference(theory_normalisation,[status(thm)],[c_3531,c_181,c_182]) ).
tcf(c_3571,plain,
! [X0: $i,X1: $i] : join(iPr_def_16,join(X0,join(X1,iPr_def_17))) = join(X0,join(top,X1)),
inference(superposition,[status(thm)],[c_2982,c_2484]) ).
tcf(c_3635,plain,
converse(join(iPr_def_10,converse(top))) = join(converse(top),iPr_def_17),
inference(superposition,[status(thm)],[c_3068,c_2521]) ).
tcf(c_3686,plain,
join(converse(top),iPr_def_17) = join(converse(iPr_def_10),top),
inference(demodulation,[status(thm)],[c_3635,c_2521]) ).
tcf(c_3687,plain,
join(top,converse(iPr_def_10)) = join(iPr_def_17,converse(top)),
inference(theory_normalisation,[status(thm)],[c_3686,c_181,c_182]) ).
tcf(c_3740,plain,
converse(join(iPr_def_22,join(iPr_def_15,top))) = join(join(iPr_def_22,converse(iPr_def_18)),iPr_def_16),
inference(superposition,[status(thm)],[c_3532,c_2676]) ).
tcf(c_3757,plain,
converse(join(iPr_def_15,join(iPr_def_22,top))) = join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18))),
inference(theory_normalisation,[status(thm)],[c_3740,c_181,c_182]) ).
tcf(c_3765,plain,
converse(join(iPr_def_17,converse(top))) = join(converse(top),iPr_def_10),
inference(superposition,[status(thm)],[c_3687,c_2521]) ).
tcf(c_3766,plain,
converse(join(iPr_def_17,converse(top))) = join(iPr_def_10,converse(top)),
inference(theory_normalisation,[status(thm)],[c_3765,c_181,c_182]) ).
tcf(c_3772,plain,
converse(join(iPr_def_10,converse(top))) = join(iPr_def_17,converse(top)),
inference(superposition,[status(thm)],[c_3766,c_177]) ).
tcf(c_3884,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_179,c_2522]) ).
tcf(c_3937,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(demodulation,[status(thm)],[c_3884,c_177]) ).
tcf(c_3944,plain,
converse(join(iPr_def_22,join(iPr_def_17,converse(top)))) = join(join(iPr_def_10,converse(top)),iPr_def_16),
inference(superposition,[status(thm)],[c_3772,c_2676]) ).
tcf(c_3958,plain,
converse(join(iPr_def_17,join(iPr_def_22,converse(top)))) = join(iPr_def_10,join(iPr_def_16,converse(top))),
inference(theory_normalisation,[status(thm)],[c_3944,c_181,c_182]) ).
tcf(c_4017,plain,
! [X0: $i,X1: $i] : composition(join(converse(one),X0),X1) = join(X1,composition(X0,X1)),
inference(superposition,[status(thm)],[c_3937,c_178]) ).
tcf(c_4018,plain,
converse(one) = one,
inference(superposition,[status(thm)],[c_3937,c_179]) ).
tcf(c_4019,plain,
! [X0: $i,X1: $i] : composition(join(X0,converse(one)),X1) = join(composition(X0,X1),X1),
inference(superposition,[status(thm)],[c_3937,c_178]) ).
tcf(c_4022,plain,
! [X0: $i] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(superposition,[status(thm)],[c_3937,c_171]) ).
tcf(c_4027,plain,
! [X0: $i] : composition(converse(one),X0) = composition(one,X0),
inference(superposition,[status(thm)],[c_3937,c_2551]) ).
tcf(c_4028,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(demodulation,[status(thm)],[c_4027,c_3937]) ).
tcf(c_4030,plain,
! [X0: $i] : join(complement(X0),complement(X0)) = complement(X0),
inference(demodulation,[status(thm)],[c_4022,c_4028]) ).
tcf(c_4031,plain,
! [X0: $i,X1: $i] : join(composition(X0,X1),X1) = composition(join(X0,one),X1),
inference(demodulation,[status(thm)],[c_4019,c_4018]) ).
tcf(c_4032,plain,
! [X0: $i,X1: $i] : join(X0,composition(X1,X0)) = composition(join(X1,one),X0),
inference(theory_normalisation,[status(thm)],[c_4031,c_181,c_182]) ).
tcf(c_4033,plain,
! [X0: $i,X1: $i] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(demodulation,[status(thm)],[c_4017,c_4018]) ).
tcf(c_4044,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_10)) = join(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_3139,c_4028]) ).
tcf(c_4051,plain,
join(top,iPr_def_17) = top,
inference(demodulation,[status(thm)],[c_2989,c_4028]) ).
tcf(c_4053,plain,
join(iPr_def_18,iPr_def_17) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2930,c_4028]) ).
tcf(c_4056,plain,
join(iPr_def_17,iPr_def_18) = iPr_def_18,
inference(theory_normalisation,[status(thm)],[c_4053,c_181,c_182]) ).
tcf(c_4058,plain,
join(iPr_def_17,top) = top,
inference(theory_normalisation,[status(thm)],[c_4051,c_181,c_182]) ).
tcf(c_4065,plain,
! [X0: $i] : join(zero,complement(complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_2874,c_4030]) ).
tcf(c_4067,plain,
converse(join(iPr_def_22,one)) = join(one,iPr_def_16),
inference(superposition,[status(thm)],[c_4018,c_2676]) ).
tcf(c_4078,plain,
converse(join(iPr_def_22,one)) = join(iPr_def_16,one),
inference(theory_normalisation,[status(thm)],[c_4067,c_181,c_182]) ).
tcf(c_4179,plain,
join(top,iPr_def_18) = join(iPr_def_16,iPr_def_18),
inference(superposition,[status(thm)],[c_4056,c_2632]) ).
tcf(c_4181,plain,
join(iPr_def_16,iPr_def_18) = join(iPr_def_18,top),
inference(theory_normalisation,[status(thm)],[c_4179,c_181,c_182]) ).
tcf(c_4182,plain,
join(iPr_def_15,top) = join(iPr_def_18,top),
inference(demodulation,[status(thm)],[c_4181,c_3446]) ).
tcf(c_4188,plain,
join(top,top) = join(iPr_def_16,top),
inference(superposition,[status(thm)],[c_4058,c_2632]) ).
tcf(c_4197,plain,
join(zero,complement(iPr_def_15)) = sk2,
inference(superposition,[status(thm)],[c_2495,c_4065]) ).
tcf(c_4200,plain,
join(zero,complement(iPr_def_17)) = iPr_def_16,
inference(superposition,[status(thm)],[c_2491,c_4065]) ).
tcf(c_4274,plain,
join(iPr_def_15,iPr_def_15) = iPr_def_15,
inference(superposition,[status(thm)],[c_2495,c_4030]) ).
tcf(c_4275,plain,
join(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_2500,c_4030]) ).
tcf(c_4276,plain,
join(iPr_def_13,iPr_def_13) = iPr_def_13,
inference(superposition,[status(thm)],[c_2506,c_4030]) ).
tcf(c_4278,plain,
join(iPr_def_19,iPr_def_19) = iPr_def_19,
inference(superposition,[status(thm)],[c_2497,c_4030]) ).
tcf(c_4279,plain,
join(zero,zero) = zero,
inference(superposition,[status(thm)],[c_2488,c_4030]) ).
tcf(c_4287,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_15,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_4274,c_181]) ).
tcf(c_4309,plain,
join(iPr_def_10,iPr_def_11) = join(iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_4275,c_2914]) ).
tcf(c_4310,plain,
join(iPr_def_10,iPr_def_11) = join(iPr_def_11,iPr_def_12),
inference(theory_normalisation,[status(thm)],[c_4309,c_181,c_182]) ).
tcf(c_4311,plain,
join(iPr_def_11,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_4310,c_2515]) ).
tcf(c_4315,plain,
join(top,iPr_def_13) = join(iPr_def_12,iPr_def_13),
inference(superposition,[status(thm)],[c_4276,c_2637]) ).
tcf(c_4316,plain,
join(iPr_def_12,iPr_def_13) = join(iPr_def_13,top),
inference(theory_normalisation,[status(thm)],[c_4315,c_181,c_182]) ).
tcf(c_4317,plain,
join(iPr_def_13,top) = top,
inference(demodulation,[status(thm)],[c_4316,c_2507]) ).
tcf(c_4322,plain,
join(top,iPr_def_19) = join(iPr_def_18,iPr_def_19),
inference(superposition,[status(thm)],[c_4278,c_2633]) ).
tcf(c_4324,plain,
join(iPr_def_18,iPr_def_19) = join(iPr_def_19,top),
inference(theory_normalisation,[status(thm)],[c_4322,c_181,c_182]) ).
tcf(c_4325,plain,
join(iPr_def_19,top) = top,
inference(demodulation,[status(thm)],[c_4324,c_2498]) ).
tcf(c_4327,plain,
! [X0: $i] : join(zero,join(zero,X0)) = join(zero,X0),
inference(superposition,[status(thm)],[c_4279,c_181]) ).
tcf(c_4330,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_12,X0)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_4311,c_181]) ).
tcf(c_4337,plain,
join(top,top) = join(iPr_def_12,top),
inference(superposition,[status(thm)],[c_4317,c_2637]) ).
tcf(c_4338,plain,
join(iPr_def_12,top) = join(iPr_def_16,top),
inference(demodulation,[status(thm)],[c_4188,c_4337]) ).
tcf(c_4378,plain,
join(top,top) = join(iPr_def_18,top),
inference(superposition,[status(thm)],[c_4325,c_2633]) ).
tcf(c_4379,plain,
join(iPr_def_12,top) = join(iPr_def_15,top),
inference(demodulation,[status(thm)],[c_4378,c_4182,c_4337]) ).
tcf(c_4392,plain,
converse(join(iPr_def_12,top)) = join(iPr_def_22,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_3450,c_4379]) ).
tcf(c_4450,plain,
converse(join(iPr_def_12,top)) = join(iPr_def_22,converse(top)),
inference(superposition,[status(thm)],[c_4338,c_2524]) ).
tcf(c_4452,plain,
join(iPr_def_22,converse(top)) = join(iPr_def_22,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_4450,c_4392]) ).
tcf(c_4455,plain,
converse(join(iPr_def_17,join(iPr_def_22,converse(iPr_def_18)))) = join(iPr_def_10,join(iPr_def_16,converse(top))),
inference(demodulation,[status(thm)],[c_3958,c_4452]) ).
tcf(c_4659,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_17,X0)) = join(X0,top),
inference(superposition,[status(thm)],[c_182,c_3120]) ).
tcf(c_4667,plain,
! [X0: $i,X1: $i] : join(iPr_def_16,join(X0,join(X1,iPr_def_17))) = join(X0,join(X1,top)),
inference(superposition,[status(thm)],[c_3120,c_2484]) ).
tcf(c_4767,plain,
converse(join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18)))) = join(join(iPr_def_12,top),iPr_def_22),
inference(superposition,[status(thm)],[c_4392,c_2601]) ).
tcf(c_4777,plain,
converse(join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18)))) = join(iPr_def_12,join(iPr_def_22,top)),
inference(theory_normalisation,[status(thm)],[c_4767,c_181,c_182]) ).
tcf(c_4778,plain,
converse(join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18)))) = join(iPr_def_12,top),
inference(demodulation,[status(thm)],[c_4777,c_3428,c_4330,c_4337]) ).
tcf(c_4784,plain,
join(iPr_def_15,join(iPr_def_22,top)) = join(iPr_def_12,top),
inference(demodulation,[status(thm)],[c_3539,c_4778]) ).
tcf(c_4785,plain,
join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18))) = converse(join(iPr_def_12,top)),
inference(demodulation,[status(thm)],[c_3757,c_4784]) ).
tcf(c_4786,plain,
join(iPr_def_16,join(iPr_def_22,converse(iPr_def_18))) = join(iPr_def_22,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_4785,c_4392]) ).
tcf(c_4922,plain,
join(iPr_def_10,join(iPr_def_22,converse(iPr_def_18))) = join(top,converse(top)),
inference(superposition,[status(thm)],[c_4452,c_2635]) ).
tcf(c_4929,plain,
join(top,converse(top)) = join(top,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_4922,c_2635]) ).
tcf(c_5016,plain,
join(join(iPr_def_16,join(iPr_def_16,converse(iPr_def_12))),converse(complement(join(iPr_def_11,join(iPr_def_22,top))))) = converse(top),
inference(superposition,[status(thm)],[c_3522,c_3247]) ).
tcf(c_5017,plain,
join(join(iPr_def_16,converse(iPr_def_12)),converse(complement(join(iPr_def_11,top)))) = converse(top),
inference(superposition,[status(thm)],[c_3515,c_3247]) ).
tcf(c_5019,plain,
join(join(iPr_def_22,one),converse(complement(join(iPr_def_16,one)))) = converse(top),
inference(superposition,[status(thm)],[c_4078,c_3247]) ).
tcf(c_5021,plain,
join(join(iPr_def_12,top),converse(complement(join(iPr_def_22,converse(iPr_def_18))))) = converse(top),
inference(superposition,[status(thm)],[c_4392,c_3247]) ).
tcf(c_5044,plain,
join(iPr_def_18,converse(complement(converse(iPr_def_17)))) = join(iPr_def_15,converse(top)),
inference(superposition,[status(thm)],[c_3247,c_2630]) ).
tcf(c_5054,plain,
join(iPr_def_22,join(one,converse(complement(join(iPr_def_16,one))))) = converse(top),
inference(theory_normalisation,[status(thm)],[c_5019,c_181,c_182]) ).
tcf(c_5058,plain,
join(iPr_def_12,join(top,converse(complement(join(iPr_def_22,converse(iPr_def_18)))))) = converse(top),
inference(theory_normalisation,[status(thm)],[c_5021,c_181,c_182]) ).
tcf(c_5061,plain,
join(iPr_def_16,join(converse(iPr_def_12),converse(complement(join(iPr_def_11,top))))) = converse(top),
inference(theory_normalisation,[status(thm)],[c_5017,c_181,c_182]) ).
tcf(c_5062,plain,
join(iPr_def_16,converse(join(iPr_def_12,complement(join(iPr_def_11,top))))) = converse(top),
inference(demodulation,[status(thm)],[c_5061,c_176]) ).
tcf(c_5085,plain,
join(iPr_def_16,join(iPr_def_16,join(converse(iPr_def_12),converse(complement(join(iPr_def_11,join(iPr_def_22,top))))))) = converse(top),
inference(theory_normalisation,[status(thm)],[c_5016,c_181,c_182]) ).
tcf(c_5086,plain,
join(iPr_def_16,join(iPr_def_16,converse(join(iPr_def_12,complement(join(iPr_def_11,join(iPr_def_22,top))))))) = converse(top),
inference(demodulation,[status(thm)],[c_5085,c_176]) ).
tcf(c_5199,plain,
converse(join(top,converse(iPr_def_18))) = join(converse(top),top),
inference(superposition,[status(thm)],[c_4929,c_2521]) ).
tcf(c_5200,plain,
converse(join(top,converse(iPr_def_18))) = join(top,converse(top)),
inference(theory_normalisation,[status(thm)],[c_5199,c_181,c_182]) ).
tcf(c_5201,plain,
converse(join(top,converse(iPr_def_18))) = join(top,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_5200,c_4929]) ).
tcf(c_5202,plain,
join(top,converse(iPr_def_18)) = join(iPr_def_18,converse(top)),
inference(demodulation,[status(thm)],[c_5201,c_3243]) ).
tcf(c_5211,plain,
converse(join(iPr_def_18,converse(top))) = join(converse(top),iPr_def_18),
inference(superposition,[status(thm)],[c_5202,c_2521]) ).
tcf(c_5212,plain,
converse(join(iPr_def_18,converse(top))) = join(iPr_def_18,converse(top)),
inference(theory_normalisation,[status(thm)],[c_5211,c_181,c_182]) ).
tcf(c_5328,plain,
join(iPr_def_11,iPr_def_10) = join(iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_4044,c_2629]) ).
tcf(c_5329,plain,
join(top,iPr_def_10) = join(iPr_def_22,iPr_def_10),
inference(superposition,[status(thm)],[c_4044,c_2635]) ).
tcf(c_5330,plain,
join(iPr_def_10,top) = join(iPr_def_10,iPr_def_22),
inference(theory_normalisation,[status(thm)],[c_5329,c_181,c_182]) ).
tcf(c_5331,plain,
join(iPr_def_10,top) = top,
inference(demodulation,[status(thm)],[c_5330,c_2504]) ).
tcf(c_5332,plain,
join(iPr_def_10,iPr_def_11) = join(iPr_def_10,iPr_def_12),
inference(theory_normalisation,[status(thm)],[c_5328,c_181,c_182]) ).
tcf(c_5333,plain,
join(iPr_def_10,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_5332,c_2515]) ).
tcf(c_5342,plain,
join(iPr_def_12,sk3) = top,
inference(demodulation,[status(thm)],[c_2917,c_5331]) ).
tcf(c_5436,plain,
join(iPr_def_11,top) = join(iPr_def_12,top),
inference(superposition,[status(thm)],[c_5342,c_3124]) ).
tcf(c_5456,plain,
converse(join(iPr_def_11,top)) = join(iPr_def_22,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_4392,c_5436]) ).
tcf(c_5459,plain,
join(iPr_def_11,top) = join(iPr_def_15,top),
inference(demodulation,[status(thm)],[c_4379,c_5436]) ).
tcf(c_5469,plain,
join(top,top) = join(iPr_def_11,top),
inference(demodulation,[status(thm)],[c_4337,c_5436]) ).
tcf(c_5473,plain,
join(iPr_def_16,converse(iPr_def_12)) = join(iPr_def_22,converse(iPr_def_18)),
inference(demodulation,[status(thm)],[c_5456,c_3422]) ).
tcf(c_5475,plain,
join(iPr_def_12,join(top,converse(complement(join(iPr_def_16,converse(iPr_def_12)))))) = converse(top),
inference(demodulation,[status(thm)],[c_5058,c_5473]) ).
tcf(c_5478,plain,
join(iPr_def_16,join(iPr_def_16,converse(iPr_def_12))) = join(iPr_def_16,converse(iPr_def_12)),
inference(demodulation,[status(thm)],[c_4786,c_5473]) ).
tcf(c_5480,plain,
converse(join(iPr_def_17,join(iPr_def_16,converse(iPr_def_12)))) = join(iPr_def_10,join(iPr_def_16,converse(top))),
inference(demodulation,[status(thm)],[c_4455,c_5473]) ).
tcf(c_5483,plain,
converse(join(iPr_def_16,join(iPr_def_17,converse(iPr_def_12)))) = join(iPr_def_10,join(iPr_def_16,converse(top))),
inference(theory_normalisation,[status(thm)],[c_5480,c_181,c_182]) ).
tcf(c_5484,plain,
join(iPr_def_10,join(iPr_def_16,converse(top))) = join(iPr_def_12,converse(top)),
inference(demodulation,[status(thm)],[c_5483,c_182,c_3243,c_4659]) ).
tcf(c_5494,plain,
converse(join(iPr_def_16,converse(iPr_def_12))) = join(iPr_def_11,join(iPr_def_22,top)),
inference(demodulation,[status(thm)],[c_3522,c_5478]) ).
tcf(c_5495,plain,
join(iPr_def_11,join(iPr_def_22,top)) = join(iPr_def_11,top),
inference(demodulation,[status(thm)],[c_5494,c_3515]) ).
tcf(c_5496,plain,
join(iPr_def_16,join(iPr_def_16,converse(join(iPr_def_12,complement(join(iPr_def_11,top)))))) = converse(top),
inference(demodulation,[status(thm)],[c_5086,c_5495]) ).
tcf(c_5497,plain,
join(iPr_def_16,converse(top)) = converse(top),
inference(demodulation,[status(thm)],[c_5496,c_5062]) ).
tcf(c_5645,plain,
converse(converse(top)) = join(top,iPr_def_22),
inference(superposition,[status(thm)],[c_5497,c_2601]) ).
tcf(c_5648,plain,
! [X0: $i] : join(iPr_def_22,converse(join(X0,converse(top)))) = converse(join(X0,converse(top))),
inference(superposition,[status(thm)],[c_5497,c_446]) ).
tcf(c_5649,plain,
converse(converse(top)) = join(iPr_def_22,top),
inference(theory_normalisation,[status(thm)],[c_5645,c_181,c_182]) ).
tcf(c_5650,plain,
join(iPr_def_22,top) = top,
inference(demodulation,[status(thm)],[c_5649,c_177]) ).
tcf(c_5654,plain,
! [X0: $i] : join(iPr_def_22,join(top,converse(X0))) = join(top,converse(X0)),
inference(demodulation,[status(thm)],[c_5648,c_3243]) ).
tcf(c_5663,plain,
! [X0: $i] : join(iPr_def_22,join(top,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_5650,c_181]) ).
tcf(c_5667,plain,
join(top,top) = join(iPr_def_10,top),
inference(superposition,[status(thm)],[c_5650,c_2635]) ).
tcf(c_5670,plain,
join(top,top) = top,
inference(demodulation,[status(thm)],[c_5667,c_5331]) ).
tcf(c_5673,plain,
join(iPr_def_11,top) = top,
inference(demodulation,[status(thm)],[c_5469,c_5670]) ).
tcf(c_5694,plain,
join(iPr_def_15,top) = top,
inference(demodulation,[status(thm)],[c_5459,c_5673]) ).
tcf(c_5707,plain,
join(iPr_def_16,converse(iPr_def_12)) = converse(top),
inference(demodulation,[status(thm)],[c_3422,c_5673]) ).
tcf(c_5709,plain,
join(iPr_def_12,join(top,converse(complement(converse(top))))) = converse(top),
inference(demodulation,[status(thm)],[c_5475,c_5707]) ).
tcf(c_5719,plain,
join(iPr_def_12,converse(top)) = converse(top),
inference(demodulation,[status(thm)],[c_5709,c_3247]) ).
tcf(c_5720,plain,
join(iPr_def_10,join(iPr_def_16,converse(top))) = converse(top),
inference(demodulation,[status(thm)],[c_5484,c_5719]) ).
tcf(c_5722,plain,
join(iPr_def_10,converse(top)) = converse(top),
inference(demodulation,[status(thm)],[c_5720,c_5497]) ).
tcf(c_5727,plain,
join(iPr_def_17,converse(top)) = converse(converse(top)),
inference(demodulation,[status(thm)],[c_3772,c_5722]) ).
tcf(c_5731,plain,
join(iPr_def_17,converse(top)) = top,
inference(demodulation,[status(thm)],[c_5727,c_177]) ).
tcf(c_5986,plain,
join(iPr_def_18,converse(top)) = join(iPr_def_15,top),
inference(superposition,[status(thm)],[c_5731,c_2630]) ).
tcf(c_5988,plain,
join(iPr_def_18,converse(top)) = top,
inference(demodulation,[status(thm)],[c_5986,c_5694]) ).
tcf(c_5994,plain,
converse(top) = top,
inference(demodulation,[status(thm)],[c_5212,c_5988]) ).
tcf(c_6055,plain,
join(iPr_def_22,join(one,converse(complement(join(iPr_def_16,one))))) = top,
inference(demodulation,[status(thm)],[c_5054,c_5994]) ).
tcf(c_6062,plain,
join(iPr_def_18,converse(complement(converse(iPr_def_17)))) = join(iPr_def_15,top),
inference(demodulation,[status(thm)],[c_5044,c_5994]) ).
tcf(c_6069,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = top,
inference(demodulation,[status(thm)],[c_3247,c_5994]) ).
tcf(c_6075,plain,
join(iPr_def_22,converse(iPr_def_17)) = top,
inference(demodulation,[status(thm)],[c_2613,c_5994]) ).
tcf(c_6076,plain,
join(iPr_def_16,converse(iPr_def_10)) = top,
inference(demodulation,[status(thm)],[c_2594,c_5994]) ).
tcf(c_6084,plain,
join(iPr_def_18,converse(complement(converse(iPr_def_17)))) = top,
inference(demodulation,[status(thm)],[c_6062,c_5694]) ).
tcf(c_6105,plain,
! [X0: $i] : composition(top,converse(X0)) = converse(composition(X0,top)),
inference(superposition,[status(thm)],[c_5994,c_2520]) ).
tcf(c_6106,plain,
! [X0: $i] : join(complement(X0),composition(top,complement(composition(top,X0)))) = complement(X0),
inference(superposition,[status(thm)],[c_5994,c_171]) ).
tcf(c_6716,plain,
join(converse(iPr_def_18),complement(converse(iPr_def_17))) = converse(top),
inference(superposition,[status(thm)],[c_6084,c_2521]) ).
tcf(c_6717,plain,
join(converse(iPr_def_18),complement(converse(iPr_def_17))) = top,
inference(demodulation,[status(thm)],[c_6716,c_5994]) ).
tcf(c_7422,plain,
join(iPr_def_15,iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_2513,c_4287]) ).
tcf(c_7899,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(superposition,[status(thm)],[c_4065,c_4327]) ).
tcf(c_8113,plain,
! [X0: $i] : join(X0,zero) = X0,
inference(superposition,[status(thm)],[c_7899,c_182]) ).
tcf(c_8118,plain,
complement(zero) = top,
inference(superposition,[status(thm)],[c_7899,c_174]) ).
tcf(c_8155,plain,
composition(iPr_def_16,iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_7899,c_2750]) ).
tcf(c_8158,plain,
converse(complement(converse(zero))) = top,
inference(superposition,[status(thm)],[c_7899,c_6069]) ).
tcf(c_8160,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(superposition,[status(thm)],[c_7899,c_4065]) ).
tcf(c_8161,plain,
complement(iPr_def_15) = sk2,
inference(superposition,[status(thm)],[c_7899,c_4197]) ).
tcf(c_8164,plain,
complement(iPr_def_17) = iPr_def_16,
inference(superposition,[status(thm)],[c_7899,c_4200]) ).
tcf(c_8339,plain,
join(sk2,sk2) = sk2,
inference(superposition,[status(thm)],[c_8161,c_4030]) ).
tcf(c_8770,plain,
! [X0: $i] : composition(join(iPr_def_16,X0),iPr_def_10) = join(zero,composition(X0,iPr_def_10)),
inference(superposition,[status(thm)],[c_8155,c_178]) ).
tcf(c_8773,plain,
composition(converse(iPr_def_10),iPr_def_22) = converse(zero),
inference(superposition,[status(thm)],[c_8155,c_2527]) ).
tcf(c_8778,plain,
! [X0: $i] : composition(join(iPr_def_16,X0),iPr_def_10) = composition(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_8770,c_7899]) ).
tcf(c_8911,plain,
! [X0: $i] : join(sk2,join(X0,sk2)) = join(X0,sk2),
inference(superposition,[status(thm)],[c_8339,c_2484]) ).
tcf(c_8987,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(superposition,[status(thm)],[c_8160,c_4030]) ).
tcf(c_9007,plain,
! [X0: $i,X1: $i] : join(X0,join(X0,X1)) = join(X0,X1),
inference(superposition,[status(thm)],[c_8987,c_181]) ).
tcf(c_9224,plain,
complement(converse(zero)) = converse(top),
inference(superposition,[status(thm)],[c_8158,c_177]) ).
tcf(c_9246,plain,
complement(converse(zero)) = top,
inference(demodulation,[status(thm)],[c_9224,c_5994]) ).
tcf(c_9296,plain,
converse(zero) = complement(top),
inference(superposition,[status(thm)],[c_9246,c_8160]) ).
tcf(c_9302,plain,
converse(zero) = zero,
inference(demodulation,[status(thm)],[c_9296,c_2488]) ).
tcf(c_9311,plain,
composition(converse(iPr_def_10),iPr_def_22) = zero,
inference(demodulation,[status(thm)],[c_8773,c_9302]) ).
tcf(c_9483,plain,
join(complement(iPr_def_22),composition(converse(converse(iPr_def_10)),complement(zero))) = complement(iPr_def_22),
inference(superposition,[status(thm)],[c_9311,c_171]) ).
tcf(c_9490,plain,
join(iPr_def_10,composition(iPr_def_10,top)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_9483,c_177,c_2502,c_8118]) ).
tcf(c_9841,plain,
! [X0: $i,X1: $i] : join(converse(join(X0,X1)),complement(converse(X1))) = join(converse(X0),top),
inference(superposition,[status(thm)],[c_174,c_2627]) ).
tcf(c_9907,plain,
! [X0: $i,X1: $i] : join(complement(converse(X0)),converse(join(X1,X0))) = join(top,converse(X1)),
inference(theory_normalisation,[status(thm)],[c_9841,c_181,c_182]) ).
tcf(c_10156,plain,
! [X0: $i] : join(top,complement(complement(X0))) = join(X0,top),
inference(superposition,[status(thm)],[c_174,c_2628]) ).
tcf(c_10160,plain,
! [X0: $i] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(superposition,[status(thm)],[c_8987,c_2628]) ).
tcf(c_10292,plain,
! [X0: $i] : join(top,complement(X0)) = top,
inference(demodulation,[status(thm)],[c_10160,c_174]) ).
tcf(c_10293,plain,
! [X0: $i] : join(X0,top) = top,
inference(demodulation,[status(thm)],[c_10156,c_10292]) ).
tcf(c_10415,plain,
! [X0: $i,X1: $i] : join(iPr_def_16,join(X0,join(X1,iPr_def_17))) = join(X0,top),
inference(demodulation,[status(thm)],[c_4667,c_10293]) ).
tcf(c_10440,plain,
! [X0: $i,X1: $i] : join(iPr_def_16,join(X0,join(X1,iPr_def_17))) = top,
inference(demodulation,[status(thm)],[c_10415,c_10293]) ).
tcf(c_10442,plain,
! [X0: $i,X1: $i] : join(X0,join(top,X1)) = top,
inference(demodulation,[status(thm)],[c_3571,c_10440]) ).
tcf(c_10475,plain,
! [X0: $i] : join(top,X0) = top,
inference(demodulation,[status(thm)],[c_5663,c_10442]) ).
tcf(c_10476,plain,
! [X0: $i] : join(top,converse(X0)) = top,
inference(demodulation,[status(thm)],[c_5654,c_10442]) ).
tcf(c_10492,plain,
! [X0: $i,X1: $i] : join(complement(converse(X0)),converse(join(X1,X0))) = top,
inference(demodulation,[status(thm)],[c_9907,c_10476]) ).
tcf(c_12953,plain,
join(iPr_def_22,composition(join(one,converse(complement(join(iPr_def_16,one)))),top)) = composition(top,top),
inference(superposition,[status(thm)],[c_6055,c_2533]) ).
tcf(c_12957,plain,
composition(top,top) = top,
inference(demodulation,[status(thm)],[c_12953,c_4033,c_10293,c_10475]) ).
tcf(c_13054,plain,
! [X0: $i] : composition(top,composition(top,X0)) = composition(top,X0),
inference(superposition,[status(thm)],[c_12957,c_180]) ).
tcf(c_19794,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[status(thm)],[c_172,c_9007]) ).
tcf(c_20105,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(theory_normalisation,[status(thm)],[c_19794,c_181,c_182]) ).
tcf(c_26088,plain,
! [X0: $i] : join(complement(composition(top,X0)),composition(converse(top),complement(composition(top,X0)))) = complement(composition(top,X0)),
inference(superposition,[status(thm)],[c_13054,c_171]) ).
tcf(c_26099,plain,
! [X0: $i] : composition(top,complement(composition(top,X0))) = complement(composition(top,X0)),
inference(demodulation,[status(thm)],[c_26088,c_4032,c_5994,c_10475]) ).
tcf(c_26133,plain,
! [X0: $i] : join(complement(X0),complement(composition(top,X0))) = complement(X0),
inference(demodulation,[status(thm)],[c_6106,c_26099]) ).
tcf(c_29071,plain,
! [X0: $i] : join(sk2,complement(join(iPr_def_15,X0))) = sk2,
inference(superposition,[status(thm)],[c_2495,c_20105]) ).
tcf(c_29075,plain,
! [X0: $i] : join(iPr_def_18,complement(join(iPr_def_19,X0))) = iPr_def_18,
inference(superposition,[status(thm)],[c_2497,c_20105]) ).
tcf(c_29078,plain,
! [X0: $i] : join(iPr_def_22,complement(join(iPr_def_10,X0))) = iPr_def_22,
inference(superposition,[status(thm)],[c_2502,c_20105]) ).
tcf(c_29233,plain,
join(sk2,complement(iPr_def_18)) = sk2,
inference(superposition,[status(thm)],[c_7422,c_29071]) ).
tcf(c_29257,plain,
join(iPr_def_19,sk2) = sk2,
inference(demodulation,[status(thm)],[c_29233,c_182,c_2497]) ).
tcf(c_29302,plain,
! [X0: $i] : join(iPr_def_19,join(sk2,X0)) = join(sk2,X0),
inference(superposition,[status(thm)],[c_29257,c_181]) ).
tcf(c_29310,plain,
join(iPr_def_14,composition(iPr_def_19,iPr_def_13)) = composition(sk2,iPr_def_13),
inference(superposition,[status(thm)],[c_29257,c_2541]) ).
tcf(c_29314,plain,
iPr_def_14 = iPr_def_21,
inference(demodulation,[status(thm)],[c_29310,c_2514,c_2516,c_2517]) ).
tcf(c_29388,plain,
iPr_def_14 != iPr_def_20,
inference(demodulation,[status(thm)],[c_157,c_29314]) ).
tcf(c_29815,plain,
join(complement(top),complement(join(complement(converse(iPr_def_17)),complement(converse(iPr_def_18))))) = converse(iPr_def_17),
inference(superposition,[status(thm)],[c_6717,c_2840]) ).
tcf(c_29920,plain,
complement(join(complement(converse(iPr_def_17)),complement(converse(iPr_def_18)))) = converse(iPr_def_17),
inference(demodulation,[status(thm)],[c_29815,c_2488,c_7899]) ).
tcf(c_30182,plain,
join(iPr_def_22,complement(iPr_def_12)) = iPr_def_22,
inference(superposition,[status(thm)],[c_5333,c_29078]) ).
tcf(c_30213,plain,
join(iPr_def_13,iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_30182,c_182,c_2506]) ).
tcf(c_30226,plain,
join(iPr_def_16,converse(iPr_def_13)) = converse(iPr_def_22),
inference(superposition,[status(thm)],[c_30213,c_2512]) ).
tcf(c_30235,plain,
join(iPr_def_16,converse(iPr_def_13)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_30226,c_2490]) ).
tcf(c_30250,plain,
composition(converse(iPr_def_13),iPr_def_10) = composition(iPr_def_16,iPr_def_10),
inference(superposition,[status(thm)],[c_30235,c_8778]) ).
tcf(c_30261,plain,
composition(converse(iPr_def_13),iPr_def_10) = zero,
inference(demodulation,[status(thm)],[c_30250,c_8155]) ).
tcf(c_30282,plain,
composition(converse(iPr_def_10),iPr_def_13) = converse(zero),
inference(superposition,[status(thm)],[c_30261,c_2522]) ).
tcf(c_30287,plain,
composition(converse(iPr_def_10),iPr_def_13) = zero,
inference(demodulation,[status(thm)],[c_30282,c_9302]) ).
tcf(c_35462,plain,
join(complement(join(iPr_def_10,converse(iPr_def_17))),complement(join(iPr_def_22,converse(iPr_def_17)))) = join(complement(converse(iPr_def_17)),complement(converse(iPr_def_18))),
inference(superposition,[status(thm)],[c_29920,c_2875]) ).
tcf(c_35485,plain,
join(complement(converse(iPr_def_17)),complement(converse(iPr_def_18))) = complement(converse(iPr_def_17)),
inference(superposition,[status(thm)],[c_29920,c_8160]) ).
tcf(c_35525,plain,
join(complement(join(iPr_def_10,converse(iPr_def_17))),complement(join(iPr_def_22,converse(iPr_def_17)))) = complement(converse(iPr_def_17)),
inference(demodulation,[status(thm)],[c_35462,c_35485]) ).
tcf(c_35526,plain,
complement(join(iPr_def_10,converse(iPr_def_17))) = complement(converse(iPr_def_17)),
inference(demodulation,[status(thm)],[c_35525,c_2488,c_6075,c_8113]) ).
tcf(c_36423,plain,
join(complement(join(iPr_def_15,iPr_def_17)),complement(join(sk2,iPr_def_17))) = iPr_def_16,
inference(superposition,[status(thm)],[c_2491,c_2881]) ).
tcf(c_36462,plain,
join(complement(join(iPr_def_15,iPr_def_17)),complement(join(iPr_def_17,sk2))) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_36423,c_181,c_182]) ).
tcf(c_36463,plain,
join(iPr_def_19,complement(join(iPr_def_17,sk2))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_36462,c_2497,c_2513]) ).
tcf(c_36516,plain,
join(complement(join(iPr_def_18,complement(join(iPr_def_17,sk2)))),complement(iPr_def_16)) = join(iPr_def_17,sk2),
inference(superposition,[status(thm)],[c_36463,c_2877]) ).
tcf(c_36523,plain,
join(complement(iPr_def_16),complement(join(iPr_def_18,complement(join(iPr_def_17,sk2))))) = join(iPr_def_17,sk2),
inference(theory_normalisation,[status(thm)],[c_36516,c_181,c_182]) ).
tcf(c_36524,plain,
join(iPr_def_17,complement(join(iPr_def_18,complement(join(iPr_def_17,sk2))))) = join(iPr_def_17,sk2),
inference(demodulation,[status(thm)],[c_36523,c_2491]) ).
tcf(c_36556,plain,
join(iPr_def_10,converse(iPr_def_17)) = complement(complement(converse(iPr_def_17))),
inference(superposition,[status(thm)],[c_35526,c_8160]) ).
tcf(c_36565,plain,
join(iPr_def_22,complement(converse(iPr_def_17))) = iPr_def_22,
inference(superposition,[status(thm)],[c_35526,c_29078]) ).
tcf(c_36566,plain,
join(iPr_def_10,converse(iPr_def_17)) = converse(iPr_def_17),
inference(demodulation,[status(thm)],[c_36556,c_8160]) ).
tcf(c_36632,plain,
join(iPr_def_16,converse(complement(converse(iPr_def_17)))) = converse(iPr_def_22),
inference(superposition,[status(thm)],[c_36565,c_2510]) ).
tcf(c_36643,plain,
join(iPr_def_16,converse(complement(converse(iPr_def_17)))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_36632,c_2490]) ).
tcf(c_36654,plain,
join(converse(iPr_def_10),iPr_def_17) = converse(converse(iPr_def_17)),
inference(superposition,[status(thm)],[c_36566,c_2521]) ).
tcf(c_36659,plain,
join(iPr_def_17,converse(iPr_def_10)) = converse(converse(iPr_def_17)),
inference(theory_normalisation,[status(thm)],[c_36654,c_181,c_182]) ).
tcf(c_36660,plain,
join(iPr_def_17,converse(iPr_def_10)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_36659,c_177]) ).
tcf(c_36756,plain,
composition(converse(complement(converse(iPr_def_17))),iPr_def_10) = composition(iPr_def_16,iPr_def_10),
inference(superposition,[status(thm)],[c_36643,c_8778]) ).
tcf(c_36767,plain,
composition(converse(complement(converse(iPr_def_17))),iPr_def_10) = zero,
inference(demodulation,[status(thm)],[c_36756,c_8155]) ).
tcf(c_36809,plain,
join(complement(converse(converse(complement(converse(iPr_def_17))))),composition(iPr_def_10,complement(converse(zero)))) = complement(converse(converse(complement(converse(iPr_def_17))))),
inference(superposition,[status(thm)],[c_36767,c_2754]) ).
tcf(c_36848,plain,
join(composition(iPr_def_10,complement(converse(zero))),complement(converse(converse(complement(converse(iPr_def_17)))))) = complement(converse(converse(complement(converse(iPr_def_17))))),
inference(theory_normalisation,[status(thm)],[c_36809,c_181,c_182]) ).
tcf(c_36849,plain,
join(converse(iPr_def_17),composition(iPr_def_10,top)) = converse(iPr_def_17),
inference(demodulation,[status(thm)],[c_36848,c_182,c_177,c_8118,c_8160,c_9302]) ).
tcf(c_37405,plain,
! [X0: $i] : join(iPr_def_18,complement(join(sk2,X0))) = iPr_def_18,
inference(superposition,[status(thm)],[c_29302,c_29075]) ).
tcf(c_37456,plain,
! [X0: $i] : join(iPr_def_18,complement(join(X0,sk2))) = iPr_def_18,
inference(superposition,[status(thm)],[c_8911,c_37405]) ).
tcf(c_37502,plain,
join(iPr_def_17,complement(iPr_def_18)) = join(iPr_def_17,sk2),
inference(demodulation,[status(thm)],[c_36524,c_37456]) ).
tcf(c_37503,plain,
join(iPr_def_17,sk2) = join(iPr_def_17,iPr_def_19),
inference(demodulation,[status(thm)],[c_37502,c_2497]) ).
tcf(c_37518,plain,
composition(join(iPr_def_17,iPr_def_19),iPr_def_13) = join(iPr_def_14,composition(iPr_def_17,iPr_def_13)),
inference(superposition,[status(thm)],[c_37503,c_2541]) ).
tcf(c_64134,plain,
join(complement(converse(composition(iPr_def_10,top))),converse(iPr_def_10)) = top,
inference(superposition,[status(thm)],[c_9490,c_10492]) ).
tcf(c_64241,plain,
join(complement(converse(composition(iPr_def_10,top))),converse(converse(iPr_def_17))) = top,
inference(superposition,[status(thm)],[c_36849,c_10492]) ).
tcf(c_64597,plain,
join(converse(iPr_def_10),complement(converse(composition(iPr_def_10,top)))) = top,
inference(theory_normalisation,[status(thm)],[c_64134,c_181,c_182]) ).
tcf(c_64598,plain,
join(converse(iPr_def_10),complement(composition(top,converse(iPr_def_10)))) = top,
inference(demodulation,[status(thm)],[c_64597,c_6105]) ).
tcf(c_64761,plain,
join(converse(converse(iPr_def_17)),complement(converse(composition(iPr_def_10,top)))) = top,
inference(theory_normalisation,[status(thm)],[c_64241,c_181,c_182]) ).
tcf(c_64762,plain,
join(iPr_def_17,complement(composition(top,converse(iPr_def_10)))) = top,
inference(demodulation,[status(thm)],[c_64761,c_177,c_6105]) ).
tcf(c_69691,plain,
join(complement(join(iPr_def_16,complement(composition(top,converse(iPr_def_10))))),complement(top)) = composition(top,converse(iPr_def_10)),
inference(superposition,[status(thm)],[c_64762,c_2878]) ).
tcf(c_69703,plain,
join(complement(top),complement(join(iPr_def_16,complement(composition(top,converse(iPr_def_10)))))) = composition(top,converse(iPr_def_10)),
inference(theory_normalisation,[status(thm)],[c_69691,c_181,c_182]) ).
tcf(c_69704,plain,
complement(join(iPr_def_16,complement(composition(top,converse(iPr_def_10))))) = composition(top,converse(iPr_def_10)),
inference(demodulation,[status(thm)],[c_69703,c_2488,c_7899]) ).
tcf(c_71065,plain,
join(complement(top),complement(join(complement(composition(top,converse(iPr_def_10))),complement(converse(iPr_def_10))))) = composition(top,converse(iPr_def_10)),
inference(superposition,[status(thm)],[c_64598,c_2840]) ).
tcf(c_71084,plain,
join(complement(top),complement(join(complement(converse(iPr_def_10)),complement(composition(top,converse(iPr_def_10)))))) = composition(top,converse(iPr_def_10)),
inference(theory_normalisation,[status(thm)],[c_71065,c_181,c_182]) ).
tcf(c_71085,plain,
composition(top,converse(iPr_def_10)) = converse(iPr_def_10),
inference(demodulation,[status(thm)],[c_71084,c_2488,c_7899,c_8160,c_26133]) ).
tcf(c_71099,plain,
complement(join(iPr_def_16,complement(converse(iPr_def_10)))) = converse(iPr_def_10),
inference(demodulation,[status(thm)],[c_69704,c_71085]) ).
tcf(c_71945,plain,
join(complement(join(iPr_def_16,converse(iPr_def_10))),complement(join(iPr_def_17,converse(iPr_def_10)))) = join(iPr_def_16,complement(converse(iPr_def_10))),
inference(superposition,[status(thm)],[c_71099,c_2878]) ).
tcf(c_71970,plain,
join(iPr_def_16,complement(converse(iPr_def_10))) = complement(converse(iPr_def_10)),
inference(superposition,[status(thm)],[c_71099,c_8160]) ).
tcf(c_72007,plain,
join(complement(join(iPr_def_16,converse(iPr_def_10))),complement(join(iPr_def_17,converse(iPr_def_10)))) = complement(converse(iPr_def_10)),
inference(demodulation,[status(thm)],[c_71945,c_71970]) ).
tcf(c_72008,plain,
complement(converse(iPr_def_10)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_72007,c_2488,c_6076,c_7899,c_8164,c_36660]) ).
tcf(c_72050,plain,
complement(complement(converse(iPr_def_10))) = converse(iPr_def_10),
inference(demodulation,[status(thm)],[c_71099,c_71970]) ).
tcf(c_72051,plain,
converse(iPr_def_10) = complement(iPr_def_16),
inference(demodulation,[status(thm)],[c_72050,c_72008]) ).
tcf(c_72052,plain,
converse(iPr_def_10) = iPr_def_17,
inference(demodulation,[status(thm)],[c_72051,c_2491]) ).
tcf(c_72345,plain,
composition(iPr_def_17,iPr_def_13) = zero,
inference(demodulation,[status(thm)],[c_30287,c_72052]) ).
tcf(c_72537,plain,
composition(join(iPr_def_17,iPr_def_19),iPr_def_13) = join(iPr_def_14,zero),
inference(demodulation,[status(thm)],[c_37518,c_72345]) ).
tcf(c_72538,plain,
composition(join(iPr_def_17,iPr_def_19),iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_72537,c_8113]) ).
tcf(c_73708,plain,
join(iPr_def_20,composition(iPr_def_17,iPr_def_13)) = iPr_def_14,
inference(superposition,[status(thm)],[c_72538,c_2540]) ).
tcf(c_73714,plain,
iPr_def_14 = iPr_def_20,
inference(demodulation,[status(thm)],[c_73708,c_8113,c_72345]) ).
tcf(c_73908,plain,
iPr_def_14 != iPr_def_14,
inference(demodulation,[status(thm)],[c_29388,c_73714]) ).
tcf(c_74124,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_73908]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL034-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.37 % Computer : n014.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:29:24 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/5.41 Running UEQ theorem proving
% 0.15/5.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.42
% 0.15/5.42 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.42
% 0.15/5.42 % Detected problem language: tptp
% 0.15/5.44 % Proving...
% 244.02/39.47 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 244.02/39.47 % SZS status Started for theBenchmark.p
% 244.02/39.47 % SZS status Unsatisfiable for theBenchmark.p
% 244.02/39.47
% 244.02/39.47 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 244.02/39.47
% 244.02/39.47 % ------ iProver source info
% 244.02/39.47
% 244.02/39.47 % git: date: 2026-07-19 20:42:38 +0200
% 244.02/39.47 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 244.02/39.47 % git: non_committed_changes: false
% 244.02/39.47
% 244.02/39.47 % ------ Parsing...% successful
% 244.02/39.47
% 244.02/39.47
% 244.02/39.47 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 244.02/39.47
% 244.02/39.47 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 244.02/39.47
% 244.02/39.47 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 244.02/39.47
% 244.02/39.47 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 244.02/39.47 % ------ Proving...
% 244.02/39.47 % ------ Problem Properties
% 244.02/39.47
% 244.02/39.47 %
% 244.02/39.47 % clauses 40
% 244.02/39.47 % conjectures 2
% 244.02/39.47 % EPR 15
% 244.02/39.47 % Horn 40
% 244.02/39.47 % unary 40
% 244.02/39.47 % binary 0
% 244.02/39.47 % lits 40
% 244.02/39.47 % lits eq 40
% 244.02/39.47 % fd_pure 0
% 244.02/39.47 % fd_pseudo 0
% 244.02/39.47 % fd_cond 0
% 244.02/39.47 % fd_pseudo_cond 0
% 244.02/39.47 % AC symbols 1
% 244.02/39.47
% 244.02/39.47 % ------ Input Options Time Limit: Unbounded
% 244.02/39.47
% 244.02/39.47
% 244.02/39.47 % ------
% 244.02/39.47 % Current options:
% 244.02/39.47 % ------
% 244.02/39.47
% 244.02/39.47
% 244.02/39.47 %
% 244.02/39.47
% 244.02/39.47 % ------ Proving...
% 244.02/39.47 %
% 244.02/39.47
% 244.02/39.47 % SZS status Unsatisfiable for theBenchmark.p
% 244.02/39.47
% 244.02/39.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 244.02/39.48
% 244.02/39.48
%------------------------------------------------------------------------------