%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : REL050-3 : 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 : n016.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:37:06 PM UTC 2026
% Result : Unsatisfiable 8.14s 3.74s
% Output : CNFRefutation 8.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 17
% Syntax : Number of formulae : 159 ( 159 unt; 3 def)
% Number of atoms : 238 ( 158 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 175 ( 0 sgn 175 !; 0 ?; 143 :)
% 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(f23,negated_conjecture,
complement(composition(sk1,top)) != composition(complement(composition(sk1,top)),top),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_17) ).
fof(f24,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_70,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(cnf_transformation,[],[f8]) ).
tcf(c_71,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_72,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(cnf_transformation,[],[f10]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(cnf_transformation,[],[f11]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[],[f14]) ).
tcf(c_76,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(cnf_transformation,[],[f15]) ).
tcf(c_77,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(cnf_transformation,[],[f24]) ).
tcf(c_81,negated_conjecture,
composition(complement(composition(sk1,top)),top) != complement(composition(sk1,top)),
inference(cnf_transformation,[],[f23]) ).
tcf(c_135,definition,
iPr_def_10 = composition(sk1,top),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_136,definition,
iPr_def_11 = complement(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_137,definition,
iPr_def_12 = composition(iPr_def_11,top),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_138,negated_conjecture,
iPr_def_12 != iPr_def_11,
inference(demodulation,[status(thm)],[c_81,c_135,c_136,c_137]) ).
tcf(c_142,plain,
! [X0: $i] : complement(join(complement(X0),complement(complement(X0)))) = zero,
inference(demodulation,[status(thm)],[c_77]) ).
tcf(c_143,plain,
! [X0: $i] : join(X0,complement(X0)) = top,
inference(demodulation,[status(thm)],[c_76]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(demodulation,[status(thm)],[c_75]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] : composition(converse(X0),converse(X1)) = converse(composition(X1,X0)),
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(X1)) = converse(join(X0,X1)),
inference(demodulation,[status(thm)],[c_73]) ).
tcf(c_147,plain,
! [X0: $i] : converse(converse(X0)) = X0,
inference(demodulation,[status(thm)],[c_72]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i] : join(composition(X0,X1),composition(X2,X1)) = composition(join(X0,X2),X1),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_149,plain,
! [X0: $i] : composition(X0,one) = X0,
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i] : composition(composition(X0,X1),X2) = composition(X0,composition(X1,X2)),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_230,plain,
complement(top) = zero,
inference(demodulation,[status(thm)],[c_142,c_143]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(demodulation,[status(thm)],[c_144,c_153]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(demodulation,[status(thm)],[c_151,c_153]) ).
tcf(c_235,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_152,c_153]) ).
tcf(c_247,plain,
join(top,zero) = top,
inference(superposition,[status(thm)],[c_230,c_143]) ).
tcf(c_248,plain,
join(iPr_def_10,iPr_def_11) = top,
inference(superposition,[status(thm)],[c_136,c_143]) ).
tcf(c_250,plain,
! [X0: $i,X1: $i] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[status(thm)],[c_147,c_145]) ).
tcf(c_253,plain,
! [X0: $i,X1: $i] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[status(thm)],[c_147,c_146]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(superposition,[status(thm)],[c_147,c_146]) ).
tcf(c_258,plain,
! [X0: $i] : composition(sk1,composition(top,X0)) = composition(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_135,c_150]) ).
tcf(c_261,plain,
! [X0: $i] : composition(iPr_def_11,composition(top,X0)) = composition(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_137,c_150]) ).
tcf(c_265,plain,
! [X0: $i,X1: $i] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[status(thm)],[c_143,c_152]) ).
tcf(c_269,plain,
! [X0: $i] : composition(join(sk1,X0),top) = join(iPr_def_10,composition(X0,top)),
inference(superposition,[status(thm)],[c_135,c_148]) ).
tcf(c_273,plain,
! [X0: $i] : composition(join(iPr_def_11,X0),top) = join(iPr_def_12,composition(X0,top)),
inference(superposition,[status(thm)],[c_137,c_148]) ).
tcf(c_274,plain,
! [X0: $i] : composition(join(X0,sk1),top) = join(composition(X0,top),iPr_def_10),
inference(superposition,[status(thm)],[c_135,c_148]) ).
tcf(c_303,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X0))) = join(X1,top),
inference(superposition,[status(thm)],[c_143,c_235]) ).
tcf(c_323,plain,
! [X0: $i] : join(zero,composition(converse(X0),complement(composition(X0,top)))) = zero,
inference(superposition,[status(thm)],[c_230,c_231]) ).
tcf(c_324,plain,
! [X0: $i] : join(iPr_def_11,composition(converse(X0),complement(composition(X0,iPr_def_10)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_136,c_231]) ).
tcf(c_362,plain,
! [X0: $i] : join(complement(join(complement(X0),complement(X0))),complement(top)) = X0,
inference(superposition,[status(thm)],[c_143,c_232]) ).
tcf(c_551,plain,
join(iPr_def_11,iPr_def_10) = top,
inference(theory_normalisation,[status(thm)],[c_248,c_152,c_153]) ).
tcf(c_552,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_362,c_152,c_153]) ).
tcf(c_553,plain,
! [X0: $i] : join(zero,complement(join(complement(X0),complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_552,c_230]) ).
tcf(c_557,plain,
! [X0: $i] : composition(join(X0,sk1),top) = join(iPr_def_10,composition(X0,top)),
inference(theory_normalisation,[status(thm)],[c_274,c_152,c_153]) ).
tcf(c_750,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_10,X0)) = join(top,X0),
inference(superposition,[status(thm)],[c_551,c_152]) ).
tcf(c_805,plain,
! [X0: $i] : composition(converse(one),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_149,c_250]) ).
tcf(c_824,plain,
! [X0: $i,X1: $i] : converse(join(X0,converse(X1))) = join(X1,converse(X0)),
inference(superposition,[status(thm)],[c_153,c_253]) ).
tcf(c_828,plain,
! [X0: $i] : join(X0,converse(complement(converse(X0)))) = converse(top),
inference(superposition,[status(thm)],[c_143,c_253]) ).
tcf(c_873,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X0))) = join(top,X1),
inference(superposition,[status(thm)],[c_153,c_265]) ).
tcf(c_876,plain,
! [X0: $i] : join(top,complement(complement(X0))) = join(X0,top),
inference(superposition,[status(thm)],[c_143,c_265]) ).
tcf(c_939,plain,
! [X0: $i] : join(iPr_def_10,join(X0,iPr_def_11)) = join(X0,top),
inference(superposition,[status(thm)],[c_136,c_303]) ).
tcf(c_959,plain,
! [X0: $i] : join(join(complement(X0),complement(X0)),X0) = join(zero,top),
inference(superposition,[status(thm)],[c_553,c_303]) ).
tcf(c_986,plain,
! [X0: $i] : join(iPr_def_11,composition(X0,complement(composition(converse(X0),iPr_def_10)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_147,c_324]) ).
tcf(c_998,plain,
! [X0: $i] : composition(converse(one),X0) = X0,
inference(demodulation,[status(thm)],[c_805,c_147]) ).
tcf(c_1000,plain,
! [X0: $i] : join(iPr_def_11,join(X0,iPr_def_10)) = join(X0,top),
inference(theory_normalisation,[status(thm)],[c_939,c_152,c_153]) ).
tcf(c_1002,plain,
! [X0: $i] : join(X0,join(complement(X0),complement(X0))) = join(top,zero),
inference(theory_normalisation,[status(thm)],[c_959,c_152,c_153]) ).
tcf(c_1003,plain,
! [X0: $i] : join(top,complement(X0)) = top,
inference(demodulation,[status(thm)],[c_1002,c_247,c_265]) ).
tcf(c_1517,plain,
! [X0: $i,X1: $i] : composition(converse(one),composition(X0,X1)) = composition(X0,X1),
inference(superposition,[status(thm)],[c_998,c_150]) ).
tcf(c_1522,plain,
converse(one) = one,
inference(superposition,[status(thm)],[c_998,c_149]) ).
tcf(c_1523,plain,
! [X0: $i,X1: $i] : composition(join(X0,converse(one)),X1) = join(composition(X0,X1),X1),
inference(superposition,[status(thm)],[c_998,c_148]) ).
tcf(c_1527,plain,
! [X0: $i] : join(complement(X0),complement(composition(one,X0))) = complement(X0),
inference(superposition,[status(thm)],[c_998,c_231]) ).
tcf(c_1533,plain,
composition(join(sk1,converse(one)),top) = join(iPr_def_10,top),
inference(superposition,[status(thm)],[c_998,c_269]) ).
tcf(c_1534,plain,
join(zero,complement(composition(one,top))) = zero,
inference(superposition,[status(thm)],[c_998,c_323]) ).
tcf(c_1603,plain,
! [X0: $i] : join(X0,top) = top,
inference(superposition,[status(thm)],[c_876,c_1003]) ).
tcf(c_1676,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_10,X0)) = join(X0,top),
inference(superposition,[status(thm)],[c_153,c_1000]) ).
tcf(c_1736,plain,
! [X0: $i,X1: $i,X2: $i] : composition(join(X0,converse(X1)),converse(X2)) = converse(composition(X2,join(X1,converse(X0)))),
inference(superposition,[status(thm)],[c_824,c_145]) ).
tcf(c_1770,plain,
! [X0: $i] : join(X0,top) = join(top,X0),
inference(superposition,[status(thm)],[c_873,c_303]) ).
tcf(c_1776,plain,
! [X0: $i] : join(top,X0) = top,
inference(demodulation,[status(thm)],[c_1770,c_1603]) ).
tcf(c_1792,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_10,X0)) = top,
inference(demodulation,[status(thm)],[c_1676,c_1603]) ).
tcf(c_1810,plain,
composition(join(sk1,one),top) = top,
inference(demodulation,[status(thm)],[c_1533,c_1522,c_1603]) ).
tcf(c_1814,plain,
! [X0: $i,X1: $i] : composition(one,composition(X0,X1)) = composition(X0,X1),
inference(demodulation,[status(thm)],[c_1517,c_1522]) ).
tcf(c_1841,plain,
! [X0: $i,X1: $i] : join(composition(X0,X1),X1) = composition(join(X0,one),X1),
inference(demodulation,[status(thm)],[c_1523,c_1522]) ).
tcf(c_1842,plain,
! [X0: $i,X1: $i] : join(X0,composition(X1,X0)) = composition(join(X1,one),X0),
inference(theory_normalisation,[status(thm)],[c_1841,c_152,c_153]) ).
tcf(c_1981,plain,
! [X0: $i] : join(complement(X0),composition(one,complement(composition(one,X0)))) = complement(X0),
inference(superposition,[status(thm)],[c_1522,c_231]) ).
tcf(c_1984,plain,
join(one,converse(complement(one))) = converse(top),
inference(superposition,[status(thm)],[c_1522,c_828]) ).
tcf(c_1986,plain,
join(zero,composition(one,complement(composition(one,top)))) = zero,
inference(superposition,[status(thm)],[c_1522,c_323]) ).
tcf(c_2004,plain,
! [X0: $i] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[status(thm)],[c_1603,c_232]) ).
tcf(c_2039,plain,
converse(top) = top,
inference(superposition,[status(thm)],[c_1776,c_828]) ).
tcf(c_2089,plain,
! [X0: $i] : composition(one,X0) = X0,
inference(superposition,[status(thm)],[c_998,c_1814]) ).
tcf(c_2162,plain,
! [X0: $i] : join(complement(join(complement(X0),composition(one,X0))),complement(complement(X0))) = X0,
inference(superposition,[status(thm)],[c_1527,c_232]) ).
tcf(c_2217,plain,
composition(one,top) = top,
inference(superposition,[status(thm)],[c_1810,c_1814]) ).
tcf(c_2253,plain,
join(one,converse(complement(one))) = top,
inference(demodulation,[status(thm)],[c_1984,c_2039]) ).
tcf(c_2271,plain,
join(zero,complement(top)) = zero,
inference(demodulation,[status(thm)],[c_1986,c_2089,c_2217]) ).
tcf(c_2272,plain,
join(zero,zero) = zero,
inference(demodulation,[status(thm)],[c_2271,c_230]) ).
tcf(c_2291,plain,
! [X0: $i] : join(zero,complement(join(zero,complement(X0)))) = X0,
inference(demodulation,[status(thm)],[c_2004,c_153,c_230]) ).
tcf(c_2296,plain,
! [X0: $i] : join(complement(X0),complement(X0)) = complement(X0),
inference(demodulation,[status(thm)],[c_1981,c_2089]) ).
tcf(c_2303,plain,
! [X0: $i] : join(complement(join(complement(X0),X0)),complement(complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_2162,c_2089]) ).
tcf(c_2304,plain,
! [X0: $i] : join(complement(complement(X0)),complement(join(X0,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_2303,c_152,c_153]) ).
tcf(c_2305,plain,
! [X0: $i] : join(zero,complement(complement(X0))) = X0,
inference(demodulation,[status(thm)],[c_2304,c_153,c_143,c_230]) ).
tcf(c_2405,plain,
! [X0: $i,X1: $i] : join(X0,composition(X1,X0)) = composition(join(one,X1),X0),
inference(superposition,[status(thm)],[c_2089,c_148]) ).
tcf(c_2472,plain,
! [X0: $i] : join(zero,join(zero,X0)) = join(zero,X0),
inference(superposition,[status(thm)],[c_2272,c_152]) ).
tcf(c_2549,plain,
! [X0: $i] : join(iPr_def_11,composition(join(X0,sk1),top)) = top,
inference(superposition,[status(thm)],[c_557,c_1792]) ).
tcf(c_2550,plain,
! [X0: $i] : join(iPr_def_11,composition(join(X0,sk1),top)) = join(top,composition(X0,top)),
inference(superposition,[status(thm)],[c_557,c_750]) ).
tcf(c_2579,plain,
join(zero,complement(iPr_def_11)) = iPr_def_10,
inference(superposition,[status(thm)],[c_136,c_2305]) ).
tcf(c_2587,plain,
! [X0: $i] : join(zero,complement(X0)) = complement(X0),
inference(superposition,[status(thm)],[c_2305,c_2291]) ).
tcf(c_2596,plain,
join(zero,complement(zero)) = composition(one,top),
inference(superposition,[status(thm)],[c_1534,c_2291]) ).
tcf(c_2629,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(composition(X0,X1))) = composition(join(converse(X1),one),converse(X0)),
inference(superposition,[status(thm)],[c_145,c_1842]) ).
tcf(c_2663,plain,
composition(one,top) = complement(zero),
inference(demodulation,[status(thm)],[c_2596,c_2587]) ).
tcf(c_2664,plain,
complement(zero) = top,
inference(demodulation,[status(thm)],[c_2663,c_2217]) ).
tcf(c_2748,plain,
! [X0: $i] : composition(join(one,X0),top) = top,
inference(demodulation,[status(thm)],[c_2550,c_2405,c_2549]) ).
tcf(c_2785,plain,
! [X0: $i,X1: $i] : join(converse(X0),converse(composition(X0,X1))) = composition(join(one,converse(X1)),converse(X0)),
inference(theory_normalisation,[status(thm)],[c_2629,c_152,c_153]) ).
tcf(c_2786,plain,
! [X0: $i,X1: $i] : converse(join(X0,composition(X0,X1))) = converse(composition(X0,join(X1,one))),
inference(demodulation,[status(thm)],[c_2785,c_146,c_1522,c_1736]) ).
tcf(c_2878,plain,
join(zero,complement(iPr_def_10)) = iPr_def_11,
inference(superposition,[status(thm)],[c_2579,c_2291]) ).
tcf(c_2954,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(superposition,[status(thm)],[c_2587,c_2305]) ).
tcf(c_3019,plain,
! [X0: $i] : join(zero,X0) = X0,
inference(superposition,[status(thm)],[c_2291,c_2472]) ).
tcf(c_3068,plain,
composition(top,top) = top,
inference(superposition,[status(thm)],[c_2253,c_2748]) ).
tcf(c_3093,plain,
! [X0: $i] : join(complement(join(complement(X0),X0)),complement(complement(X0))) = X0,
inference(superposition,[status(thm)],[c_2296,c_232]) ).
tcf(c_3113,plain,
complement(iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2878,c_3019]) ).
tcf(c_3142,plain,
! [X0: $i] : join(complement(join(complement(X0),X0)),X0) = X0,
inference(demodulation,[status(thm)],[c_3093,c_2954]) ).
tcf(c_3143,plain,
! [X0: $i] : join(X0,complement(join(X0,complement(X0)))) = X0,
inference(theory_normalisation,[status(thm)],[c_3142,c_152,c_153]) ).
tcf(c_3144,plain,
! [X0: $i] : join(X0,zero) = X0,
inference(demodulation,[status(thm)],[c_3143,c_143,c_230]) ).
tcf(c_3437,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(superposition,[status(thm)],[c_2954,c_2296]) ).
tcf(c_3498,plain,
! [X0: $i] : join(converse(zero),X0) = converse(converse(X0)),
inference(superposition,[status(thm)],[c_3019,c_254]) ).
tcf(c_3536,plain,
composition(iPr_def_11,top) = composition(iPr_def_12,top),
inference(superposition,[status(thm)],[c_3068,c_261]) ).
tcf(c_3537,plain,
composition(sk1,top) = composition(iPr_def_10,top),
inference(superposition,[status(thm)],[c_3068,c_258]) ).
tcf(c_3557,plain,
composition(iPr_def_10,top) = iPr_def_10,
inference(demodulation,[status(thm)],[c_3537,c_135]) ).
tcf(c_3558,plain,
composition(iPr_def_12,top) = iPr_def_12,
inference(demodulation,[status(thm)],[c_3536,c_137]) ).
tcf(c_3564,plain,
! [X0: $i] : join(converse(zero),X0) = X0,
inference(demodulation,[status(thm)],[c_3498,c_147]) ).
tcf(c_3902,plain,
join(zero,composition(converse(iPr_def_10),complement(iPr_def_10))) = zero,
inference(superposition,[status(thm)],[c_3557,c_323]) ).
tcf(c_3917,plain,
composition(join(iPr_def_11,iPr_def_12),top) = join(iPr_def_12,iPr_def_12),
inference(superposition,[status(thm)],[c_3558,c_273]) ).
tcf(c_3925,plain,
composition(join(iPr_def_11,iPr_def_12),top) = iPr_def_12,
inference(demodulation,[status(thm)],[c_3917,c_3437]) ).
tcf(c_3935,plain,
composition(converse(iPr_def_10),iPr_def_11) = zero,
inference(demodulation,[status(thm)],[c_3902,c_3019,c_3113]) ).
tcf(c_4289,plain,
converse(zero) = zero,
inference(superposition,[status(thm)],[c_3564,c_3144]) ).
tcf(c_4626,plain,
composition(converse(iPr_def_11),iPr_def_10) = converse(zero),
inference(superposition,[status(thm)],[c_3935,c_250]) ).
tcf(c_4705,plain,
composition(converse(iPr_def_11),iPr_def_10) = zero,
inference(demodulation,[status(thm)],[c_4626,c_4289]) ).
tcf(c_5193,plain,
join(iPr_def_11,composition(iPr_def_11,complement(zero))) = iPr_def_11,
inference(superposition,[status(thm)],[c_4705,c_986]) ).
tcf(c_5314,plain,
join(iPr_def_11,iPr_def_12) = iPr_def_11,
inference(demodulation,[status(thm)],[c_5193,c_137,c_2664]) ).
tcf(c_5540,plain,
composition(iPr_def_11,top) = iPr_def_12,
inference(superposition,[status(thm)],[c_5314,c_3925]) ).
tcf(c_18635,plain,
! [X0: $i,X1: $i] : converse(converse(composition(X0,join(X1,one)))) = join(X0,composition(X0,X1)),
inference(superposition,[status(thm)],[c_2786,c_147]) ).
tcf(c_18673,plain,
! [X0: $i,X1: $i] : join(X0,composition(X0,X1)) = composition(X0,join(X1,one)),
inference(demodulation,[status(thm)],[c_18635,c_147]) ).
tcf(c_19517,plain,
composition(iPr_def_11,join(top,one)) = join(iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_5540,c_18673]) ).
tcf(c_19731,plain,
iPr_def_11 = iPr_def_12,
inference(demodulation,[status(thm)],[c_19517,c_1776,c_5314,c_5540]) ).
tcf(c_20131,plain,
$false,
inference(superposition,[status(thm)],[c_19731,c_138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050-3 : 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.37 % Computer : n016.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 07:43:45 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.41 Running UEQ theorem proving
% 0.08/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.43
% 0.08/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.43
% 0.08/0.43 % Detected problem language: tptp
% 0.08/0.44 % Proving...
% 8.14/3.74 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 8.14/3.74 % SZS status Started for theBenchmark.p
% 8.14/3.74 % SZS status Unsatisfiable for theBenchmark.p
% 8.14/3.74
% 8.14/3.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.14/3.74
% 8.14/3.74 % ------ iProver source info
% 8.14/3.74
% 8.14/3.74 % git: date: 2026-07-19 20:42:38 +0200
% 8.14/3.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.14/3.74 % git: non_committed_changes: false
% 8.14/3.74
% 8.14/3.74 % ------ Parsing...% successful
% 8.14/3.74
% 8.14/3.74
% 8.14/3.74 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.14/3.74
% 8.14/3.74 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 8.14/3.74
% 8.14/3.74 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.14/3.74
% 8.14/3.74 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 8.14/3.74 % ------ Proving...
% 8.14/3.74 % ------ Problem Properties
% 8.14/3.74
% 8.14/3.74 %
% 8.14/3.74 % clauses 19
% 8.14/3.74 % conjectures 1
% 8.14/3.74 % EPR 1
% 8.14/3.74 % Horn 19
% 8.14/3.74 % unary 19
% 8.14/3.74 % binary 0
% 8.14/3.74 % lits 19
% 8.14/3.74 % lits eq 19
% 8.14/3.74 % fd_pure 0
% 8.14/3.74 % fd_pseudo 0
% 8.14/3.74 % fd_cond 0
% 8.14/3.74 % fd_pseudo_cond 0
% 8.14/3.74 % AC symbols 1
% 8.14/3.74
% 8.14/3.74 % ------ Input Options Time Limit: Unbounded
% 8.14/3.74
% 8.14/3.74
% 8.14/3.74 % ------
% 8.14/3.74 % Current options:
% 8.14/3.74 % ------
% 8.14/3.74
% 8.14/3.74
% 8.14/3.74 %
% 8.14/3.74
% 8.14/3.74 % ------ Proving...
% 8.14/3.74 %
% 8.14/3.74
% 8.14/3.74 % SZS status Unsatisfiable for theBenchmark.p
% 8.14/3.74
% 8.14/3.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.14/3.74
% 8.14/3.74
%------------------------------------------------------------------------------