%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL021-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 : 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:51 PM UTC 2026
% Result : Unsatisfiable 185.94s 24.96s
% Output : CNFRefutation 185.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 25
% Syntax : Number of formulae : 306 ( 306 unt; 10 def)
% Number of atoms : 781 ( 305 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 : 9 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 11 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 201 ( 0 sgn 201 !; 0 ?; 169 :)
% 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(meet(sk1,one),sk2),meet(sk1,sk2)) != meet(sk1,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
meet(sk1,sk2) != join(composition(meet(sk1,one),sk2),meet(sk1,sk2)),
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f22,plain,
complement(join(complement(sk1),complement(sk2))) != join(composition(complement(join(complement(sk1),complement(one))),sk2),complement(join(complement(sk1),complement(sk2)))),
inference(definition_unfolding,[],[f20,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(complement(join(complement(sk1),complement(one))),sk2),complement(join(complement(sk1),complement(sk2)))) != complement(join(complement(sk1),complement(sk2))),
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_92,negated_conjecture,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(one))),sk2)) != complement(join(complement(sk1),complement(sk2))),
inference(theory_normalisation,[status(thm)],[c_77,c_65,c_64]) ).
tcf(c_123,plain,
complement(top) = zero,
inference(demodulation,[status(thm)],[c_75,c_74]) ).
tcf(c_130,definition,
iPr_def_10 = complement(sk1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_131,definition,
iPr_def_11 = complement(sk2),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_132,definition,
iPr_def_12 = join(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_133,definition,
iPr_def_13 = complement(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_134,definition,
iPr_def_14 = complement(one),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_135,definition,
iPr_def_15 = join(iPr_def_10,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_136,definition,
iPr_def_16 = complement(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_137,definition,
iPr_def_17 = composition(iPr_def_16,sk2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_138,definition,
iPr_def_18 = join(iPr_def_13,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_139,definition,
iPr_def_19 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_140,negated_conjecture,
iPr_def_18 != iPr_def_13,
inference(demodulation,[status(thm)],[c_92,c_134,c_135,c_136,c_137,c_131,c_130,c_132,c_133,c_138]) ).
tcf(c_141,negated_conjecture,
iPr_def_19 = sk1,
inference(demodulation,[status(thm)],[c_76,c_139]) ).
tcf(c_228,plain,
complement(iPr_def_19) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_130,c_141]) ).
tcf(c_229,plain,
composition(iPr_def_19,top) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_139,c_141]) ).
tcf(c_230,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_65,c_64]) ).
tcf(c_237,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_11,X0)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_132,c_65]) ).
tcf(c_240,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_14,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_135,c_65]) ).
tcf(c_243,plain,
! [X0: $i] : join(iPr_def_13,join(iPr_def_17,X0)) = join(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_138,c_65]) ).
tcf(c_259,plain,
join(sk2,iPr_def_11) = top,
inference(superposition,[status(thm)],[c_131,c_74]) ).
tcf(c_260,plain,
join(one,iPr_def_14) = top,
inference(superposition,[status(thm)],[c_134,c_74]) ).
tcf(c_261,plain,
join(top,zero) = top,
inference(superposition,[status(thm)],[c_123,c_74]) ).
tcf(c_264,plain,
join(iPr_def_19,iPr_def_10) = top,
inference(superposition,[status(thm)],[c_228,c_74]) ).
tcf(c_265,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[status(thm)],[c_74,c_65]) ).
tcf(c_266,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(join(X0,X1)))) = top,
inference(superposition,[status(thm)],[c_74,c_65]) ).
tcf(c_267,plain,
join(iPr_def_10,iPr_def_19) = top,
inference(demodulation,[status(thm)],[c_264,c_64]) ).
tcf(c_268,plain,
join(iPr_def_14,one) = top,
inference(demodulation,[status(thm)],[c_260,c_64]) ).
tcf(c_269,plain,
join(iPr_def_11,sk2) = top,
inference(demodulation,[status(thm)],[c_259,c_64]) ).
tcf(c_279,plain,
! [X0: $i,X1: $i] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(superposition,[status(thm)],[c_68,c_67]) ).
tcf(c_285,plain,
! [X0: $i] : join(top,join(zero,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_261,c_65]) ).
tcf(c_294,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_19,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_267,c_65]) ).
tcf(c_297,plain,
! [X0: $i] : join(iPr_def_14,join(one,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_268,c_65]) ).
tcf(c_307,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_11)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_64,c_237]) ).
tcf(c_310,plain,
join(iPr_def_10,top) = join(iPr_def_12,sk2),
inference(superposition,[status(thm)],[c_269,c_237]) ).
tcf(c_343,plain,
! [X0: $i] : composition(join(iPr_def_16,X0),sk2) = join(iPr_def_17,composition(X0,sk2)),
inference(superposition,[status(thm)],[c_137,c_69]) ).
tcf(c_365,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_14)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_64,c_240]) ).
tcf(c_368,plain,
join(iPr_def_10,top) = join(iPr_def_15,one),
inference(superposition,[status(thm)],[c_268,c_240]) ).
tcf(c_387,plain,
join(iPr_def_18,complement(iPr_def_17)) = join(iPr_def_13,top),
inference(superposition,[status(thm)],[c_74,c_243]) ).
tcf(c_432,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_70,c_71]) ).
tcf(c_433,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(superposition,[status(thm)],[c_70,c_71]) ).
tcf(c_466,plain,
! [X0: $i] : join(top,join(X0,zero)) = join(top,X0),
inference(superposition,[status(thm)],[c_64,c_285]) ).
tcf(c_525,plain,
! [X0: $i,X1: $i] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(superposition,[status(thm)],[c_70,c_72]) ).
tcf(c_526,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_70,c_72]) ).
tcf(c_527,plain,
! [X0: $i,X1: $i,X2: $i] : join(converse(composition(X0,X1)),composition(X2,converse(X0))) = composition(join(converse(X1),X2),converse(X0)),
inference(superposition,[status(thm)],[c_72,c_69]) ).
tcf(c_596,plain,
join(top,iPr_def_11) = join(iPr_def_12,iPr_def_19),
inference(superposition,[status(thm)],[c_307,c_294]) ).
tcf(c_597,plain,
join(iPr_def_11,top) = join(iPr_def_12,iPr_def_19),
inference(demodulation,[status(thm)],[c_596,c_64]) ).
tcf(c_638,plain,
join(top,iPr_def_14) = join(iPr_def_15,iPr_def_19),
inference(superposition,[status(thm)],[c_365,c_294]) ).
tcf(c_639,plain,
join(iPr_def_14,top) = join(iPr_def_15,iPr_def_19),
inference(demodulation,[status(thm)],[c_638,c_64]) ).
tcf(c_702,plain,
! [X0: $i,X1: $i] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[status(thm)],[c_64,c_90]) ).
tcf(c_714,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_74,c_90]) ).
tcf(c_716,plain,
! [X0: $i] : join(complement(join(iPr_def_11,X0)),complement(join(iPr_def_11,complement(X0)))) = sk2,
inference(superposition,[status(thm)],[c_131,c_90]) ).
tcf(c_718,plain,
! [X0: $i] : join(complement(join(zero,X0)),complement(join(zero,complement(X0)))) = top,
inference(superposition,[status(thm)],[c_123,c_90]) ).
tcf(c_719,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_133,c_90]) ).
tcf(c_721,plain,
! [X0: $i] : join(complement(join(iPr_def_10,X0)),complement(join(iPr_def_10,complement(X0)))) = iPr_def_19,
inference(superposition,[status(thm)],[c_228,c_90]) ).
tcf(c_724,plain,
! [X0: $i] : join(complement(join(complement(X0),top)),complement(join(complement(X0),zero))) = X0,
inference(superposition,[status(thm)],[c_123,c_90]) ).
tcf(c_725,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_12)),complement(join(complement(X0),iPr_def_13))) = X0,
inference(superposition,[status(thm)],[c_133,c_90]) ).
tcf(c_726,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_15)),complement(join(complement(X0),iPr_def_16))) = X0,
inference(superposition,[status(thm)],[c_136,c_90]) ).
tcf(c_730,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(complement(join(complement(X0),X1)),complement(complement(join(complement(X0),complement(X1))))))) = join(complement(X0),X1),
inference(superposition,[status(thm)],[c_90,c_90]) ).
tcf(c_731,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_714,c_64]) ).
tcf(c_732,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_731,c_123]) ).
tcf(c_734,plain,
! [X0: $i] : join(complement(join(iPr_def_15,complement(X0))),complement(join(iPr_def_16,complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_726,c_64]) ).
tcf(c_735,plain,
! [X0: $i] : join(complement(join(iPr_def_12,complement(X0))),complement(join(iPr_def_13,complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_725,c_64]) ).
tcf(c_736,plain,
! [X0: $i] : join(complement(join(top,complement(X0))),complement(join(zero,complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_724,c_64]) ).
tcf(c_909,plain,
! [X0: $i] : join(complement(one),composition(converse(X0),complement(X0))) = complement(one),
inference(superposition,[status(thm)],[c_68,c_91]) ).
tcf(c_921,plain,
! [X0: $i] : join(iPr_def_14,composition(converse(X0),complement(X0))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_909,c_134]) ).
tcf(c_981,plain,
join(iPr_def_14,composition(converse(one),iPr_def_14)) = iPr_def_14,
inference(superposition,[status(thm)],[c_134,c_921]) ).
tcf(c_1001,plain,
join(iPr_def_15,composition(converse(one),iPr_def_14)) = join(iPr_def_10,iPr_def_14),
inference(superposition,[status(thm)],[c_981,c_240]) ).
tcf(c_1002,plain,
join(iPr_def_15,composition(converse(one),iPr_def_14)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_1001,c_135]) ).
tcf(c_1316,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X0))) = join(X1,top),
inference(superposition,[status(thm)],[c_74,c_230]) ).
tcf(c_1318,plain,
! [X0: $i,X1: $i,X2: $i] : join(complement(X0),join(X1,composition(converse(X2),complement(composition(X2,X0))))) = join(X1,complement(X0)),
inference(superposition,[status(thm)],[c_91,c_230]) ).
tcf(c_1321,plain,
! [X0: $i] : join(iPr_def_13,join(X0,iPr_def_17)) = join(X0,iPr_def_18),
inference(superposition,[status(thm)],[c_138,c_230]) ).
tcf(c_1325,plain,
! [X0: $i] : join(top,join(X0,zero)) = join(X0,top),
inference(superposition,[status(thm)],[c_261,c_230]) ).
tcf(c_1383,plain,
! [X0: $i,X1: $i,X2: $i] : join(complement(join(X0,join(complement(X1),X2))),complement(join(complement(X1),complement(join(X0,X2))))) = X1,
inference(superposition,[status(thm)],[c_230,c_90]) ).
tcf(c_1617,plain,
! [X0: $i] : join(top,complement(complement(X0))) = join(X0,top),
inference(superposition,[status(thm)],[c_74,c_265]) ).
tcf(c_2042,plain,
join(iPr_def_15,join(composition(converse(one),iPr_def_14),complement(iPr_def_15))) = top,
inference(superposition,[status(thm)],[c_1002,c_266]) ).
tcf(c_2109,plain,
join(top,composition(converse(one),iPr_def_14)) = top,
inference(demodulation,[status(thm)],[c_2042,c_64,c_265]) ).
tcf(c_5356,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[status(thm)],[c_74,c_432]) ).
tcf(c_5709,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_68,c_526]) ).
tcf(c_5735,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(demodulation,[status(thm)],[c_5709,c_70]) ).
tcf(c_5748,plain,
join(top,iPr_def_14) = top,
inference(demodulation,[status(thm)],[c_2109,c_5735]) ).
tcf(c_5750,plain,
join(iPr_def_14,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_981,c_5735]) ).
tcf(c_5752,plain,
join(iPr_def_14,top) = top,
inference(demodulation,[status(thm)],[c_5748,c_64]) ).
tcf(c_5754,plain,
join(iPr_def_15,iPr_def_19) = top,
inference(demodulation,[status(thm)],[c_639,c_5752]) ).
tcf(c_5961,plain,
! [X0: $i] : join(iPr_def_14,join(iPr_def_14,X0)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_5750,c_65]) ).
tcf(c_6086,plain,
converse(one) = one,
inference(superposition,[status(thm)],[c_5735,c_68]) ).
tcf(c_6091,plain,
! [X0: $i] : composition(converse(one),X0) = composition(one,X0),
inference(superposition,[status(thm)],[c_5735,c_279]) ).
tcf(c_6116,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(demodulation,[status(thm)],[c_6091,c_5735]) ).
tcf(c_6129,plain,
join(one,converse(complement(one))) = converse(top),
inference(superposition,[status(thm)],[c_6086,c_5356]) ).
tcf(c_6149,plain,
join(one,converse(iPr_def_14)) = converse(top),
inference(light_normalisation,[status(thm)],[c_6129,c_134]) ).
tcf(c_6535,plain,
join(top,converse(iPr_def_14)) = join(iPr_def_14,converse(top)),
inference(superposition,[status(thm)],[c_6149,c_297]) ).
tcf(c_6694,plain,
join(iPr_def_14,converse(top)) = converse(top),
inference(superposition,[status(thm)],[c_5356,c_5961]) ).
tcf(c_6723,plain,
join(converse(iPr_def_14),top) = converse(converse(top)),
inference(superposition,[status(thm)],[c_6694,c_433]) ).
tcf(c_6724,plain,
join(top,converse(iPr_def_14)) = top,
inference(demodulation,[status(thm)],[c_6723,c_64,c_70]) ).
tcf(c_7686,plain,
converse(top) = top,
inference(light_normalisation,[status(thm)],[c_6535,c_6694,c_6724]) ).
tcf(c_7698,plain,
! [X0: $i] : composition(top,converse(X0)) = converse(composition(X0,top)),
inference(superposition,[status(thm)],[c_7686,c_525]) ).
tcf(c_9171,plain,
composition(top,converse(iPr_def_19)) = converse(iPr_def_19),
inference(superposition,[status(thm)],[c_229,c_7698]) ).
tcf(c_10179,plain,
join(zero,complement(join(iPr_def_14,iPr_def_14))) = one,
inference(superposition,[status(thm)],[c_134,c_732]) ).
tcf(c_10181,plain,
join(zero,complement(join(iPr_def_13,iPr_def_13))) = iPr_def_12,
inference(superposition,[status(thm)],[c_133,c_732]) ).
tcf(c_10190,plain,
join(zero,complement(iPr_def_14)) = one,
inference(light_normalisation,[status(thm)],[c_10179,c_5750]) ).
tcf(c_10398,plain,
! [X0: $i] : join(join(complement(X0),complement(X0)),X0) = join(zero,top),
inference(superposition,[status(thm)],[c_732,c_1316]) ).
tcf(c_10585,plain,
! [X0: $i] : join(top,complement(X0)) = join(top,zero),
inference(demodulation,[status(thm)],[c_10398,c_64,c_65,c_74]) ).
tcf(c_10586,plain,
! [X0: $i] : join(top,complement(X0)) = top,
inference(light_normalisation,[status(thm)],[c_10585,c_261]) ).
tcf(c_10651,plain,
! [X0: $i] : join(X0,top) = top,
inference(demodulation,[status(thm)],[c_1617,c_10586]) ).
tcf(c_10680,plain,
! [X0: $i] : join(top,join(X0,zero)) = top,
inference(demodulation,[status(thm)],[c_1325,c_10651]) ).
tcf(c_10681,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X0))) = top,
inference(demodulation,[status(thm)],[c_1316,c_10651]) ).
tcf(c_10684,plain,
join(iPr_def_15,one) = top,
inference(demodulation,[status(thm)],[c_368,c_10651]) ).
tcf(c_10686,plain,
join(iPr_def_12,sk2) = top,
inference(demodulation,[status(thm)],[c_310,c_10651]) ).
tcf(c_10688,plain,
join(iPr_def_12,iPr_def_19) = top,
inference(demodulation,[status(thm)],[c_597,c_10651]) ).
tcf(c_10689,plain,
join(iPr_def_18,complement(iPr_def_17)) = top,
inference(demodulation,[status(thm)],[c_387,c_10651]) ).
tcf(c_10697,plain,
! [X0: $i] : join(top,X0) = top,
inference(demodulation,[status(thm)],[c_466,c_10680]) ).
tcf(c_10718,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = top,
inference(demodulation,[status(thm)],[c_265,c_10697]) ).
tcf(c_10965,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[status(thm)],[c_10651,c_90]) ).
tcf(c_10985,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(light_normalisation,[status(thm)],[c_10965,c_123]) ).
tcf(c_10986,plain,
! [X0: $i] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_10985,c_65,c_64]) ).
tcf(c_11695,plain,
! [X0: $i] : composition(join(converse(X0),top),converse(iPr_def_19)) = join(converse(composition(iPr_def_19,X0)),converse(iPr_def_19)),
inference(superposition,[status(thm)],[c_9171,c_527]) ).
tcf(c_11715,plain,
! [X0: $i] : converse(join(iPr_def_19,composition(iPr_def_19,X0))) = composition(top,converse(iPr_def_19)),
inference(demodulation,[status(thm)],[c_11695,c_64,c_71,c_10651]) ).
tcf(c_11716,plain,
! [X0: $i] : converse(join(iPr_def_19,composition(iPr_def_19,X0))) = converse(iPr_def_19),
inference(light_normalisation,[status(thm)],[c_11715,c_9171]) ).
tcf(c_12613,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,join(X2,complement(X0)))) = top,
inference(superposition,[status(thm)],[c_65,c_10681]) ).
tcf(c_13459,plain,
join(zero,complement(top)) = zero,
inference(superposition,[status(thm)],[c_74,c_10986]) ).
tcf(c_13460,plain,
! [X0: $i] : join(complement(X0),complement(X0)) = join(zero,complement(X0)),
inference(superposition,[status(thm)],[c_732,c_10986]) ).
tcf(c_13464,plain,
join(zero,complement(iPr_def_12)) = join(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_10181,c_10986]) ).
tcf(c_13480,plain,
join(zero,zero) = zero,
inference(light_normalisation,[status(thm)],[c_13459,c_123]) ).
tcf(c_13490,plain,
join(zero,iPr_def_13) = join(iPr_def_13,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_13464,c_133]) ).
tcf(c_13491,plain,
join(iPr_def_13,zero) = join(iPr_def_13,iPr_def_13),
inference(theory_normalisation,[status(thm)],[c_13490,c_65,c_64]) ).
tcf(c_13695,plain,
! [X0: $i] : join(zero,join(zero,X0)) = join(zero,X0),
inference(superposition,[status(thm)],[c_13480,c_65]) ).
tcf(c_15461,plain,
! [X0: $i] : join(iPr_def_19,composition(iPr_def_19,X0)) = converse(converse(iPr_def_19)),
inference(superposition,[status(thm)],[c_11716,c_70]) ).
tcf(c_15470,plain,
! [X0: $i] : join(iPr_def_19,composition(iPr_def_19,X0)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_15461,c_70]) ).
tcf(c_17588,plain,
join(complement(top),complement(join(complement(iPr_def_17),complement(iPr_def_18)))) = iPr_def_17,
inference(superposition,[status(thm)],[c_10689,c_702]) ).
tcf(c_17643,plain,
join(zero,complement(join(complement(iPr_def_17),complement(iPr_def_18)))) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_17588,c_123]) ).
tcf(c_19378,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(superposition,[status(thm)],[c_10986,c_13695]) ).
tcf(c_19419,plain,
complement(iPr_def_14) = one,
inference(demodulation,[status(thm)],[c_10190,c_19378]) ).
tcf(c_19532,plain,
! [X0: $i] : join(X0,zero) = X0,
inference(superposition,[status(thm)],[c_19378,c_64]) ).
tcf(c_19537,plain,
complement(zero) = top,
inference(superposition,[status(thm)],[c_19378,c_74]) ).
tcf(c_19548,plain,
join(zero,iPr_def_18) = join(iPr_def_13,iPr_def_17),
inference(superposition,[status(thm)],[c_19378,c_1321]) ).
tcf(c_19620,plain,
join(iPr_def_13,iPr_def_17) = iPr_def_18,
inference(demodulation,[status(thm)],[c_19548,c_19378]) ).
tcf(c_19639,plain,
join(iPr_def_13,iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_13491,c_19532]) ).
tcf(c_19655,plain,
join(complement(join(iPr_def_11,zero)),complement(join(iPr_def_11,top))) = sk2,
inference(superposition,[status(thm)],[c_19537,c_716]) ).
tcf(c_19668,plain,
join(complement(top),complement(join(iPr_def_11,zero))) = sk2,
inference(demodulation,[status(thm)],[c_19655,c_64,c_10651]) ).
tcf(c_19669,plain,
join(zero,complement(join(iPr_def_11,zero))) = sk2,
inference(light_normalisation,[status(thm)],[c_19668,c_123]) ).
tcf(c_19670,plain,
complement(iPr_def_11) = sk2,
inference(ac_demodulation,[status(thm)],[c_19669,c_19378,c_19378,c_65,c_64]) ).
tcf(c_20117,plain,
! [X0: $i] : join(complement(X0),complement(join(zero,complement(X0)))) = top,
inference(light_normalisation,[status(thm)],[c_718,c_19378]) ).
tcf(c_20148,plain,
! [X0: $i] : join(complement(join(join(zero,complement(X0)),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_20117,c_702]) ).
tcf(c_20159,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_20148,c_64,c_65,c_19378]) ).
tcf(c_20160,plain,
! [X0: $i] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_20159,c_123,c_13460]) ).
tcf(c_20161,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(ac_demodulation,[status(thm)],[c_20160,c_19378,c_19378,c_65,c_64]) ).
tcf(c_20303,plain,
! [X0: $i] : join(iPr_def_13,join(iPr_def_13,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_19639,c_65]) ).
tcf(c_20456,plain,
complement(iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_133,c_20161]) ).
tcf(c_20458,plain,
complement(iPr_def_10) = iPr_def_19,
inference(superposition,[status(thm)],[c_228,c_20161]) ).
tcf(c_20459,plain,
complement(sk2) = iPr_def_11,
inference(superposition,[status(thm)],[c_19670,c_20161]) ).
tcf(c_20497,plain,
complement(iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_20456,c_20161]) ).
tcf(c_20510,plain,
join(complement(iPr_def_18),complement(join(iPr_def_13,complement(iPr_def_17)))) = iPr_def_12,
inference(superposition,[status(thm)],[c_19620,c_719]) ).
tcf(c_20517,plain,
! [X0: $i] : join(complement(top),complement(join(iPr_def_13,complement(join(X0,complement(iPr_def_13)))))) = iPr_def_12,
inference(superposition,[status(thm)],[c_10681,c_719]) ).
tcf(c_20576,plain,
! [X0: $i] : join(zero,complement(join(iPr_def_13,complement(join(X0,iPr_def_12))))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_20517,c_123,c_20456]) ).
tcf(c_20577,plain,
! [X0: $i] : complement(join(iPr_def_13,complement(join(X0,iPr_def_12)))) = iPr_def_12,
inference(ac_demodulation,[status(thm)],[c_20576,c_19378,c_65,c_64]) ).
tcf(c_23487,plain,
join(complement(join(iPr_def_15,one)),complement(join(iPr_def_16,one))) = iPr_def_14,
inference(superposition,[status(thm)],[c_19419,c_734]) ).
tcf(c_23491,plain,
join(complement(join(iPr_def_15,iPr_def_19)),complement(join(iPr_def_16,iPr_def_19))) = iPr_def_10,
inference(superposition,[status(thm)],[c_20458,c_734]) ).
tcf(c_23508,plain,
join(zero,complement(join(iPr_def_16,iPr_def_19))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_23491,c_123,c_5754]) ).
tcf(c_23509,plain,
complement(join(iPr_def_16,iPr_def_19)) = iPr_def_10,
inference(ac_demodulation,[status(thm)],[c_23508,c_19378,c_65,c_64]) ).
tcf(c_23515,plain,
join(zero,complement(join(iPr_def_16,one))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_23487,c_123,c_10684]) ).
tcf(c_23516,plain,
complement(join(iPr_def_16,one)) = iPr_def_14,
inference(ac_demodulation,[status(thm)],[c_23515,c_19378,c_65,c_64]) ).
tcf(c_23571,plain,
join(iPr_def_16,iPr_def_19) = complement(iPr_def_10),
inference(superposition,[status(thm)],[c_23509,c_20161]) ).
tcf(c_23582,plain,
join(iPr_def_16,iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_23571,c_20458]) ).
tcf(c_23843,plain,
join(iPr_def_17,composition(iPr_def_19,sk2)) = composition(iPr_def_19,sk2),
inference(superposition,[status(thm)],[c_23582,c_343]) ).
tcf(c_23861,plain,
join(iPr_def_16,one) = complement(iPr_def_14),
inference(superposition,[status(thm)],[c_23516,c_20161]) ).
tcf(c_23872,plain,
join(iPr_def_16,one) = one,
inference(light_normalisation,[status(thm)],[c_23861,c_19419]) ).
tcf(c_23896,plain,
join(iPr_def_17,composition(one,sk2)) = composition(one,sk2),
inference(superposition,[status(thm)],[c_23872,c_343]) ).
tcf(c_23904,plain,
join(iPr_def_17,sk2) = sk2,
inference(demodulation,[status(thm)],[c_23896,c_6116]) ).
tcf(c_23910,plain,
! [X0: $i] : join(iPr_def_17,join(sk2,X0)) = join(sk2,X0),
inference(superposition,[status(thm)],[c_23904,c_65]) ).
tcf(c_23914,plain,
join(iPr_def_13,sk2) = join(iPr_def_18,sk2),
inference(superposition,[status(thm)],[c_23904,c_243]) ).
tcf(c_24000,plain,
join(complement(join(iPr_def_12,sk2)),complement(join(iPr_def_13,sk2))) = iPr_def_11,
inference(superposition,[status(thm)],[c_19670,c_735]) ).
tcf(c_24005,plain,
join(complement(join(iPr_def_12,iPr_def_19)),complement(join(iPr_def_13,iPr_def_19))) = iPr_def_10,
inference(superposition,[status(thm)],[c_20458,c_735]) ).
tcf(c_24022,plain,
join(zero,complement(join(iPr_def_13,iPr_def_19))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_24005,c_123,c_10688]) ).
tcf(c_24023,plain,
complement(join(iPr_def_13,iPr_def_19)) = iPr_def_10,
inference(ac_demodulation,[status(thm)],[c_24022,c_19378,c_65,c_64]) ).
tcf(c_24028,plain,
join(zero,complement(join(iPr_def_13,sk2))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_24000,c_123,c_10686]) ).
tcf(c_24029,plain,
complement(join(iPr_def_13,sk2)) = iPr_def_11,
inference(ac_demodulation,[status(thm)],[c_24028,c_19378,c_65,c_64]) ).
tcf(c_24081,plain,
join(iPr_def_13,iPr_def_19) = complement(iPr_def_10),
inference(superposition,[status(thm)],[c_24023,c_20161]) ).
tcf(c_24092,plain,
join(iPr_def_13,iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_24081,c_20458]) ).
tcf(c_24347,plain,
join(iPr_def_13,sk2) = complement(iPr_def_11),
inference(superposition,[status(thm)],[c_24029,c_20161]) ).
tcf(c_24358,plain,
join(iPr_def_13,sk2) = sk2,
inference(light_normalisation,[status(thm)],[c_24347,c_19670]) ).
tcf(c_24372,plain,
join(iPr_def_18,sk2) = sk2,
inference(demodulation,[status(thm)],[c_23914,c_24358]) ).
tcf(c_24391,plain,
! [X0: $i] : join(iPr_def_18,join(sk2,X0)) = join(sk2,X0),
inference(superposition,[status(thm)],[c_24372,c_65]) ).
tcf(c_24561,plain,
! [X0: $i] : join(complement(join(top,complement(X0))),complement(join(complement(join(complement(join(top,complement(X0))),join(zero,complement(X0)))),complement(complement(X0))))) = join(complement(join(top,complement(X0))),join(zero,complement(X0))),
inference(superposition,[status(thm)],[c_736,c_730]) ).
tcf(c_24650,plain,
! [X0: $i] : join(complement(top),complement(join(X0,complement(join(complement(X0),complement(top)))))) = join(complement(X0),complement(top)),
inference(demodulation,[status(thm)],[c_24561,c_64,c_230,c_10697,c_20161,c_19378]) ).
tcf(c_24651,plain,
! [X0: $i] : join(zero,complement(join(X0,complement(join(complement(X0),zero))))) = join(complement(X0),zero),
inference(light_normalisation,[status(thm)],[c_24650,c_123]) ).
tcf(c_24652,plain,
! [X0: $i] : join(zero,complement(join(X0,complement(join(zero,complement(X0)))))) = join(zero,complement(X0)),
inference(theory_normalisation,[status(thm)],[c_24651,c_65,c_64]) ).
tcf(c_24653,plain,
! [X0: $i] : complement(join(X0,complement(complement(X0)))) = complement(X0),
inference(ac_demodulation,[status(thm)],[c_24652,c_19378,c_19378,c_19378,c_65,c_64]) ).
tcf(c_29632,plain,
join(iPr_def_13,iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_19620,c_20303]) ).
tcf(c_30801,plain,
! [X0: $i] : join(iPr_def_13,complement(join(X0,iPr_def_12))) = complement(iPr_def_12),
inference(superposition,[status(thm)],[c_20577,c_20161]) ).
tcf(c_30816,plain,
! [X0: $i] : join(iPr_def_13,complement(join(X0,iPr_def_12))) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_30801,c_20497]) ).
tcf(c_30849,plain,
! [X0: $i] : join(iPr_def_13,complement(join(iPr_def_12,X0))) = iPr_def_13,
inference(superposition,[status(thm)],[c_64,c_30816]) ).
tcf(c_34136,plain,
join(sk2,complement(iPr_def_17)) = top,
inference(superposition,[status(thm)],[c_23910,c_10681]) ).
tcf(c_34167,plain,
! [X0: $i] : join(sk2,join(complement(iPr_def_17),X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_34136,c_65]) ).
tcf(c_34181,plain,
! [X0: $i] : join(sk2,join(complement(iPr_def_17),X0)) = top,
inference(demodulation,[status(thm)],[c_34167,c_10697]) ).
tcf(c_34875,plain,
join(sk2,complement(iPr_def_18)) = top,
inference(superposition,[status(thm)],[c_24391,c_10681]) ).
tcf(c_34906,plain,
! [X0: $i] : join(sk2,join(complement(iPr_def_18),X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_34875,c_65]) ).
tcf(c_34921,plain,
! [X0: $i] : join(sk2,join(complement(iPr_def_18),X0)) = top,
inference(demodulation,[status(thm)],[c_34906,c_10697]) ).
tcf(c_35095,plain,
! [X0: $i] : complement(join(X0,X0)) = complement(X0),
inference(light_normalisation,[status(thm)],[c_24653,c_20161]) ).
tcf(c_35109,plain,
! [X0: $i] : join(X0,X0) = complement(complement(X0)),
inference(superposition,[status(thm)],[c_35095,c_20161]) ).
tcf(c_35148,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_35109,c_20161]) ).
tcf(c_35200,plain,
! [X0: $i,X1: $i] : join(X0,join(X0,X1)) = join(X0,X1),
inference(superposition,[status(thm)],[c_35148,c_65]) ).
tcf(c_40153,plain,
! [X0: $i] : join(complement(join(iPr_def_13,X0)),iPr_def_12) = iPr_def_12,
inference(superposition,[status(thm)],[c_719,c_35200]) ).
tcf(c_40489,plain,
! [X0: $i] : join(iPr_def_12,complement(join(iPr_def_13,X0))) = iPr_def_12,
inference(demodulation,[status(thm)],[c_40153,c_64]) ).
tcf(c_41041,plain,
join(iPr_def_12,complement(iPr_def_18)) = iPr_def_12,
inference(superposition,[status(thm)],[c_29632,c_40489]) ).
tcf(c_64914,plain,
join(complement(join(top,complement(join(complement(iPr_def_17),complement(iPr_def_18))))),complement(iPr_def_17)) = join(complement(iPr_def_17),complement(iPr_def_18)),
inference(superposition,[status(thm)],[c_17643,c_736]) ).
tcf(c_64929,plain,
join(complement(iPr_def_17),complement(top)) = join(complement(iPr_def_17),complement(iPr_def_18)),
inference(demodulation,[status(thm)],[c_64914,c_64,c_10697]) ).
tcf(c_64930,plain,
join(complement(iPr_def_17),complement(iPr_def_18)) = join(complement(iPr_def_17),zero),
inference(light_normalisation,[status(thm)],[c_64929,c_123]) ).
tcf(c_64931,plain,
join(complement(iPr_def_17),complement(iPr_def_18)) = join(zero,complement(iPr_def_17)),
inference(theory_normalisation,[status(thm)],[c_64930,c_65,c_64]) ).
tcf(c_64932,plain,
join(complement(iPr_def_17),complement(iPr_def_18)) = complement(iPr_def_17),
inference(ac_demodulation,[status(thm)],[c_64931,c_19378,c_65,c_64]) ).
tcf(c_66479,plain,
join(complement(iPr_def_18),complement(join(complement(join(complement(iPr_def_18),join(iPr_def_13,complement(iPr_def_17)))),complement(complement(iPr_def_12))))) = join(complement(iPr_def_18),join(iPr_def_13,complement(iPr_def_17))),
inference(superposition,[status(thm)],[c_20510,c_730]) ).
tcf(c_66508,plain,
join(iPr_def_13,join(complement(iPr_def_17),complement(iPr_def_18))) = join(complement(iPr_def_12),complement(iPr_def_18)),
inference(demodulation,[status(thm)],[c_66479,c_64,c_230,c_20161,c_40489]) ).
tcf(c_66509,plain,
join(iPr_def_13,complement(iPr_def_17)) = join(iPr_def_13,complement(iPr_def_18)),
inference(light_normalisation,[status(thm)],[c_66508,c_20497,c_64932]) ).
tcf(c_109889,plain,
! [X0: $i,X1: $i] : join(complement(top),complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(superposition,[status(thm)],[c_10718,c_1383]) ).
tcf(c_110005,plain,
! [X0: $i] : join(complement(top),complement(join(complement(iPr_def_17),complement(join(sk2,X0))))) = iPr_def_17,
inference(superposition,[status(thm)],[c_34181,c_1383]) ).
tcf(c_110009,plain,
! [X0: $i] : join(complement(top),complement(join(complement(iPr_def_18),complement(join(sk2,X0))))) = iPr_def_18,
inference(superposition,[status(thm)],[c_34921,c_1383]) ).
tcf(c_110780,plain,
! [X0: $i] : join(zero,complement(join(complement(iPr_def_18),complement(join(sk2,X0))))) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_110009,c_123]) ).
tcf(c_110781,plain,
! [X0: $i] : complement(join(complement(iPr_def_18),complement(join(sk2,X0)))) = iPr_def_18,
inference(ac_demodulation,[status(thm)],[c_110780,c_19378,c_65,c_64]) ).
tcf(c_110782,plain,
! [X0: $i] : join(zero,complement(join(complement(iPr_def_17),complement(join(sk2,X0))))) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_110005,c_123]) ).
tcf(c_110783,plain,
! [X0: $i] : complement(join(complement(iPr_def_17),complement(join(sk2,X0)))) = iPr_def_17,
inference(ac_demodulation,[status(thm)],[c_110782,c_19378,c_65,c_64]) ).
tcf(c_110824,plain,
! [X0: $i,X1: $i] : join(zero,complement(join(complement(X0),complement(join(X0,X1))))) = X0,
inference(light_normalisation,[status(thm)],[c_109889,c_123]) ).
tcf(c_110825,plain,
! [X0: $i,X1: $i] : complement(join(complement(X0),complement(join(X0,X1)))) = X0,
inference(ac_demodulation,[status(thm)],[c_110824,c_19378,c_65,c_64]) ).
tcf(c_143866,plain,
complement(join(complement(iPr_def_18),complement(sk2))) = iPr_def_18,
inference(superposition,[status(thm)],[c_19532,c_110781]) ).
tcf(c_143961,plain,
complement(join(complement(iPr_def_18),iPr_def_11)) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_143866,c_20459]) ).
tcf(c_143962,plain,
complement(join(iPr_def_11,complement(iPr_def_18))) = iPr_def_18,
inference(theory_normalisation,[status(thm)],[c_143961,c_65,c_64]) ).
tcf(c_144069,plain,
join(iPr_def_11,complement(iPr_def_18)) = complement(iPr_def_18),
inference(superposition,[status(thm)],[c_143962,c_20161]) ).
tcf(c_144161,plain,
join(iPr_def_10,complement(iPr_def_18)) = join(iPr_def_12,complement(iPr_def_18)),
inference(superposition,[status(thm)],[c_144069,c_237]) ).
tcf(c_144172,plain,
join(iPr_def_10,complement(iPr_def_18)) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_144161,c_41041]) ).
tcf(c_144205,plain,
join(iPr_def_10,join(complement(iPr_def_18),complement(iPr_def_12))) = top,
inference(superposition,[status(thm)],[c_144172,c_266]) ).
tcf(c_144234,plain,
join(iPr_def_10,join(complement(iPr_def_12),complement(iPr_def_18))) = top,
inference(demodulation,[status(thm)],[c_144205,c_64]) ).
tcf(c_144235,plain,
join(iPr_def_10,join(iPr_def_13,complement(iPr_def_17))) = top,
inference(light_normalisation,[status(thm)],[c_144234,c_20497,c_66509]) ).
tcf(c_144868,plain,
join(complement(top),complement(join(iPr_def_10,complement(join(iPr_def_13,complement(iPr_def_17)))))) = iPr_def_19,
inference(superposition,[status(thm)],[c_144235,c_721]) ).
tcf(c_144890,plain,
join(zero,complement(join(iPr_def_10,complement(join(iPr_def_13,complement(iPr_def_17)))))) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_144868,c_123]) ).
tcf(c_144891,plain,
complement(join(iPr_def_10,complement(join(iPr_def_13,complement(iPr_def_17))))) = iPr_def_19,
inference(ac_demodulation,[status(thm)],[c_144890,c_19378,c_65,c_64]) ).
tcf(c_145027,plain,
complement(join(complement(iPr_def_17),complement(sk2))) = iPr_def_17,
inference(superposition,[status(thm)],[c_19532,c_110783]) ).
tcf(c_145122,plain,
complement(join(complement(iPr_def_17),iPr_def_11)) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_145027,c_20459]) ).
tcf(c_145123,plain,
complement(join(iPr_def_11,complement(iPr_def_17))) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_145122,c_65,c_64]) ).
tcf(c_145432,plain,
join(iPr_def_11,complement(iPr_def_17)) = complement(iPr_def_17),
inference(superposition,[status(thm)],[c_145123,c_20161]) ).
tcf(c_145488,plain,
join(iPr_def_10,complement(iPr_def_17)) = join(iPr_def_12,complement(iPr_def_17)),
inference(superposition,[status(thm)],[c_145432,c_237]) ).
tcf(c_145760,plain,
join(iPr_def_13,complement(join(iPr_def_10,complement(iPr_def_17)))) = iPr_def_13,
inference(superposition,[status(thm)],[c_145488,c_30849]) ).
tcf(c_146656,plain,
complement(join(complement(iPr_def_17),complement(composition(iPr_def_19,sk2)))) = iPr_def_17,
inference(superposition,[status(thm)],[c_23843,c_110825]) ).
tcf(c_147048,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(X0,X1))) = complement(X0),
inference(superposition,[status(thm)],[c_110825,c_20161]) ).
tcf(c_226298,plain,
join(iPr_def_10,complement(join(iPr_def_13,complement(iPr_def_17)))) = complement(iPr_def_19),
inference(superposition,[status(thm)],[c_144891,c_20161]) ).
tcf(c_226315,plain,
join(iPr_def_10,complement(join(iPr_def_13,complement(iPr_def_17)))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_226298,c_228]) ).
tcf(c_235199,plain,
join(complement(iPr_def_17),complement(composition(iPr_def_19,sk2))) = complement(iPr_def_17),
inference(superposition,[status(thm)],[c_146656,c_20161]) ).
tcf(c_236830,plain,
! [X0: $i,X1: $i] : join(complement(complement(X0)),complement(join(X1,complement(X0)))) = complement(complement(X0)),
inference(superposition,[status(thm)],[c_1318,c_147048]) ).
tcf(c_238065,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_236830,c_20161]) ).
tcf(c_238878,plain,
join(join(iPr_def_13,complement(iPr_def_17)),complement(iPr_def_10)) = join(iPr_def_13,complement(iPr_def_17)),
inference(superposition,[status(thm)],[c_226315,c_238065]) ).
tcf(c_239492,plain,
join(iPr_def_13,join(complement(iPr_def_10),complement(iPr_def_17))) = join(iPr_def_13,complement(iPr_def_17)),
inference(demodulation,[status(thm)],[c_238878,c_64,c_65]) ).
tcf(c_239493,plain,
join(iPr_def_13,join(iPr_def_19,complement(iPr_def_17))) = join(iPr_def_13,complement(iPr_def_17)),
inference(light_normalisation,[status(thm)],[c_239492,c_20458]) ).
tcf(c_239494,plain,
join(complement(iPr_def_17),iPr_def_19) = join(iPr_def_13,complement(iPr_def_17)),
inference(ac_demodulation,[status(thm)],[c_239493,c_24092,c_65,c_64]) ).
tcf(c_243139,plain,
join(iPr_def_13,complement(iPr_def_17)) = join(iPr_def_19,complement(iPr_def_17)),
inference(theory_normalisation,[status(thm)],[c_239494,c_65,c_64]) ).
tcf(c_280086,plain,
! [X0: $i] : join(composition(iPr_def_19,sk2),join(X0,complement(iPr_def_17))) = top,
inference(superposition,[status(thm)],[c_235199,c_12613]) ).
tcf(c_280092,plain,
! [X0: $i] : join(complement(iPr_def_17),join(X0,composition(iPr_def_19,sk2))) = top,
inference(theory_normalisation,[status(thm)],[c_280086,c_65,c_64]) ).
tcf(c_305586,plain,
join(complement(iPr_def_17),iPr_def_19) = top,
inference(superposition,[status(thm)],[c_15470,c_280092]) ).
tcf(c_305672,plain,
join(iPr_def_19,complement(iPr_def_17)) = top,
inference(demodulation,[status(thm)],[c_305586,c_64]) ).
tcf(c_305718,plain,
join(iPr_def_13,complement(iPr_def_17)) = top,
inference(demodulation,[status(thm)],[c_243139,c_305672]) ).
tcf(c_305725,plain,
join(complement(iPr_def_18),complement(top)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_20510,c_305718]) ).
tcf(c_305726,plain,
join(complement(iPr_def_18),zero) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_305725,c_123]) ).
tcf(c_305727,plain,
join(zero,complement(iPr_def_18)) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_305726,c_65,c_64]) ).
tcf(c_305728,plain,
complement(iPr_def_18) = iPr_def_12,
inference(ac_demodulation,[status(thm)],[c_305727,c_19378,c_65,c_64]) ).
tcf(c_305761,plain,
join(complement(iPr_def_17),iPr_def_12) = complement(iPr_def_17),
inference(demodulation,[status(thm)],[c_64932,c_305728]) ).
tcf(c_305767,plain,
join(iPr_def_12,complement(iPr_def_17)) = complement(iPr_def_17),
inference(demodulation,[status(thm)],[c_305761,c_64]) ).
tcf(c_305768,plain,
join(iPr_def_10,complement(iPr_def_17)) = complement(iPr_def_17),
inference(demodulation,[status(thm)],[c_145488,c_305767]) ).
tcf(c_305769,plain,
join(iPr_def_13,complement(complement(iPr_def_17))) = iPr_def_13,
inference(demodulation,[status(thm)],[c_145760,c_305768]) ).
tcf(c_305770,plain,
join(iPr_def_13,iPr_def_17) = iPr_def_13,
inference(demodulation,[status(thm)],[c_305769,c_20161]) ).
tcf(c_305772,plain,
iPr_def_13 = iPr_def_18,
inference(demodulation,[status(thm)],[c_138,c_305770]) ).
tcf(c_305883,plain,
iPr_def_13 != iPr_def_13,
inference(demodulation,[status(thm)],[c_140,c_305772]) ).
tcf(c_305884,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_305883]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL021-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.08/0.36 % Computer : n009.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 07:16:58 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 Running UEQ theorem proving
% 0.14/0.40 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.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 185.94/24.96 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 185.94/24.96 % SZS status Started for theBenchmark.p
% 185.94/24.96 % SZS status Unsatisfiable for theBenchmark.p
% 185.94/24.96
% 185.94/24.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 185.94/24.96
% 185.94/24.96 % ------ iProver source info
% 185.94/24.96
% 185.94/24.96 % git: date: 2026-07-19 20:42:38 +0200
% 185.94/24.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 185.94/24.96 % git: non_committed_changes: false
% 185.94/24.96
% 185.94/24.96 % ------ Parsing...% successful
% 185.94/24.96
% 185.94/24.96
% 185.94/24.96 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 185.94/24.96
% 185.94/24.96 % ------ Preprocessing... sup_sim: 1 sf_s rm: 0 0s sf_e pe_s pe_e %
% 185.94/24.96
% 185.94/24.96 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 185.94/24.96
% 185.94/24.96 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 185.94/24.96 % ------ Proving...
% 185.94/24.96 % ------ Problem Properties
% 185.94/24.96
% 185.94/24.96 %
% 185.94/24.96 % clauses 24
% 185.94/24.96 % conjectures 2
% 185.94/24.96 % EPR 2
% 185.94/24.96 % Horn 24
% 185.94/24.96 % unary 24
% 185.94/24.96 % binary 0
% 185.94/24.96 % lits 24
% 185.94/24.96 % lits eq 24
% 185.94/24.96 % fd_pure 0
% 185.94/24.96 % fd_pseudo 0
% 185.94/24.96 % fd_cond 0
% 185.94/24.96 % fd_pseudo_cond 0
% 185.94/24.96 % AC symbols 1
% 185.94/24.96
% 185.94/24.96 % ------ Input Options Time Limit: Unbounded
% 185.94/24.96
% 185.94/24.96
% 185.94/24.96 % ------
% 185.94/24.96 % Current options:
% 185.94/24.96 % ------
% 185.94/24.96
% 185.94/24.96
% 185.94/24.96 %
% 185.94/24.96
% 185.94/24.96 % ------ Proving...
% 185.94/24.96 %
% 185.94/24.96
% 185.94/24.96 % SZS status Unsatisfiable for theBenchmark.p
% 185.94/24.96
% 185.94/24.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 185.94/24.97
% 185.94/24.97
%------------------------------------------------------------------------------