%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL012-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 : n005.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:35 PM UTC 2026
% Result : Unsatisfiable 196.06s 40.43s
% Output : CNFRefutation 196.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 20
% Syntax : Number of formulae : 172 ( 172 unt; 6 def)
% Number of atoms : 302 ( 171 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 7 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 194 ( 0 sgn 194 !; 0 ?; 162 :)
% 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,
join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)) != complement(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
complement(sk1) != join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)),
inference(reorient_equations,[],[f17]) ).
fof(f19,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,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_68,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_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(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)) != complement(sk1),
inference(cnf_transformation,[],[f18]) ).
tcf(c_88,negated_conjecture,
join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2))) != complement(sk1),
inference(theory_normalisation,[status(thm)],[c_75,c_64,c_63]) ).
tcf(c_89,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_90,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_125,definition,
iPr_def_10 = complement(sk1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_126,definition,
iPr_def_11 = composition(sk1,sk2),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_127,definition,
iPr_def_12 = complement(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_128,definition,
iPr_def_13 = converse(sk2),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_129,definition,
iPr_def_14 = composition(iPr_def_12,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_130,definition,
iPr_def_15 = join(iPr_def_10,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_131,negated_conjecture,
iPr_def_15 != iPr_def_10,
inference(demodulation,[status(thm)],[c_88,c_128,c_126,c_127,c_129,c_125,c_130]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(demodulation,[status(thm)],[c_89]) ).
tcf(c_134,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_135,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(demodulation,[status(thm)],[c_73]) ).
tcf(c_136,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_137,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_138,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i,X2: $i] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X0,X2),X1),
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_140,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_142,c_143]) ).
tcf(c_234,plain,
complement(top) = zero,
inference(superposition,[status(thm)],[c_135,c_134]) ).
tcf(c_235,plain,
! [X0: $i] : composition(iPr_def_13,converse(X0)) = converse(composition(X0,sk2)),
inference(superposition,[status(thm)],[c_128,c_136]) ).
tcf(c_236,plain,
! [X0: $i,X1: $i] : converse(composition(X0,converse(X1))) = composition(X1,converse(X0)),
inference(superposition,[status(thm)],[c_138,c_136]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_138,c_136]) ).
tcf(c_242,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_138,c_137]) ).
tcf(c_249,plain,
! [X0: $i,X1: $i] : composition(X0,composition(one,X1)) = composition(X0,X1),
inference(superposition,[status(thm)],[c_140,c_141]) ).
tcf(c_251,plain,
! [X0: $i] : composition(iPr_def_12,composition(iPr_def_13,X0)) = composition(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_129,c_141]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(join(X0,X1)))) = top,
inference(superposition,[status(thm)],[c_142,c_135]) ).
tcf(c_268,plain,
! [X0: $i] : join(complement(X0),composition(iPr_def_13,complement(composition(sk2,X0)))) = complement(X0),
inference(superposition,[status(thm)],[c_128,c_132]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(X1,complement(composition(converse(X1),X0)))) = complement(X0),
inference(superposition,[status(thm)],[c_138,c_132]) ).
tcf(c_280,plain,
! [X0: $i] : composition(join(sk1,X0),sk2) = join(iPr_def_11,composition(X0,sk2)),
inference(superposition,[status(thm)],[c_126,c_139]) ).
tcf(c_295,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(complement(complement(X0)))))) = X0,
inference(superposition,[status(thm)],[c_134,c_133]) ).
tcf(c_302,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_220,c_133]) ).
tcf(c_306,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),zero) = X0,
inference(superposition,[status(thm)],[c_134,c_133]) ).
tcf(c_307,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X1),complement(X0)))) = X0,
inference(superposition,[status(thm)],[c_143,c_133]) ).
tcf(c_314,plain,
! [X0: $i] : join(complement(join(complement(X0),sk1)),complement(join(complement(X0),iPr_def_10))) = X0,
inference(superposition,[status(thm)],[c_125,c_133]) ).
tcf(c_316,plain,
! [X0: $i] : join(complement(join(complement(X0),iPr_def_11)),complement(join(complement(X0),iPr_def_12))) = X0,
inference(superposition,[status(thm)],[c_127,c_133]) ).
tcf(c_319,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)) = join(complement(X0),X1),
inference(superposition,[status(thm)],[c_133,c_133]) ).
tcf(c_328,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_306,c_142,c_143]) ).
tcf(c_336,plain,
! [X0: $i] : join(complement(join(iPr_def_11,complement(X0))),complement(join(iPr_def_12,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_316,c_142,c_143]) ).
tcf(c_337,plain,
! [X0: $i] : join(complement(join(iPr_def_10,complement(X0))),complement(join(sk1,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_314,c_142,c_143]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(complement(X0),X1)))))) = join(complement(X0),X1),
inference(theory_normalisation,[status(thm)],[c_319,c_142,c_143]) ).
tcf(c_441,plain,
! [X0: $i,X1: $i] : join(converse(X0),composition(iPr_def_13,converse(X1))) = converse(join(X0,composition(X1,sk2))),
inference(superposition,[status(thm)],[c_235,c_137]) ).
tcf(c_496,plain,
! [X0: $i] : composition(sk2,converse(X0)) = converse(composition(X0,iPr_def_13)),
inference(superposition,[status(thm)],[c_128,c_236]) ).
tcf(c_527,plain,
composition(iPr_def_12,iPr_def_13) = composition(iPr_def_14,one),
inference(superposition,[status(thm)],[c_140,c_251]) ).
tcf(c_579,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_140,c_238]) ).
tcf(c_607,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[status(thm)],[c_135,c_242]) ).
tcf(c_779,plain,
! [X0: $i] : composition(iPr_def_13,converse(join(sk1,X0))) = converse(join(iPr_def_11,composition(X0,sk2))),
inference(superposition,[status(thm)],[c_280,c_235]) ).
tcf(c_982,plain,
join(complement(join(iPr_def_11,complement(iPr_def_12))),complement(top)) = iPr_def_12,
inference(superposition,[status(thm)],[c_135,c_336]) ).
tcf(c_994,plain,
join(complement(top),complement(join(sk1,complement(iPr_def_10)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_135,c_337]) ).
tcf(c_1103,plain,
! [X0: $i] : join(complement(join(complement(complement(X0)),X0)),zero) = complement(X0),
inference(superposition,[status(thm)],[c_134,c_307]) ).
tcf(c_1216,plain,
composition(iPr_def_12,iPr_def_13) = iPr_def_14,
inference(demodulation,[status(thm)],[c_527,c_140]) ).
tcf(c_1226,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(demodulation,[status(thm)],[c_579,c_138]) ).
tcf(c_1246,plain,
join(zero,complement(join(sk1,complement(iPr_def_10)))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_994,c_234]) ).
tcf(c_1247,plain,
join(complement(top),complement(join(iPr_def_11,complement(iPr_def_12)))) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_982,c_142,c_143]) ).
tcf(c_1248,plain,
join(zero,complement(join(iPr_def_11,complement(iPr_def_12)))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_1247,c_234]) ).
tcf(c_1261,plain,
! [X0: $i] : join(zero,complement(join(X0,complement(complement(X0))))) = complement(X0),
inference(theory_normalisation,[status(thm)],[c_1103,c_142,c_143]) ).
tcf(c_1580,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(ac_demodulation,[status(thm)],[c_295,c_1261,c_142,c_143]) ).
tcf(c_2709,plain,
complement(iPr_def_10) = sk1,
inference(superposition,[status(thm)],[c_125,c_1580]) ).
tcf(c_2710,plain,
complement(iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_127,c_1580]) ).
tcf(c_2725,plain,
! [X0: $i] : join(zero,complement(join(X0,X0))) = complement(X0),
inference(superposition,[status(thm)],[c_1580,c_328]) ).
tcf(c_2758,plain,
! [X0: $i] : join(complement(X0),composition(one,complement(X0))) = complement(X0),
inference(superposition,[status(thm)],[c_1226,c_269]) ).
tcf(c_2760,plain,
! [X0: $i] : composition(converse(one),X0) = composition(one,X0),
inference(superposition,[status(thm)],[c_1226,c_249]) ).
tcf(c_2821,plain,
composition(sk2,converse(iPr_def_12)) = converse(iPr_def_14),
inference(superposition,[status(thm)],[c_1216,c_496]) ).
tcf(c_3402,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(demodulation,[status(thm)],[c_2760,c_1226]) ).
tcf(c_3441,plain,
! [X0: $i] : join(complement(X0),complement(X0)) = complement(X0),
inference(demodulation,[status(thm)],[c_2758,c_3402]) ).
tcf(c_3856,plain,
join(zero,complement(join(sk1,sk1))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_1246,c_2709]) ).
tcf(c_3860,plain,
join(zero,complement(join(iPr_def_11,iPr_def_11))) = iPr_def_12,
inference(demodulation,[status(thm)],[c_1248,c_2710]) ).
tcf(c_3878,plain,
! [X0: $i] : join(zero,complement(complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_328,c_3441]) ).
tcf(c_3879,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(demodulation,[status(thm)],[c_3878,c_1580]) ).
tcf(c_4015,plain,
! [X0: $i] : join(X0,zero) = X0,
inference(superposition,[status(thm)],[c_3879,c_143]) ).
tcf(c_4211,plain,
! [X0: $i] : join(complement(X0),join(complement(X0),complement(complement(X0)))) = top,
inference(superposition,[status(thm)],[c_3441,c_257]) ).
tcf(c_4343,plain,
complement(sk1) = iPr_def_10,
inference(superposition,[status(thm)],[c_2725,c_3856]) ).
tcf(c_4344,plain,
complement(iPr_def_11) = iPr_def_12,
inference(superposition,[status(thm)],[c_2725,c_3860]) ).
tcf(c_4737,plain,
! [X0: $i] : join(top,complement(X0)) = top,
inference(demodulation,[status(thm)],[c_4211,c_143,c_135]) ).
tcf(c_5403,plain,
! [X0: $i] : join(top,X0) = top,
inference(superposition,[status(thm)],[c_1580,c_4737]) ).
tcf(c_5414,plain,
! [X0: $i] : join(X0,top) = top,
inference(superposition,[status(thm)],[c_4737,c_257]) ).
tcf(c_6442,plain,
converse(top) = top,
inference(superposition,[status(thm)],[c_5403,c_607]) ).
tcf(c_6925,plain,
! [X0: $i,X1: $i] : join(complement(join(X0,top)),complement(join(complement(X1),complement(join(X0,complement(complement(X1))))))) = X1,
inference(superposition,[status(thm)],[c_135,c_302]) ).
tcf(c_7527,plain,
! [X0: $i,X1: $i] : join(complement(top),complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(demodulation,[status(thm)],[c_6925,c_1580,c_5414]) ).
tcf(c_7528,plain,
! [X0: $i,X1: $i] : join(zero,complement(join(complement(X0),complement(join(X1,X0))))) = X0,
inference(light_normalisation,[status(thm)],[c_7527,c_234]) ).
tcf(c_7529,plain,
! [X0: $i,X1: $i] : complement(join(complement(X0),complement(join(X1,X0)))) = X0,
inference(ac_demodulation,[status(thm)],[c_7528,c_3879,c_142,c_143]) ).
tcf(c_7864,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = top,
inference(demodulation,[status(thm)],[c_607,c_6442]) ).
tcf(c_8247,plain,
! [X0: $i] : complement(join(iPr_def_10,complement(join(X0,sk1)))) = sk1,
inference(superposition,[status(thm)],[c_4343,c_7529]) ).
tcf(c_8263,plain,
! [X0: $i,X1: $i] : complement(join(complement(X0),complement(join(X0,X1)))) = X0,
inference(superposition,[status(thm)],[c_143,c_7529]) ).
tcf(c_8356,plain,
! [X0: $i,X1: $i] : join(complement(X0),complement(join(X1,X0))) = complement(X0),
inference(superposition,[status(thm)],[c_7529,c_1580]) ).
tcf(c_10367,plain,
! [X0: $i] : join(iPr_def_10,complement(join(X0,sk1))) = complement(sk1),
inference(superposition,[status(thm)],[c_8247,c_1580]) ).
tcf(c_11146,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(X0,join(complement(X1),complement(join(X0,X1)))))) = join(X0,X1),
inference(superposition,[status(thm)],[c_8263,c_347]) ).
tcf(c_11212,plain,
! [X0: $i] : join(iPr_def_10,complement(join(X0,sk1))) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_10367,c_4343]) ).
tcf(c_11430,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(X0,complement(X1)))) = join(X0,X1),
inference(demodulation,[status(thm)],[c_11146,c_8356]) ).
tcf(c_12164,plain,
! [X0: $i] : join(iPr_def_10,complement(join(sk1,X0))) = iPr_def_10,
inference(superposition,[status(thm)],[c_143,c_11212]) ).
tcf(c_12537,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(superposition,[status(thm)],[c_1580,c_8356]) ).
tcf(c_13545,plain,
! [X0: $i,X1: $i] : join(X0,converse(complement(join(X1,complement(converse(X0)))))) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_12537,c_242]) ).
tcf(c_14340,plain,
! [X0: $i,X1: $i] : join(X0,converse(complement(join(X1,complement(converse(X0)))))) = X0,
inference(demodulation,[status(thm)],[c_13545,c_138]) ).
tcf(c_24567,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(complement(X1),X0))) = join(X0,X1),
inference(superposition,[status(thm)],[c_143,c_11430]) ).
tcf(c_24683,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(X0,X1))) = join(X0,complement(X1)),
inference(superposition,[status(thm)],[c_1580,c_11430]) ).
tcf(c_35737,plain,
! [X0: $i] : join(converse(complement(converse(complement(X0)))),complement(top)) = join(converse(complement(converse(complement(X0)))),X0),
inference(superposition,[status(thm)],[c_7864,c_24567]) ).
tcf(c_35986,plain,
! [X0: $i] : join(X0,complement(converse(complement(converse(X0))))) = join(X0,complement(top)),
inference(superposition,[status(thm)],[c_7864,c_24683]) ).
tcf(c_36514,plain,
! [X0: $i] : join(X0,complement(converse(complement(converse(X0))))) = X0,
inference(light_normalisation,[status(thm)],[c_35986,c_234,c_4015]) ).
tcf(c_36995,plain,
! [X0: $i] : join(complement(top),converse(complement(converse(complement(X0))))) = join(X0,converse(complement(converse(complement(X0))))),
inference(theory_normalisation,[status(thm)],[c_35737,c_142,c_143]) ).
tcf(c_36996,plain,
! [X0: $i] : join(X0,converse(complement(converse(complement(X0))))) = join(zero,converse(complement(converse(complement(X0))))),
inference(light_normalisation,[status(thm)],[c_36995,c_234]) ).
tcf(c_36997,plain,
! [X0: $i] : join(X0,converse(complement(converse(complement(X0))))) = converse(complement(converse(complement(X0)))),
inference(ac_demodulation,[status(thm)],[c_36996,c_3879,c_142,c_143]) ).
tcf(c_37471,plain,
! [X0: $i] : join(converse(X0),complement(converse(complement(X0)))) = converse(X0),
inference(superposition,[status(thm)],[c_138,c_36514]) ).
tcf(c_37522,plain,
! [X0: $i] : join(X0,converse(complement(converse(complement(converse(converse(X0))))))) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_36514,c_242]) ).
tcf(c_37560,plain,
! [X0: $i] : join(complement(converse(X0)),converse(complement(X0))) = complement(converse(X0)),
inference(superposition,[status(thm)],[c_36514,c_14340]) ).
tcf(c_38557,plain,
! [X0: $i] : converse(complement(converse(complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_37522,c_138,c_36997]) ).
tcf(c_39610,plain,
! [X0: $i,X1: $i] : join(complement(converse(complement(X0))),converse(complement(join(X1,complement(X0))))) = complement(converse(complement(X0))),
inference(superposition,[status(thm)],[c_38557,c_14340]) ).
tcf(c_39643,plain,
! [X0: $i] : complement(converse(complement(X0))) = converse(X0),
inference(superposition,[status(thm)],[c_38557,c_138]) ).
tcf(c_39789,plain,
! [X0: $i] : join(converse(complement(X0)),complement(converse(X0))) = converse(complement(X0)),
inference(superposition,[status(thm)],[c_37471,c_12537]) ).
tcf(c_40611,plain,
! [X0: $i] : join(complement(converse(X0)),converse(complement(X0))) = converse(complement(X0)),
inference(theory_normalisation,[status(thm)],[c_39789,c_142,c_143]) ).
tcf(c_40612,plain,
! [X0: $i] : complement(converse(X0)) = converse(complement(X0)),
inference(demodulation,[status(thm)],[c_40611,c_37560]) ).
tcf(c_40961,plain,
! [X0: $i,X1: $i] : join(converse(X0),complement(converse(join(X1,complement(X0))))) = converse(X0),
inference(demodulation,[status(thm)],[c_39610,c_39643,c_40612]) ).
tcf(c_41428,plain,
complement(converse(iPr_def_11)) = converse(iPr_def_12),
inference(superposition,[status(thm)],[c_4344,c_40612]) ).
tcf(c_41433,plain,
complement(converse(iPr_def_12)) = converse(iPr_def_11),
inference(superposition,[status(thm)],[c_2710,c_40612]) ).
tcf(c_41472,plain,
! [X0: $i,X1: $i] : join(converse(X0),composition(iPr_def_13,complement(converse(X1)))) = converse(join(X0,composition(complement(X1),sk2))),
inference(superposition,[status(thm)],[c_40612,c_441]) ).
tcf(c_41480,plain,
! [X0: $i,X1: $i] : join(converse(X0),complement(converse(X1))) = converse(join(X0,complement(X1))),
inference(superposition,[status(thm)],[c_40612,c_137]) ).
tcf(c_41481,plain,
! [X0: $i,X1: $i] : composition(converse(X0),complement(converse(X1))) = converse(composition(complement(X1),X0)),
inference(superposition,[status(thm)],[c_40612,c_136]) ).
tcf(c_42424,plain,
join(converse(iPr_def_11),composition(iPr_def_13,complement(composition(sk2,converse(iPr_def_12))))) = converse(iPr_def_11),
inference(superposition,[status(thm)],[c_41433,c_268]) ).
tcf(c_43042,plain,
join(converse(iPr_def_11),composition(iPr_def_13,complement(converse(iPr_def_14)))) = converse(iPr_def_11),
inference(light_normalisation,[status(thm)],[c_42424,c_2821]) ).
tcf(c_82380,plain,
join(converse(iPr_def_11),complement(composition(iPr_def_13,complement(converse(iPr_def_14))))) = join(converse(iPr_def_11),complement(converse(iPr_def_11))),
inference(superposition,[status(thm)],[c_43042,c_24683]) ).
tcf(c_83270,plain,
join(converse(iPr_def_11),complement(composition(iPr_def_13,complement(converse(iPr_def_14))))) = converse(top),
inference(demodulation,[status(thm)],[c_82380,c_135,c_41480]) ).
tcf(c_83271,plain,
join(converse(iPr_def_11),complement(composition(iPr_def_13,complement(converse(iPr_def_14))))) = top,
inference(light_normalisation,[status(thm)],[c_83270,c_6442]) ).
tcf(c_112704,plain,
join(converse(iPr_def_11),complement(complement(composition(iPr_def_13,complement(converse(iPr_def_14)))))) = join(converse(iPr_def_11),complement(top)),
inference(superposition,[status(thm)],[c_83271,c_24683]) ).
tcf(c_112929,plain,
join(converse(iPr_def_11),complement(complement(composition(iPr_def_13,complement(converse(iPr_def_14)))))) = join(complement(top),converse(iPr_def_11)),
inference(theory_normalisation,[status(thm)],[c_112704,c_142,c_143]) ).
tcf(c_112930,plain,
composition(iPr_def_13,converse(join(sk1,complement(iPr_def_14)))) = join(complement(top),converse(iPr_def_11)),
inference(demodulation,[status(thm)],[c_112929,c_779,c_1580,c_41472]) ).
tcf(c_112931,plain,
composition(iPr_def_13,converse(join(sk1,complement(iPr_def_14)))) = join(zero,converse(iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_112930,c_234]) ).
tcf(c_112932,plain,
composition(iPr_def_13,converse(join(sk1,complement(iPr_def_14)))) = converse(iPr_def_11),
inference(ac_demodulation,[status(thm)],[c_112931,c_3879,c_142,c_143]) ).
tcf(c_113457,plain,
join(complement(converse(join(sk1,complement(iPr_def_14)))),composition(converse(iPr_def_13),complement(converse(iPr_def_11)))) = complement(converse(join(sk1,complement(iPr_def_14)))),
inference(superposition,[status(thm)],[c_112932,c_132]) ).
tcf(c_114384,plain,
join(composition(sk2,complement(converse(iPr_def_11))),complement(converse(join(sk1,complement(iPr_def_14))))) = complement(converse(join(sk1,complement(iPr_def_14)))),
inference(demodulation,[status(thm)],[c_113457,c_143,c_496,c_40612,c_41481]) ).
tcf(c_114385,plain,
join(converse(iPr_def_14),complement(converse(join(sk1,complement(iPr_def_14))))) = complement(converse(join(sk1,complement(iPr_def_14)))),
inference(light_normalisation,[status(thm)],[c_114384,c_2821,c_41428]) ).
tcf(c_114386,plain,
complement(converse(join(sk1,complement(iPr_def_14)))) = converse(iPr_def_14),
inference(demodulation,[status(thm)],[c_114385,c_40961]) ).
tcf(c_115188,plain,
complement(converse(converse(join(sk1,complement(iPr_def_14))))) = converse(converse(iPr_def_14)),
inference(superposition,[status(thm)],[c_114386,c_40612]) ).
tcf(c_115550,plain,
complement(join(sk1,complement(iPr_def_14))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_115188,c_138]) ).
tcf(c_116193,plain,
join(iPr_def_10,iPr_def_14) = iPr_def_10,
inference(superposition,[status(thm)],[c_115550,c_12164]) ).
tcf(c_119001,plain,
iPr_def_10 = iPr_def_15,
inference(demodulation,[status(thm)],[c_130,c_116193]) ).
tcf(c_119126,plain,
iPr_def_10 != iPr_def_10,
inference(demodulation,[status(thm)],[c_131,c_119001]) ).
tcf(c_119127,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_119126]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL012-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.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:10:33 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.40 Running UEQ theorem proving
% 0.09/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.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 196.06/40.43 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 196.06/40.43 % SZS status Started for theBenchmark.p
% 196.06/40.43 % SZS status Unsatisfiable for theBenchmark.p
% 196.06/40.43
% 196.06/40.43 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 196.06/40.43
% 196.06/40.43 % ------ iProver source info
% 196.06/40.43
% 196.06/40.43 % git: date: 2026-07-19 20:42:38 +0200
% 196.06/40.43 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 196.06/40.43 % git: non_committed_changes: false
% 196.06/40.43
% 196.06/40.43 % ------ Parsing...% successful
% 196.06/40.43
% 196.06/40.43
% 196.06/40.43 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 196.06/40.43
% 196.06/40.43 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 196.06/40.43
% 196.06/40.43 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 196.06/40.43
% 196.06/40.43 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 196.06/40.43 % ------ Proving...
% 196.06/40.43 % ------ Problem Properties
% 196.06/40.43
% 196.06/40.43 %
% 196.06/40.43 % clauses 19
% 196.06/40.43 % conjectures 1
% 196.06/40.43 % EPR 1
% 196.06/40.43 % Horn 19
% 196.06/40.43 % unary 19
% 196.06/40.43 % binary 0
% 196.06/40.43 % lits 19
% 196.06/40.43 % lits eq 19
% 196.06/40.43 % fd_pure 0
% 196.06/40.43 % fd_pseudo 0
% 196.06/40.43 % fd_cond 0
% 196.06/40.43 % fd_pseudo_cond 0
% 196.06/40.43 % AC symbols 1
% 196.06/40.43
% 196.06/40.43 % ------ Input Options Time Limit: Unbounded
% 196.06/40.43
% 196.06/40.43
% 196.06/40.43 % ------
% 196.06/40.43 % Current options:
% 196.06/40.43 % ------
% 196.06/40.43
% 196.06/40.43
% 196.06/40.43 %
% 196.06/40.43
% 196.06/40.43 % ------ Proving...
% 196.06/40.43 %
% 196.06/40.43
% 196.06/40.43 % SZS status Unsatisfiable for theBenchmark.p
% 196.06/40.43
% 196.06/40.43 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 196.06/40.43
% 196.06/40.43
%------------------------------------------------------------------------------