%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL005-2 : 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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:36:31 PM UTC 2026
% Result : Unsatisfiable 67.58s 22.40s
% Output : CNFRefutation 67.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 25
% Syntax : Number of formulae : 371 ( 364 unt; 12 def)
% Number of atoms : 963 ( 377 equ)
% Maximal formula atoms : 2 ( 2 avg)
% Number of connectives : 22 ( 15 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 185 ( 0 sgn 185 !; 0 ?; 156 :)
% 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(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,
( join(meet(converse(sk1),converse(sk2)),converse(meet(sk1,sk2))) != converse(meet(sk1,sk2))
| join(converse(meet(sk1,sk2)),meet(converse(sk1),converse(sk2))) != meet(converse(sk1),converse(sk2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
( converse(meet(sk1,sk2)) != join(meet(converse(sk1),converse(sk2)),converse(meet(sk1,sk2)))
| meet(converse(sk1),converse(sk2)) != join(converse(meet(sk1,sk2)),meet(converse(sk1),converse(sk2))) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f20,plain,
( converse(complement(join(complement(sk1),complement(sk2)))) != join(complement(join(complement(converse(sk1)),complement(converse(sk2)))),converse(complement(join(complement(sk1),complement(sk2)))))
| complement(join(complement(converse(sk1)),complement(converse(sk2)))) != join(converse(complement(join(complement(sk1),complement(sk2)))),complement(join(complement(converse(sk1)),complement(converse(sk2))))) ),
inference(definition_unfolding,[],[f18,f6,f6,f6,f6,f6,f6]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_67,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f8]) ).
tcf(c_69,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f10]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(cnf_transformation,[],[f11]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[],[f14]) ).
tcf(c_73,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(cnf_transformation,[],[f15]) ).
tcf(c_74,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(cnf_transformation,[],[f19]) ).
tcf(c_75,negated_conjecture,
( ( join(converse(complement(join(complement(sk1),complement(sk2)))),complement(join(complement(converse(sk1)),complement(converse(sk2))))) != complement(join(complement(converse(sk1)),complement(converse(sk2)))) )
| ( join(complement(join(complement(converse(sk1)),complement(converse(sk2)))),converse(complement(join(complement(sk1),complement(sk2))))) != converse(complement(join(complement(sk1),complement(sk2)))) ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(theory_normalisation,[status(thm)],[c_65,c_64,c_63]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(theory_normalisation,[status(thm)],[c_72,c_64,c_63]) ).
tcf(c_90,negated_conjecture,
( ( join(converse(complement(join(complement(sk1),complement(sk2)))),complement(join(complement(converse(sk1)),complement(converse(sk2))))) != converse(complement(join(complement(sk1),complement(sk2)))) )
| ( join(converse(complement(join(complement(sk1),complement(sk2)))),complement(join(complement(converse(sk1)),complement(converse(sk2))))) != complement(join(complement(converse(sk1)),complement(converse(sk2)))) ) ),
inference(theory_normalisation,[status(thm)],[c_75,c_64,c_63]) ).
tcf(c_121,plain,
complement(top) = zero,
inference(ac_demodulation,[status(thm)],[c_74,c_73,c_64,c_63]) ).
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 = converse(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_135,definition,
iPr_def_15 = converse(sk1),
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 = converse(sk2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_138,definition,
iPr_def_18 = complement(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_139,definition,
iPr_def_19 = join(iPr_def_16,iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_140,definition,
iPr_def_20 = complement(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_141,definition,
iPr_def_21 = join(iPr_def_14,iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_142,negated_conjecture,
( ( iPr_def_21 != iPr_def_20 )
| ( iPr_def_21 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_90,c_137,c_138,c_135,c_136,c_139,c_140,c_131,c_130,c_132,c_133,c_134,c_141]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_245,plain,
! [X0: $i] : join(complement(join(iPr_def_10,X0)),complement(join(iPr_def_10,complement(X0)))) = sk1,
inference(superposition,[status(thm)],[c_130,c_88]) ).
tcf(c_247,plain,
! [X0: $i] : join(complement(join(zero,X0)),complement(join(zero,complement(X0)))) = top,
inference(superposition,[status(thm)],[c_121,c_88]) ).
tcf(c_249,plain,
! [X0: $i] : join(complement(join(iPr_def_16,X0)),complement(join(iPr_def_16,complement(X0)))) = iPr_def_15,
inference(superposition,[status(thm)],[c_136,c_88]) ).
tcf(c_252,plain,
! [X0: $i] : join(complement(join(complement(X0),top)),complement(join(complement(X0),zero))) = X0,
inference(superposition,[status(thm)],[c_121,c_88]) ).
tcf(c_259,plain,
! [X0: $i] : join(complement(join(top,complement(X0))),complement(join(zero,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_252,c_64,c_63]) ).
tcf(c_276,plain,
! [X0: $i] : join(complement(join(iPr_def_18,X0)),complement(join(iPr_def_18,complement(X0)))) = iPr_def_17,
inference(superposition,[status(thm)],[c_138,c_88]) ).
tcf(c_286,plain,
converse(iPr_def_15) = sk1,
inference(superposition,[status(thm)],[c_135,c_69]) ).
tcf(c_295,plain,
join(sk1,iPr_def_10) = top,
inference(superposition,[status(thm)],[c_130,c_73]) ).
tcf(c_297,plain,
join(top,zero) = top,
inference(superposition,[status(thm)],[c_121,c_73]) ).
tcf(c_299,plain,
join(iPr_def_15,iPr_def_16) = top,
inference(superposition,[status(thm)],[c_136,c_73]) ).
tcf(c_300,plain,
join(iPr_def_17,iPr_def_18) = top,
inference(superposition,[status(thm)],[c_138,c_73]) ).
tcf(c_302,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_73,c_88]) ).
tcf(c_305,plain,
join(iPr_def_10,sk1) = top,
inference(theory_normalisation,[status(thm)],[c_295,c_64,c_63]) ).
tcf(c_306,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_302,c_64,c_63]) ).
tcf(c_307,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_306,c_121]) ).
tcf(c_327,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(X1,complement(composition(converse(X1),X0)))) = complement(X0),
inference(superposition,[status(thm)],[c_69,c_89]) ).
tcf(c_388,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_69,c_70]) ).
tcf(c_391,plain,
! [X0: $i] : converse(join(iPr_def_15,X0)) = join(sk1,converse(X0)),
inference(superposition,[status(thm)],[c_286,c_70]) ).
tcf(c_398,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(superposition,[status(thm)],[c_69,c_70]) ).
tcf(c_455,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_69,c_71]) ).
tcf(c_501,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_18,X0)) = join(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_139,c_64]) ).
tcf(c_503,plain,
! [X0: $i] : join(top,join(zero,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_297,c_64]) ).
tcf(c_504,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(join(X0,X1)))) = top,
inference(superposition,[status(thm)],[c_64,c_73]) ).
tcf(c_565,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_16,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_299,c_64]) ).
tcf(c_573,plain,
! [X0: $i] : join(iPr_def_10,join(sk1,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_305,c_64]) ).
tcf(c_704,plain,
! [X0: $i] : join(iPr_def_15,join(X0,iPr_def_16)) = join(X0,top),
inference(superposition,[status(thm)],[c_299,c_233]) ).
tcf(c_705,plain,
! [X0: $i] : join(iPr_def_17,join(X0,iPr_def_18)) = join(X0,top),
inference(superposition,[status(thm)],[c_300,c_233]) ).
tcf(c_779,plain,
! [X0: $i,X1: $i] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(superposition,[status(thm)],[c_67,c_66]) ).
tcf(c_1258,plain,
join(complement(join(iPr_def_10,iPr_def_10)),complement(top)) = sk1,
inference(superposition,[status(thm)],[c_73,c_245]) ).
tcf(c_1271,plain,
join(complement(top),complement(join(iPr_def_10,iPr_def_10))) = sk1,
inference(theory_normalisation,[status(thm)],[c_1258,c_64,c_63]) ).
tcf(c_1272,plain,
join(zero,complement(join(iPr_def_10,iPr_def_10))) = sk1,
inference(light_normalisation,[status(thm)],[c_1271,c_121]) ).
tcf(c_2484,plain,
join(complement(join(zero,zero)),complement(top)) = top,
inference(superposition,[status(thm)],[c_73,c_247]) ).
tcf(c_2499,plain,
join(complement(top),complement(join(zero,zero))) = top,
inference(theory_normalisation,[status(thm)],[c_2484,c_64,c_63]) ).
tcf(c_2500,plain,
join(zero,complement(join(zero,zero))) = top,
inference(light_normalisation,[status(thm)],[c_2499,c_121]) ).
tcf(c_4902,plain,
join(top,complement(zero)) = join(top,top),
inference(superposition,[status(thm)],[c_73,c_503]) ).
tcf(c_4906,plain,
join(top,complement(join(zero,zero))) = join(top,top),
inference(superposition,[status(thm)],[c_2500,c_503]) ).
tcf(c_4959,plain,
join(complement(join(iPr_def_16,iPr_def_16)),complement(top)) = iPr_def_15,
inference(superposition,[status(thm)],[c_73,c_249]) ).
tcf(c_4972,plain,
join(complement(top),complement(join(iPr_def_16,iPr_def_16))) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_4959,c_64,c_63]) ).
tcf(c_4973,plain,
join(zero,complement(join(iPr_def_16,iPr_def_16))) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_4972,c_121]) ).
tcf(c_5069,plain,
join(top,iPr_def_18) = join(iPr_def_15,iPr_def_19),
inference(superposition,[status(thm)],[c_139,c_565]) ).
tcf(c_5076,plain,
join(iPr_def_15,iPr_def_19) = join(iPr_def_18,top),
inference(theory_normalisation,[status(thm)],[c_5069,c_64,c_63]) ).
tcf(c_5265,plain,
join(iPr_def_15,iPr_def_16) = top,
inference(superposition,[status(thm)],[c_136,c_73]) ).
tcf(c_5267,plain,
join(iPr_def_19,iPr_def_20) = top,
inference(superposition,[status(thm)],[c_140,c_73]) ).
tcf(c_5268,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[status(thm)],[c_73,c_64]) ).
tcf(c_5319,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_69,c_71]) ).
tcf(c_5365,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_16,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_5265,c_64]) ).
tcf(c_5367,plain,
! [X0: $i] : join(iPr_def_19,join(iPr_def_20,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_5267,c_64]) ).
tcf(c_5430,plain,
! [X0: $i] : join(iPr_def_16,composition(converse(X0),complement(composition(X0,iPr_def_15)))) = iPr_def_16,
inference(superposition,[status(thm)],[c_136,c_89]) ).
tcf(c_5478,plain,
! [X0: $i] : join(complement(join(iPr_def_20,X0)),complement(join(iPr_def_20,complement(X0)))) = iPr_def_19,
inference(superposition,[status(thm)],[c_140,c_88]) ).
tcf(c_5485,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_19)),complement(join(complement(X0),iPr_def_20))) = X0,
inference(superposition,[status(thm)],[c_140,c_88]) ).
tcf(c_5492,plain,
! [X0: $i] : join(complement(join(iPr_def_19,complement(X0))),complement(join(iPr_def_20,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_5485,c_64,c_63]) ).
tcf(c_6211,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_16,X0)) = join(X0,top),
inference(superposition,[status(thm)],[c_63,c_704]) ).
tcf(c_6230,plain,
! [X0: $i] : join(iPr_def_17,join(iPr_def_18,X0)) = join(X0,top),
inference(superposition,[status(thm)],[c_63,c_705]) ).
tcf(c_6792,plain,
join(complement(join(top,complement(zero))),complement(top)) = zero,
inference(superposition,[status(thm)],[c_73,c_259]) ).
tcf(c_6795,plain,
join(complement(join(top,complement(join(zero,zero)))),complement(top)) = join(zero,zero),
inference(superposition,[status(thm)],[c_2500,c_259]) ).
tcf(c_6812,plain,
join(complement(top),complement(join(top,complement(zero)))) = zero,
inference(theory_normalisation,[status(thm)],[c_6792,c_64,c_63]) ).
tcf(c_6813,plain,
join(zero,complement(join(top,top))) = zero,
inference(light_normalisation,[status(thm)],[c_6812,c_121,c_4902]) ).
tcf(c_6833,plain,
join(complement(top),complement(join(top,complement(join(zero,zero))))) = join(zero,zero),
inference(theory_normalisation,[status(thm)],[c_6795,c_64,c_63]) ).
tcf(c_6834,plain,
join(zero,complement(join(top,top))) = join(zero,zero),
inference(light_normalisation,[status(thm)],[c_6833,c_121,c_4906]) ).
tcf(c_6864,plain,
join(top,complement(join(top,top))) = join(top,zero),
inference(superposition,[status(thm)],[c_6813,c_503]) ).
tcf(c_6868,plain,
join(top,complement(join(top,top))) = top,
inference(light_normalisation,[status(thm)],[c_6864,c_297]) ).
tcf(c_6989,plain,
join(complement(top),complement(join(zero,complement(join(top,top))))) = join(top,top),
inference(superposition,[status(thm)],[c_6868,c_259]) ).
tcf(c_6990,plain,
join(top,top) = top,
inference(light_normalisation,[status(thm)],[c_6989,c_121,c_2500,c_6834]) ).
tcf(c_6992,plain,
join(zero,complement(top)) = zero,
inference(demodulation,[status(thm)],[c_6813,c_6990]) ).
tcf(c_6994,plain,
join(zero,zero) = zero,
inference(light_normalisation,[status(thm)],[c_6992,c_121]) ).
tcf(c_7004,plain,
! [X0: $i] : join(zero,join(zero,X0)) = join(zero,X0),
inference(superposition,[status(thm)],[c_6994,c_64]) ).
tcf(c_8880,plain,
join(complement(join(iPr_def_18,iPr_def_18)),complement(top)) = iPr_def_17,
inference(superposition,[status(thm)],[c_73,c_276]) ).
tcf(c_8896,plain,
join(complement(top),complement(join(iPr_def_18,iPr_def_18))) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_8880,c_64,c_63]) ).
tcf(c_8897,plain,
join(zero,complement(join(iPr_def_18,iPr_def_18))) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_8896,c_121]) ).
tcf(c_11331,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(superposition,[status(thm)],[c_307,c_7004]) ).
tcf(c_11366,plain,
! [X0: $i] : complement(join(complement(X0),complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_307,c_11331]) ).
tcf(c_11367,plain,
complement(join(iPr_def_10,iPr_def_10)) = sk1,
inference(demodulation,[status(thm)],[c_1272,c_11331]) ).
tcf(c_11370,plain,
complement(join(iPr_def_16,iPr_def_16)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4973,c_11331]) ).
tcf(c_11371,plain,
complement(join(iPr_def_18,iPr_def_18)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_8897,c_11331]) ).
tcf(c_11689,plain,
join(join(iPr_def_10,iPr_def_10),sk1) = top,
inference(superposition,[status(thm)],[c_11367,c_73]) ).
tcf(c_11695,plain,
join(iPr_def_10,join(iPr_def_10,sk1)) = top,
inference(theory_normalisation,[status(thm)],[c_11689,c_64,c_63]) ).
tcf(c_11696,plain,
join(iPr_def_10,top) = top,
inference(light_normalisation,[status(thm)],[c_11695,c_305]) ).
tcf(c_11722,plain,
! [X0: $i] : join(iPr_def_10,join(top,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_11696,c_64]) ).
tcf(c_12770,plain,
join(join(iPr_def_16,iPr_def_16),iPr_def_15) = top,
inference(superposition,[status(thm)],[c_11370,c_73]) ).
tcf(c_12771,plain,
join(iPr_def_15,join(iPr_def_16,iPr_def_16)) = top,
inference(theory_normalisation,[status(thm)],[c_12770,c_64,c_63]) ).
tcf(c_12774,plain,
join(join(iPr_def_18,iPr_def_18),iPr_def_17) = top,
inference(superposition,[status(thm)],[c_11371,c_73]) ).
tcf(c_12775,plain,
join(iPr_def_17,join(iPr_def_18,iPr_def_18)) = top,
inference(theory_normalisation,[status(thm)],[c_12774,c_64,c_63]) ).
tcf(c_13099,plain,
join(iPr_def_16,top) = top,
inference(demodulation,[status(thm)],[c_12771,c_6211]) ).
tcf(c_13121,plain,
join(iPr_def_15,iPr_def_19) = top,
inference(demodulation,[status(thm)],[c_12775,c_5076,c_6230]) ).
tcf(c_13123,plain,
join(iPr_def_18,top) = top,
inference(demodulation,[status(thm)],[c_5076,c_13121]) ).
tcf(c_13127,plain,
join(sk1,converse(iPr_def_19)) = converse(top),
inference(superposition,[status(thm)],[c_13121,c_391]) ).
tcf(c_13145,plain,
join(iPr_def_16,top) = join(iPr_def_19,top),
inference(superposition,[status(thm)],[c_13123,c_501]) ).
tcf(c_13147,plain,
join(iPr_def_19,top) = top,
inference(light_normalisation,[status(thm)],[c_13145,c_13099]) ).
tcf(c_13177,plain,
! [X0: $i] : join(iPr_def_19,join(top,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_13147,c_64]) ).
tcf(c_13484,plain,
join(top,converse(iPr_def_19)) = join(iPr_def_10,converse(top)),
inference(superposition,[status(thm)],[c_13127,c_573]) ).
tcf(c_13568,plain,
! [X0: $i] : join(complement(X0),complement(X0)) = complement(join(X0,X0)),
inference(superposition,[status(thm)],[c_11366,c_11366]) ).
tcf(c_23374,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[status(thm)],[c_73,c_388]) ).
tcf(c_25588,plain,
join(iPr_def_19,converse(top)) = converse(top),
inference(superposition,[status(thm)],[c_23374,c_13177]) ).
tcf(c_25597,plain,
join(iPr_def_10,converse(top)) = converse(top),
inference(superposition,[status(thm)],[c_23374,c_11722]) ).
tcf(c_25673,plain,
join(top,converse(iPr_def_19)) = converse(top),
inference(demodulation,[status(thm)],[c_13484,c_25597]) ).
tcf(c_25951,plain,
join(converse(iPr_def_19),top) = converse(converse(top)),
inference(superposition,[status(thm)],[c_25588,c_398]) ).
tcf(c_25958,plain,
join(top,converse(iPr_def_19)) = converse(converse(top)),
inference(theory_normalisation,[status(thm)],[c_25951,c_64,c_63]) ).
tcf(c_25959,plain,
converse(converse(top)) = converse(top),
inference(light_normalisation,[status(thm)],[c_25958,c_25673]) ).
tcf(c_25968,plain,
converse(top) = top,
inference(demodulation,[status(thm)],[c_25959,c_69]) ).
tcf(c_27796,plain,
! [X0: $i] : join(iPr_def_19,join(X0,iPr_def_20)) = join(top,X0),
inference(superposition,[status(thm)],[c_63,c_5367]) ).
tcf(c_28142,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_67,c_455]) ).
tcf(c_28265,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(light_normalisation,[status(thm)],[c_28142,c_69]) ).
tcf(c_28488,plain,
converse(one) = one,
inference(superposition,[status(thm)],[c_28265,c_67]) ).
tcf(c_28520,plain,
! [X0: $i] : composition(converse(one),X0) = composition(one,X0),
inference(superposition,[status(thm)],[c_28265,c_779]) ).
tcf(c_28525,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(light_normalisation,[status(thm)],[c_28520,c_28265]) ).
tcf(c_28728,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_67,c_5319]) ).
tcf(c_28816,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(light_normalisation,[status(thm)],[c_28728,c_69]) ).
tcf(c_28841,plain,
! [X0: $i] : join(complement(X0),complement(composition(converse(one),X0))) = complement(X0),
inference(superposition,[status(thm)],[c_28525,c_327]) ).
tcf(c_28853,plain,
! [X0: $i] : complement(join(X0,X0)) = complement(X0),
inference(light_normalisation,[status(thm)],[c_28841,c_13568,c_28488,c_28525]) ).
tcf(c_29687,plain,
converse(one) = one,
inference(superposition,[status(thm)],[c_28816,c_67]) ).
tcf(c_29703,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(demodulation,[status(thm)],[c_28816,c_29687]) ).
tcf(c_34130,plain,
! [X0: $i] : join(X0,join(X0,complement(X0))) = top,
inference(superposition,[status(thm)],[c_28853,c_504]) ).
tcf(c_34132,plain,
! [X0: $i] : join(X0,top) = top,
inference(light_normalisation,[status(thm)],[c_34130,c_73]) ).
tcf(c_86556,plain,
join(iPr_def_16,composition(converse(one),complement(iPr_def_15))) = iPr_def_16,
inference(superposition,[status(thm)],[c_29703,c_5430]) ).
tcf(c_86560,plain,
join(iPr_def_16,composition(one,iPr_def_16)) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_86556,c_136,c_29687]) ).
tcf(c_108486,plain,
join(iPr_def_16,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_86560,c_29703]) ).
tcf(c_108489,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_16,X0)) = join(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_108486,c_64]) ).
tcf(c_128862,plain,
join(iPr_def_16,iPr_def_19) = iPr_def_19,
inference(superposition,[status(thm)],[c_139,c_108489]) ).
tcf(c_134613,plain,
! [X0: $i] : join(top,complement(join(iPr_def_20,complement(X0)))) = join(join(iPr_def_20,X0),iPr_def_19),
inference(superposition,[status(thm)],[c_5478,c_5268]) ).
tcf(c_134624,plain,
! [X0: $i] : join(top,complement(join(iPr_def_20,complement(X0)))) = join(iPr_def_19,join(X0,iPr_def_20)),
inference(theory_normalisation,[status(thm)],[c_134613,c_64,c_63]) ).
tcf(c_134625,plain,
! [X0: $i] : join(top,complement(join(iPr_def_20,complement(X0)))) = join(top,X0),
inference(light_normalisation,[status(thm)],[c_134624,c_27796]) ).
tcf(c_137740,plain,
join(top,iPr_def_19) = join(iPr_def_15,iPr_def_19),
inference(superposition,[status(thm)],[c_128862,c_5365]) ).
tcf(c_137741,plain,
join(iPr_def_15,iPr_def_19) = join(iPr_def_19,top),
inference(theory_normalisation,[status(thm)],[c_137740,c_64,c_63]) ).
tcf(c_155410,plain,
! [X0: $i] : join(top,complement(join(iPr_def_20,complement(X0)))) = join(join(iPr_def_19,complement(X0)),X0),
inference(superposition,[status(thm)],[c_5492,c_5268]) ).
tcf(c_155432,plain,
! [X0: $i] : join(top,complement(join(iPr_def_20,complement(X0)))) = join(iPr_def_19,join(X0,complement(X0))),
inference(theory_normalisation,[status(thm)],[c_155410,c_64,c_63]) ).
tcf(c_155433,plain,
! [X0: $i] : join(top,X0) = join(iPr_def_15,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_155432,c_73,c_137741,c_134625]) ).
tcf(c_208019,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_208030,plain,
! [X0: $i] : join(complement(join(iPr_def_10,X0)),complement(join(iPr_def_10,complement(X0)))) = sk1,
inference(superposition,[status(thm)],[c_130,c_88]) ).
tcf(c_208031,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_88]) ).
tcf(c_208033,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_88]) ).
tcf(c_208034,plain,
! [X0: $i] : join(complement(join(iPr_def_16,X0)),complement(join(iPr_def_16,complement(X0)))) = iPr_def_15,
inference(superposition,[status(thm)],[c_136,c_88]) ).
tcf(c_208038,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_88]) ).
tcf(c_208043,plain,
! [X0: $i] : join(complement(join(iPr_def_12,complement(X0))),complement(join(iPr_def_13,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_208038,c_64,c_63]) ).
tcf(c_208049,plain,
! [X0: $i] : join(complement(join(iPr_def_18,X0)),complement(join(iPr_def_18,complement(X0)))) = iPr_def_17,
inference(superposition,[status(thm)],[c_138,c_88]) ).
tcf(c_208053,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_19)),complement(join(complement(X0),iPr_def_20))) = X0,
inference(superposition,[status(thm)],[c_140,c_88]) ).
tcf(c_208054,plain,
! [X0: $i] : join(complement(join(iPr_def_19,complement(X0))),complement(join(iPr_def_20,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_208053,c_64,c_63]) ).
tcf(c_208055,plain,
converse(iPr_def_15) = sk1,
inference(superposition,[status(thm)],[c_135,c_69]) ).
tcf(c_208056,plain,
converse(iPr_def_17) = sk2,
inference(superposition,[status(thm)],[c_137,c_69]) ).
tcf(c_208057,plain,
converse(iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_134,c_69]) ).
tcf(c_208058,plain,
converse(sk1) = iPr_def_15,
inference(superposition,[status(thm)],[c_208055,c_69]) ).
tcf(c_208059,plain,
converse(sk2) = iPr_def_17,
inference(superposition,[status(thm)],[c_208056,c_69]) ).
tcf(c_208060,plain,
converse(iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_208057,c_69]) ).
tcf(c_208064,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[status(thm)],[c_34132,c_88]) ).
tcf(c_208065,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(light_normalisation,[status(thm)],[c_208064,c_121]) ).
tcf(c_208066,plain,
! [X0: $i] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_208065,c_64,c_63]) ).
tcf(c_208092,plain,
join(iPr_def_12,iPr_def_13) = top,
inference(superposition,[status(thm)],[c_133,c_73]) ).
tcf(c_208094,plain,
join(iPr_def_17,iPr_def_18) = top,
inference(superposition,[status(thm)],[c_138,c_73]) ).
tcf(c_208096,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_73,c_88]) ).
tcf(c_208100,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_208096,c_64,c_63]) ).
tcf(c_208101,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(light_normalisation,[status(thm)],[c_208100,c_121]) ).
tcf(c_208119,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X1),complement(X0)))) = X0,
inference(superposition,[status(thm)],[c_63,c_88]) ).
tcf(c_208120,plain,
! [X0: $i,X1: $i] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[status(thm)],[c_63,c_88]) ).
tcf(c_208121,plain,
! [X0: $i] : join(top,X0) = top,
inference(superposition,[status(thm)],[c_63,c_34132]) ).
tcf(c_208130,plain,
! [X0: $i] : converse(join(sk1,X0)) = join(iPr_def_15,converse(X0)),
inference(superposition,[status(thm)],[c_208058,c_70]) ).
tcf(c_208132,plain,
! [X0: $i] : converse(join(sk2,X0)) = join(iPr_def_17,converse(X0)),
inference(superposition,[status(thm)],[c_208059,c_70]) ).
tcf(c_208137,plain,
! [X0: $i] : converse(join(iPr_def_15,X0)) = join(sk1,converse(X0)),
inference(superposition,[status(thm)],[c_208055,c_70]) ).
tcf(c_208138,plain,
! [X0: $i] : converse(join(iPr_def_17,X0)) = join(sk2,converse(X0)),
inference(superposition,[status(thm)],[c_208056,c_70]) ).
tcf(c_208139,plain,
! [X0: $i] : converse(join(iPr_def_14,X0)) = join(iPr_def_13,converse(X0)),
inference(superposition,[status(thm)],[c_208057,c_70]) ).
tcf(c_208228,plain,
join(iPr_def_15,iPr_def_19) = top,
inference(light_normalisation,[status(thm)],[c_155433,c_208121]) ).
tcf(c_208242,plain,
! [X0: $i] : join(iPr_def_10,join(iPr_def_11,X0)) = join(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_132,c_64]) ).
tcf(c_208243,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_18,X0)) = join(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_139,c_64]) ).
tcf(c_208246,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_13,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_208092,c_64]) ).
tcf(c_208248,plain,
! [X0: $i] : join(iPr_def_17,join(iPr_def_18,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_208094,c_64]) ).
tcf(c_208259,plain,
! [X0: $i] : join(iPr_def_17,join(iPr_def_18,X0)) = top,
inference(light_normalisation,[status(thm)],[c_208248,c_208121]) ).
tcf(c_208261,plain,
! [X0: $i] : join(iPr_def_12,join(iPr_def_13,X0)) = top,
inference(light_normalisation,[status(thm)],[c_208246,c_208121]) ).
tcf(c_208383,plain,
! [X0: $i] : join(iPr_def_17,join(X0,iPr_def_18)) = top,
inference(superposition,[status(thm)],[c_63,c_208259]) ).
tcf(c_208455,plain,
join(iPr_def_17,iPr_def_19) = top,
inference(superposition,[status(thm)],[c_139,c_208383]) ).
tcf(c_208761,plain,
join(zero,complement(top)) = zero,
inference(superposition,[status(thm)],[c_73,c_208066]) ).
tcf(c_208768,plain,
join(zero,complement(join(zero,iPr_def_20))) = iPr_def_19,
inference(superposition,[status(thm)],[c_140,c_208066]) ).
tcf(c_208772,plain,
join(zero,zero) = zero,
inference(light_normalisation,[status(thm)],[c_208761,c_121]) ).
tcf(c_208773,plain,
join(zero,complement(join(iPr_def_20,zero))) = iPr_def_19,
inference(theory_normalisation,[status(thm)],[c_208768,c_64,c_63]) ).
tcf(c_208798,plain,
! [X0: $i] : join(zero,join(zero,X0)) = join(zero,X0),
inference(superposition,[status(thm)],[c_208772,c_64]) ).
tcf(c_208833,plain,
join(complement(join(iPr_def_10,iPr_def_10)),complement(top)) = sk1,
inference(superposition,[status(thm)],[c_73,c_208030]) ).
tcf(c_208835,plain,
join(complement(join(iPr_def_10,sk2)),complement(join(iPr_def_10,iPr_def_11))) = sk1,
inference(superposition,[status(thm)],[c_131,c_208030]) ).
tcf(c_208846,plain,
join(complement(top),complement(join(iPr_def_10,iPr_def_10))) = sk1,
inference(theory_normalisation,[status(thm)],[c_208833,c_64,c_63]) ).
tcf(c_208847,plain,
join(zero,complement(join(iPr_def_10,iPr_def_10))) = sk1,
inference(light_normalisation,[status(thm)],[c_208846,c_121]) ).
tcf(c_208851,plain,
join(complement(join(iPr_def_10,iPr_def_11)),complement(join(iPr_def_10,sk2))) = sk1,
inference(theory_normalisation,[status(thm)],[c_208835,c_64,c_63]) ).
tcf(c_208852,plain,
join(iPr_def_13,complement(join(iPr_def_10,sk2))) = sk1,
inference(light_normalisation,[status(thm)],[c_208851,c_132,c_133]) ).
tcf(c_208934,plain,
join(zero,complement(sk1)) = join(iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_208847,c_208066]) ).
tcf(c_208935,plain,
join(zero,iPr_def_10) = join(iPr_def_10,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_208934,c_130]) ).
tcf(c_208936,plain,
join(iPr_def_10,zero) = join(iPr_def_10,iPr_def_10),
inference(theory_normalisation,[status(thm)],[c_208935,c_64,c_63]) ).
tcf(c_208972,plain,
join(iPr_def_12,sk1) = top,
inference(superposition,[status(thm)],[c_208852,c_208261]) ).
tcf(c_209138,plain,
join(complement(join(iPr_def_11,iPr_def_11)),complement(top)) = sk2,
inference(superposition,[status(thm)],[c_73,c_208031]) ).
tcf(c_209139,plain,
join(complement(join(iPr_def_11,sk1)),complement(join(iPr_def_11,iPr_def_10))) = sk2,
inference(superposition,[status(thm)],[c_130,c_208031]) ).
tcf(c_209151,plain,
join(complement(top),complement(join(iPr_def_11,iPr_def_11))) = sk2,
inference(theory_normalisation,[status(thm)],[c_209138,c_64,c_63]) ).
tcf(c_209152,plain,
join(zero,complement(join(iPr_def_11,iPr_def_11))) = sk2,
inference(light_normalisation,[status(thm)],[c_209151,c_121]) ).
tcf(c_209158,plain,
join(complement(join(iPr_def_10,iPr_def_11)),complement(join(iPr_def_11,sk1))) = sk2,
inference(theory_normalisation,[status(thm)],[c_209139,c_64,c_63]) ).
tcf(c_209159,plain,
join(iPr_def_13,complement(join(iPr_def_11,sk1))) = sk2,
inference(light_normalisation,[status(thm)],[c_209158,c_132,c_133]) ).
tcf(c_209218,plain,
join(zero,complement(sk2)) = join(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_209152,c_208066]) ).
tcf(c_209219,plain,
join(zero,iPr_def_11) = join(iPr_def_11,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_209218,c_131]) ).
tcf(c_209220,plain,
join(iPr_def_11,zero) = join(iPr_def_11,iPr_def_11),
inference(theory_normalisation,[status(thm)],[c_209219,c_64,c_63]) ).
tcf(c_209225,plain,
join(iPr_def_12,sk2) = top,
inference(superposition,[status(thm)],[c_209159,c_208261]) ).
tcf(c_210152,plain,
join(complement(join(iPr_def_13,iPr_def_13)),complement(top)) = iPr_def_12,
inference(superposition,[status(thm)],[c_73,c_208033]) ).
tcf(c_210168,plain,
join(complement(top),complement(join(iPr_def_13,iPr_def_13))) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_210152,c_64,c_63]) ).
tcf(c_210169,plain,
join(zero,complement(join(iPr_def_13,iPr_def_13))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_210168,c_121]) ).
tcf(c_210283,plain,
join(zero,complement(iPr_def_12)) = join(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_210169,c_208066]) ).
tcf(c_210284,plain,
join(zero,iPr_def_13) = join(iPr_def_13,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_210283,c_133]) ).
tcf(c_210285,plain,
join(iPr_def_13,zero) = join(iPr_def_13,iPr_def_13),
inference(theory_normalisation,[status(thm)],[c_210284,c_64,c_63]) ).
tcf(c_210554,plain,
join(complement(join(iPr_def_16,iPr_def_16)),complement(top)) = iPr_def_15,
inference(superposition,[status(thm)],[c_73,c_208034]) ).
tcf(c_210568,plain,
join(complement(top),complement(join(iPr_def_16,iPr_def_16))) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_210554,c_64,c_63]) ).
tcf(c_210569,plain,
join(zero,complement(join(iPr_def_16,iPr_def_16))) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_210568,c_121]) ).
tcf(c_210662,plain,
join(zero,complement(iPr_def_15)) = join(iPr_def_16,iPr_def_16),
inference(superposition,[status(thm)],[c_210569,c_208066]) ).
tcf(c_210663,plain,
join(zero,iPr_def_16) = join(iPr_def_16,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_210662,c_136]) ).
tcf(c_210664,plain,
join(iPr_def_16,zero) = join(iPr_def_16,iPr_def_16),
inference(theory_normalisation,[status(thm)],[c_210663,c_64,c_63]) ).
tcf(c_211176,plain,
join(iPr_def_13,converse(complement(iPr_def_14))) = converse(top),
inference(superposition,[status(thm)],[c_73,c_208139]) ).
tcf(c_211177,plain,
join(iPr_def_13,converse(iPr_def_20)) = converse(iPr_def_21),
inference(superposition,[status(thm)],[c_141,c_208139]) ).
tcf(c_211212,plain,
join(iPr_def_13,converse(complement(iPr_def_14))) = top,
inference(light_normalisation,[status(thm)],[c_211176,c_25968]) ).
tcf(c_211365,plain,
! [X0: $i] : join(iPr_def_13,join(X0,converse(complement(iPr_def_14)))) = join(X0,top),
inference(superposition,[status(thm)],[c_211212,c_208019]) ).
tcf(c_211371,plain,
! [X0: $i] : join(iPr_def_13,join(X0,converse(complement(iPr_def_14)))) = top,
inference(light_normalisation,[status(thm)],[c_211365,c_34132]) ).
tcf(c_218438,plain,
join(complement(join(iPr_def_18,iPr_def_18)),complement(top)) = iPr_def_17,
inference(superposition,[status(thm)],[c_73,c_208049]) ).
tcf(c_218455,plain,
join(complement(top),complement(join(iPr_def_18,iPr_def_18))) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_218438,c_64,c_63]) ).
tcf(c_218456,plain,
join(zero,complement(join(iPr_def_18,iPr_def_18))) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_218455,c_121]) ).
tcf(c_218483,plain,
join(zero,complement(iPr_def_17)) = join(iPr_def_18,iPr_def_18),
inference(superposition,[status(thm)],[c_218456,c_208066]) ).
tcf(c_218484,plain,
join(zero,iPr_def_18) = join(iPr_def_18,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_218483,c_138]) ).
tcf(c_218485,plain,
join(iPr_def_18,zero) = join(iPr_def_18,iPr_def_18),
inference(theory_normalisation,[status(thm)],[c_218484,c_64,c_63]) ).
tcf(c_220180,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(superposition,[status(thm)],[c_208066,c_208798]) ).
tcf(c_220197,plain,
! [X0: $i] : join(zero,complement(complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_208066,c_220180]) ).
tcf(c_220198,plain,
complement(join(iPr_def_10,iPr_def_10)) = sk1,
inference(demodulation,[status(thm)],[c_208847,c_220180]) ).
tcf(c_220199,plain,
complement(join(iPr_def_11,iPr_def_11)) = sk2,
inference(demodulation,[status(thm)],[c_209152,c_220180]) ).
tcf(c_220200,plain,
complement(join(iPr_def_20,zero)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_208773,c_220180]) ).
tcf(c_220201,plain,
complement(join(iPr_def_13,iPr_def_13)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_210169,c_220180]) ).
tcf(c_220202,plain,
complement(join(iPr_def_16,iPr_def_16)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_210569,c_220180]) ).
tcf(c_220203,plain,
complement(join(iPr_def_18,iPr_def_18)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_218456,c_220180]) ).
tcf(c_220218,plain,
! [X0: $i] : join(X0,zero) = X0,
inference(superposition,[status(thm)],[c_220180,c_63]) ).
tcf(c_220309,plain,
join(iPr_def_10,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_208936,c_220218]) ).
tcf(c_220310,plain,
join(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_209220,c_220218]) ).
tcf(c_220311,plain,
join(iPr_def_13,iPr_def_13) = iPr_def_13,
inference(demodulation,[status(thm)],[c_210285,c_220218]) ).
tcf(c_220312,plain,
join(iPr_def_16,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_210664,c_220218]) ).
tcf(c_220313,plain,
join(iPr_def_18,iPr_def_18) = iPr_def_18,
inference(demodulation,[status(thm)],[c_218485,c_220218]) ).
tcf(c_220717,plain,
! [X0: $i] : join(iPr_def_13,join(iPr_def_13,X0)) = join(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_220311,c_64]) ).
tcf(c_220815,plain,
complement(iPr_def_10) = sk1,
inference(light_normalisation,[status(thm)],[c_220198,c_220309]) ).
tcf(c_220822,plain,
join(complement(join(iPr_def_12,sk1)),complement(join(iPr_def_13,sk1))) = iPr_def_10,
inference(superposition,[status(thm)],[c_220815,c_208043]) ).
tcf(c_220839,plain,
join(zero,complement(join(iPr_def_13,sk1))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_220822,c_121,c_208972]) ).
tcf(c_220881,plain,
complement(iPr_def_11) = sk2,
inference(light_normalisation,[status(thm)],[c_220199,c_220310]) ).
tcf(c_220892,plain,
join(complement(join(iPr_def_12,sk2)),complement(join(iPr_def_13,sk2))) = iPr_def_11,
inference(superposition,[status(thm)],[c_220881,c_208043]) ).
tcf(c_220907,plain,
join(zero,complement(join(iPr_def_13,sk2))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_220892,c_121,c_209225]) ).
tcf(c_220928,plain,
complement(iPr_def_20) = iPr_def_19,
inference(demodulation,[status(thm)],[c_220200,c_220218]) ).
tcf(c_221156,plain,
complement(iPr_def_13) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_220201,c_220311]) ).
tcf(c_221201,plain,
complement(iPr_def_16) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_220202,c_220312]) ).
tcf(c_221202,plain,
join(complement(join(iPr_def_19,iPr_def_15)),complement(join(iPr_def_20,iPr_def_15))) = iPr_def_16,
inference(superposition,[status(thm)],[c_221201,c_208054]) ).
tcf(c_221238,plain,
join(complement(join(iPr_def_15,iPr_def_19)),complement(join(iPr_def_15,iPr_def_20))) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_221202,c_64,c_63]) ).
tcf(c_221239,plain,
join(zero,complement(join(iPr_def_15,iPr_def_20))) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_221238,c_121,c_208228]) ).
tcf(c_221271,plain,
complement(iPr_def_18) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_220203,c_220313]) ).
tcf(c_221278,plain,
join(complement(join(iPr_def_19,iPr_def_17)),complement(join(iPr_def_20,iPr_def_17))) = iPr_def_18,
inference(superposition,[status(thm)],[c_221271,c_208054]) ).
tcf(c_221313,plain,
join(complement(join(iPr_def_17,iPr_def_19)),complement(join(iPr_def_17,iPr_def_20))) = iPr_def_18,
inference(theory_normalisation,[status(thm)],[c_221278,c_64,c_63]) ).
tcf(c_221314,plain,
join(zero,complement(join(iPr_def_17,iPr_def_20))) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_221313,c_121,c_208455]) ).
tcf(c_221414,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(demodulation,[status(thm)],[c_220197,c_220180]) ).
tcf(c_221424,plain,
complement(iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_221156,c_221414]) ).
tcf(c_221425,plain,
complement(sk1) = iPr_def_10,
inference(superposition,[status(thm)],[c_220815,c_221414]) ).
tcf(c_221426,plain,
complement(sk2) = iPr_def_11,
inference(superposition,[status(thm)],[c_220881,c_221414]) ).
tcf(c_221429,plain,
complement(iPr_def_17) = iPr_def_18,
inference(superposition,[status(thm)],[c_221271,c_221414]) ).
tcf(c_221430,plain,
complement(iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_221201,c_221414]) ).
tcf(c_222283,plain,
complement(join(iPr_def_13,sk1)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_220839,c_220180]) ).
tcf(c_222284,plain,
join(iPr_def_13,sk1) = complement(iPr_def_10),
inference(superposition,[status(thm)],[c_222283,c_221414]) ).
tcf(c_222287,plain,
join(iPr_def_13,sk1) = sk1,
inference(light_normalisation,[status(thm)],[c_222284,c_220815]) ).
tcf(c_222295,plain,
! [X0: $i] : join(iPr_def_13,join(sk1,X0)) = join(sk1,X0),
inference(superposition,[status(thm)],[c_222287,c_64]) ).
tcf(c_222396,plain,
complement(join(iPr_def_13,sk2)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_220907,c_220180]) ).
tcf(c_222397,plain,
join(iPr_def_13,sk2) = complement(iPr_def_11),
inference(superposition,[status(thm)],[c_222396,c_221414]) ).
tcf(c_222400,plain,
join(iPr_def_13,sk2) = sk2,
inference(light_normalisation,[status(thm)],[c_222397,c_220881]) ).
tcf(c_222411,plain,
! [X0: $i] : join(iPr_def_13,join(sk2,X0)) = join(sk2,X0),
inference(superposition,[status(thm)],[c_222400,c_64]) ).
tcf(c_222819,plain,
complement(join(iPr_def_15,iPr_def_20)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_221239,c_220180]) ).
tcf(c_222820,plain,
join(iPr_def_15,iPr_def_20) = complement(iPr_def_16),
inference(superposition,[status(thm)],[c_222819,c_221414]) ).
tcf(c_222823,plain,
join(iPr_def_15,iPr_def_20) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_222820,c_221201]) ).
tcf(c_223125,plain,
join(sk1,converse(iPr_def_20)) = converse(iPr_def_15),
inference(superposition,[status(thm)],[c_222823,c_208137]) ).
tcf(c_223132,plain,
join(sk1,converse(iPr_def_20)) = sk1,
inference(light_normalisation,[status(thm)],[c_223125,c_208055]) ).
tcf(c_223184,plain,
complement(join(iPr_def_17,iPr_def_20)) = iPr_def_18,
inference(demodulation,[status(thm)],[c_221314,c_220180]) ).
tcf(c_223185,plain,
join(iPr_def_17,iPr_def_20) = complement(iPr_def_18),
inference(superposition,[status(thm)],[c_223184,c_221414]) ).
tcf(c_223188,plain,
join(iPr_def_17,iPr_def_20) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_223185,c_221271]) ).
tcf(c_223195,plain,
join(sk2,converse(iPr_def_20)) = converse(iPr_def_17),
inference(superposition,[status(thm)],[c_223188,c_208138]) ).
tcf(c_223202,plain,
join(sk2,converse(iPr_def_20)) = sk2,
inference(light_normalisation,[status(thm)],[c_223195,c_208056]) ).
tcf(c_224941,plain,
join(iPr_def_13,converse(iPr_def_21)) = converse(iPr_def_21),
inference(superposition,[status(thm)],[c_211177,c_220717]) ).
tcf(c_225734,plain,
join(sk1,converse(complement(iPr_def_14))) = top,
inference(superposition,[status(thm)],[c_222295,c_211371]) ).
tcf(c_225973,plain,
join(iPr_def_15,converse(converse(complement(iPr_def_14)))) = converse(top),
inference(superposition,[status(thm)],[c_225734,c_208130]) ).
tcf(c_225979,plain,
join(iPr_def_15,converse(converse(complement(iPr_def_14)))) = top,
inference(light_normalisation,[status(thm)],[c_225973,c_25968]) ).
tcf(c_226008,plain,
join(iPr_def_15,complement(iPr_def_14)) = top,
inference(demodulation,[status(thm)],[c_225979,c_69]) ).
tcf(c_226176,plain,
join(sk2,converse(complement(iPr_def_14))) = top,
inference(superposition,[status(thm)],[c_222411,c_211371]) ).
tcf(c_226422,plain,
join(iPr_def_17,converse(converse(complement(iPr_def_14)))) = converse(top),
inference(superposition,[status(thm)],[c_226176,c_208132]) ).
tcf(c_226428,plain,
join(iPr_def_17,converse(converse(complement(iPr_def_14)))) = top,
inference(light_normalisation,[status(thm)],[c_226422,c_25968]) ).
tcf(c_226431,plain,
join(iPr_def_17,complement(iPr_def_14)) = top,
inference(demodulation,[status(thm)],[c_226428,c_69]) ).
tcf(c_231250,plain,
! [X0: $i] : complement(join(complement(X0),complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_208101,c_220180]) ).
tcf(c_231273,plain,
! [X0: $i] : complement(join(X0,X0)) = complement(X0),
inference(superposition,[status(thm)],[c_221414,c_231250]) ).
tcf(c_231779,plain,
! [X0: $i] : join(X0,X0) = complement(complement(X0)),
inference(superposition,[status(thm)],[c_231273,c_221414]) ).
tcf(c_231782,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(light_normalisation,[status(thm)],[c_231779,c_221414]) ).
tcf(c_231798,plain,
! [X0: $i,X1: $i] : join(X0,join(X0,X1)) = join(X0,X1),
inference(superposition,[status(thm)],[c_231782,c_64]) ).
tcf(c_233579,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),X0) = X0,
inference(superposition,[status(thm)],[c_208119,c_231798]) ).
tcf(c_233585,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(theory_normalisation,[status(thm)],[c_233579,c_64,c_63]) ).
tcf(c_235263,plain,
join(complement(top),complement(join(complement(iPr_def_14),complement(iPr_def_17)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_226431,c_208120]) ).
tcf(c_235264,plain,
join(complement(top),complement(join(complement(iPr_def_14),complement(iPr_def_15)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_226008,c_208120]) ).
tcf(c_235337,plain,
! [X0: $i,X1: $i] : join(complement(join(X0,complement(X1))),X1) = X1,
inference(superposition,[status(thm)],[c_208120,c_231798]) ).
tcf(c_235343,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_235337,c_64,c_63]) ).
tcf(c_235348,plain,
join(zero,complement(join(complement(iPr_def_14),iPr_def_16))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_235264,c_121,c_221430]) ).
tcf(c_235349,plain,
join(zero,complement(join(iPr_def_16,complement(iPr_def_14)))) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_235348,c_64,c_63]) ).
tcf(c_235350,plain,
join(zero,complement(join(complement(iPr_def_14),iPr_def_18))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_235263,c_121,c_221429]) ).
tcf(c_235351,plain,
join(zero,complement(join(iPr_def_18,complement(iPr_def_14)))) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_235350,c_64,c_63]) ).
tcf(c_242795,plain,
! [X0: $i] : join(iPr_def_12,complement(join(iPr_def_13,X0))) = iPr_def_12,
inference(superposition,[status(thm)],[c_221424,c_233585]) ).
tcf(c_242807,plain,
! [X0: $i] : join(iPr_def_20,complement(join(iPr_def_19,X0))) = iPr_def_20,
inference(superposition,[status(thm)],[c_220928,c_233585]) ).
tcf(c_243200,plain,
join(iPr_def_12,complement(converse(iPr_def_21))) = iPr_def_12,
inference(superposition,[status(thm)],[c_224941,c_242795]) ).
tcf(c_247974,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(X1,X0))) = complement(X0),
inference(superposition,[status(thm)],[c_221414,c_235343]) ).
tcf(c_248409,plain,
complement(join(iPr_def_16,complement(iPr_def_14))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_235349,c_220180]) ).
tcf(c_248425,plain,
join(iPr_def_16,complement(iPr_def_14)) = complement(iPr_def_14),
inference(superposition,[status(thm)],[c_248409,c_221414]) ).
tcf(c_248487,plain,
complement(join(iPr_def_18,complement(iPr_def_14))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_235351,c_220180]) ).
tcf(c_248503,plain,
join(iPr_def_18,complement(iPr_def_14)) = complement(iPr_def_14),
inference(superposition,[status(thm)],[c_248487,c_221414]) ).
tcf(c_248581,plain,
join(iPr_def_16,complement(iPr_def_14)) = join(iPr_def_19,complement(iPr_def_14)),
inference(superposition,[status(thm)],[c_248503,c_208243]) ).
tcf(c_248591,plain,
join(iPr_def_19,complement(iPr_def_14)) = complement(iPr_def_14),
inference(light_normalisation,[status(thm)],[c_248581,c_248425]) ).
tcf(c_248605,plain,
join(iPr_def_20,complement(complement(iPr_def_14))) = iPr_def_20,
inference(superposition,[status(thm)],[c_248591,c_242807]) ).
tcf(c_248622,plain,
iPr_def_20 = iPr_def_21,
inference(demodulation,[status(thm)],[c_248605,c_63,c_141,c_221414]) ).
tcf(c_248628,plain,
join(iPr_def_12,complement(converse(iPr_def_20))) = iPr_def_12,
inference(demodulation,[status(thm)],[c_243200,c_248622]) ).
tcf(c_248691,plain,
( ( iPr_def_20 != iPr_def_20 )
| ( iPr_def_14 != iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_142,c_248622]) ).
tcf(c_248700,plain,
iPr_def_14 != iPr_def_20,
inference(equality_resolution_simp,[status(thm)],[c_248691]) ).
tcf(c_313746,plain,
join(complement(converse(iPr_def_20)),complement(sk1)) = complement(converse(iPr_def_20)),
inference(superposition,[status(thm)],[c_223132,c_247974]) ).
tcf(c_313957,plain,
join(complement(converse(iPr_def_20)),complement(sk2)) = complement(converse(iPr_def_20)),
inference(superposition,[status(thm)],[c_223202,c_247974]) ).
tcf(c_314350,plain,
join(complement(sk2),complement(converse(iPr_def_20))) = complement(converse(iPr_def_20)),
inference(theory_normalisation,[status(thm)],[c_313957,c_64,c_63]) ).
tcf(c_314351,plain,
join(iPr_def_11,complement(converse(iPr_def_20))) = complement(converse(iPr_def_20)),
inference(light_normalisation,[status(thm)],[c_314350,c_221426]) ).
tcf(c_314363,plain,
join(complement(sk1),complement(converse(iPr_def_20))) = complement(converse(iPr_def_20)),
inference(theory_normalisation,[status(thm)],[c_313746,c_64,c_63]) ).
tcf(c_314364,plain,
join(iPr_def_10,complement(converse(iPr_def_20))) = complement(converse(iPr_def_20)),
inference(light_normalisation,[status(thm)],[c_314363,c_221425]) ).
tcf(c_318308,plain,
join(iPr_def_10,complement(converse(iPr_def_20))) = join(iPr_def_12,complement(converse(iPr_def_20))),
inference(superposition,[status(thm)],[c_314351,c_208242]) ).
tcf(c_318318,plain,
complement(converse(iPr_def_20)) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_318308,c_248628,c_314364]) ).
tcf(c_318358,plain,
converse(iPr_def_20) = complement(iPr_def_12),
inference(superposition,[status(thm)],[c_318318,c_221414]) ).
tcf(c_318367,plain,
converse(iPr_def_20) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_318358,c_221424]) ).
tcf(c_318453,plain,
converse(iPr_def_13) = iPr_def_20,
inference(superposition,[status(thm)],[c_318367,c_69]) ).
tcf(c_318467,plain,
iPr_def_14 = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_318453,c_208060]) ).
tcf(c_318468,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_318467,c_248700]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL005-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/5.38 % Computer : n015.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Thu Sep 24 07:10:17 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.43
% 0.14/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.43
% 0.14/5.43 % Detected problem language: tptp
% 0.14/5.44 % Proving...
% 67.58/22.40 % SZS status Started for theBenchmark.p
% 67.58/22.40 % SZS status Unsatisfiable for theBenchmark.p
% 67.58/22.40
% 67.58/22.40 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 67.58/22.40
% 67.58/22.40 % ------ iProver source info
% 67.58/22.40
% 67.58/22.40 % git: date: 2026-07-19 20:42:38 +0200
% 67.58/22.40 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 67.58/22.40 % git: non_committed_changes: false
% 67.58/22.40
% 67.58/22.40 % ------ Parsing...% successful
% 67.58/22.40
% 67.58/22.40
% 67.58/22.40 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 67.58/22.40
% 67.58/22.40 % ------ Preprocessing... sup_sim: 1 sf_s rm: 0 0s sf_e pe_s pe_e %
% 67.58/22.40
% 67.58/22.40 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 67.58/22.40
% 67.58/22.40 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 67.58/22.40 % ------ Proving...
% 67.58/22.40 % ------ Problem Properties
% 67.58/22.40
% 67.58/22.40 %
% 67.58/22.40 % clauses 25
% 67.58/22.40 % conjectures 1
% 67.58/22.40 % EPR 1
% 67.58/22.40 % Horn 25
% 67.58/22.40 % unary 24
% 67.58/22.40 % binary 1
% 67.58/22.40 % lits 26
% 67.58/22.40 % lits eq 26
% 67.58/22.40 % fd_pure 0
% 67.58/22.40 % fd_pseudo 0
% 67.58/22.40 % fd_cond 0
% 67.58/22.40 % fd_pseudo_cond 0
% 67.58/22.40 % AC symbols 1
% 67.58/22.40
% 67.58/22.40 % ------ Schedule dynamic 5 is on
% 67.58/22.40
% 67.58/22.40 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 67.58/22.40
% 67.58/22.40
% 67.58/22.40 % ------
% 67.58/22.40 % Current options:
% 67.58/22.40 % ------
% 67.58/22.40
% 67.58/22.40
% 67.58/22.40 %
% 67.58/22.40
% 67.58/22.40 % ------ Proving...
% 67.58/22.40 % Proof_search_loop: time out after: 4505 full_loop iterations
% 67.58/22.40
% 67.58/22.40 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 67.58/22.40
% 67.58/22.40
% 67.58/22.40 % ------
% 67.58/22.40 % Current options:
% 67.58/22.40 % ------
% 67.58/22.40
% 67.58/22.40
% 67.58/22.40 %
% 67.58/22.40
% 67.58/22.40 % ------ Proving...
% 67.58/22.40 %
% 67.58/22.40
% 67.58/22.40 % SZS status Unsatisfiable for theBenchmark.p
% 67.58/22.40
% 67.58/22.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 67.58/22.41
% 67.58/22.41
%------------------------------------------------------------------------------