%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n003.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 01:58:06 PM UTC 2026
% Result : Unsatisfiable 6.80s 6.68s
% Output : CNFRefutation 6.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 31
% Syntax : Number of formulae : 146 ( 146 unt; 23 def)
% Number of atoms : 427 ( 145 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 23 usr; 24 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 69 ( 0 sgn 69 !; 0 ?; 52 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : join(complement(X0),X0) = n1,
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',top) ).
fof(f3,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',absorption2) ).
fof(f5,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',associativity_of_join) ).
fof(f8,axiom,
! [X0] : complement(complement(X0)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',complement_involution) ).
fof(f9,axiom,
! [X0,X1] : join(X0,join(X1,complement(X1))) = join(X1,complement(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',join_complement) ).
fof(f10,plain,
! [X0,X1] : join(X1,complement(X1)) = join(X0,join(X1,complement(X1))),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/LAT003-0.ax',meet_complement) ).
fof(f12,negated_conjecture,
join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b)))))) != n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_e2) ).
fof(f13,plain,
n1 != join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b)))))),
inference(reorient_equations,[],[f12]) ).
fof(f15,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(definition_unfolding,[],[f3,f11]) ).
fof(f18,plain,
n1 != join(a,join(complement(join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))),
inference(definition_unfolding,[],[f13,f11,f11,f11,f11,f11]) ).
tcf(c_60,plain,
! [X0: $i] : join(complement(X0),X0) = n1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(cnf_transformation,[],[f15]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_67,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(cnf_transformation,[],[f8]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X1))) = join(X1,complement(X1)),
inference(cnf_transformation,[],[f10]) ).
tcf(c_69,negated_conjecture,
join(a,join(complement(join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(cnf_transformation,[],[f18]) ).
tcf(c_103,definition,
iPr_def_10 = complement(a),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_104,definition,
iPr_def_11 = complement(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_105,definition,
iPr_def_12 = complement(b),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_106,definition,
iPr_def_13 = join(a,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_107,definition,
iPr_def_14 = complement(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_108,definition,
iPr_def_15 = join(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_109,definition,
iPr_def_16 = complement(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_110,definition,
iPr_def_17 = join(iPr_def_14,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_111,definition,
iPr_def_18 = complement(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_112,definition,
iPr_def_19 = complement(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_113,definition,
iPr_def_20 = join(iPr_def_11,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_114,definition,
iPr_def_21 = complement(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_115,definition,
iPr_def_22 = join(iPr_def_11,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_116,definition,
iPr_def_23 = complement(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_117,definition,
iPr_def_24 = complement(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_118,definition,
iPr_def_25 = join(iPr_def_11,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_119,definition,
iPr_def_26 = complement(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_120,definition,
iPr_def_27 = join(iPr_def_23,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_121,definition,
iPr_def_28 = complement(iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_122,definition,
iPr_def_29 = join(iPr_def_11,iPr_def_28),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_123,definition,
iPr_def_30 = complement(iPr_def_29),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_124,definition,
iPr_def_31 = join(iPr_def_21,iPr_def_30),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_125,definition,
iPr_def_32 = join(a,iPr_def_31),
introduced(definition,[new_symbols(definition,[iPr_def_32])],[]) ).
tcf(c_126,negated_conjecture,
iPr_def_32 != n1,
inference(demodulation,[status(thm)],[c_69,c_117,c_118,c_119,c_115,c_116,c_120,c_121,c_122,c_123,c_108,c_109,c_105,c_106,c_107,c_110,c_111,c_112,c_103,c_104,c_113,c_114,c_124,c_125]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X1))) = join(X1,complement(X1)),
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_132,plain,
! [X0: $i] : complement(complement(X0)) = X0,
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_135,plain,
! [X0: $i] : join(complement(X0),X0) = n1,
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_226,plain,
join(iPr_def_12,a) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_106,c_133,c_134]) ).
tcf(c_227,plain,
join(iPr_def_16,iPr_def_14) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_110,c_133,c_134]) ).
tcf(c_228,plain,
join(iPr_def_19,iPr_def_11) = iPr_def_20,
inference(theory_normalisation,[status(thm)],[c_113,c_133,c_134]) ).
tcf(c_229,plain,
join(iPr_def_24,iPr_def_11) = iPr_def_25,
inference(theory_normalisation,[status(thm)],[c_118,c_133,c_134]) ).
tcf(c_230,plain,
join(iPr_def_26,iPr_def_23) = iPr_def_27,
inference(theory_normalisation,[status(thm)],[c_120,c_133,c_134]) ).
tcf(c_231,plain,
join(iPr_def_28,iPr_def_11) = iPr_def_29,
inference(theory_normalisation,[status(thm)],[c_122,c_133,c_134]) ).
tcf(c_232,plain,
join(iPr_def_31,a) = iPr_def_32,
inference(theory_normalisation,[status(thm)],[c_125,c_133,c_134]) ).
tcf(c_233,plain,
! [X0: $i] : join(X0,complement(X0)) = n1,
inference(theory_normalisation,[status(thm)],[c_135,c_133,c_134]) ).
tcf(c_235,plain,
! [X0: $i] : join(X0,n1) = n1,
inference(demodulation,[status(thm)],[c_131,c_233]) ).
tcf(c_236,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,X2)) = join(X1,join(X0,X2)),
inference(superposition,[status(thm)],[c_133,c_134]) ).
tcf(c_251,plain,
complement(iPr_def_10) = a,
inference(superposition,[status(thm)],[c_103,c_132]) ).
tcf(c_252,plain,
complement(iPr_def_12) = b,
inference(superposition,[status(thm)],[c_105,c_132]) ).
tcf(c_253,plain,
complement(iPr_def_11) = iPr_def_10,
inference(superposition,[status(thm)],[c_104,c_132]) ).
tcf(c_255,plain,
complement(iPr_def_16) = iPr_def_15,
inference(superposition,[status(thm)],[c_109,c_132]) ).
tcf(c_256,plain,
complement(iPr_def_18) = iPr_def_17,
inference(superposition,[status(thm)],[c_111,c_132]) ).
tcf(c_257,plain,
complement(iPr_def_19) = iPr_def_18,
inference(superposition,[status(thm)],[c_112,c_132]) ).
tcf(c_259,plain,
complement(iPr_def_23) = iPr_def_22,
inference(superposition,[status(thm)],[c_116,c_132]) ).
tcf(c_261,plain,
complement(iPr_def_26) = iPr_def_25,
inference(superposition,[status(thm)],[c_119,c_132]) ).
tcf(c_263,plain,
complement(iPr_def_30) = iPr_def_29,
inference(superposition,[status(thm)],[c_123,c_132]) ).
tcf(c_291,plain,
! [X0: $i] : join(iPr_def_10,complement(join(iPr_def_11,complement(X0)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_104,c_129]) ).
tcf(c_295,plain,
! [X0: $i] : join(iPr_def_18,complement(join(iPr_def_19,complement(X0)))) = iPr_def_18,
inference(superposition,[status(thm)],[c_112,c_129]) ).
tcf(c_296,plain,
! [X0: $i] : join(iPr_def_20,complement(join(iPr_def_21,complement(X0)))) = iPr_def_20,
inference(superposition,[status(thm)],[c_114,c_129]) ).
tcf(c_318,plain,
! [X0: $i] : join(X0,complement(complement(X0))) = X0,
inference(superposition,[status(thm)],[c_129,c_129]) ).
tcf(c_339,plain,
! [X0: $i] : join(iPr_def_21,join(iPr_def_30,X0)) = join(iPr_def_31,X0),
inference(superposition,[status(thm)],[c_124,c_133]) ).
tcf(c_341,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_14,X0)) = join(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_227,c_133]) ).
tcf(c_346,plain,
! [X0: $i] : join(iPr_def_31,join(a,X0)) = join(iPr_def_32,X0),
inference(superposition,[status(thm)],[c_232,c_133]) ).
tcf(c_369,plain,
! [X0: $i] : join(iPr_def_12,join(X0,a)) = join(X0,iPr_def_13),
inference(superposition,[status(thm)],[c_226,c_236]) ).
tcf(c_371,plain,
! [X0: $i] : join(iPr_def_19,join(X0,iPr_def_11)) = join(X0,iPr_def_20),
inference(superposition,[status(thm)],[c_228,c_236]) ).
tcf(c_375,plain,
! [X0: $i] : join(iPr_def_31,join(X0,a)) = join(X0,iPr_def_32),
inference(superposition,[status(thm)],[c_232,c_236]) ).
tcf(c_376,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X0))) = join(X1,n1),
inference(superposition,[status(thm)],[c_233,c_236]) ).
tcf(c_451,plain,
iPr_def_17 = iPr_def_19,
inference(demodulation,[status(thm)],[c_256,c_112]) ).
tcf(c_452,plain,
b = iPr_def_24,
inference(demodulation,[status(thm)],[c_252,c_117]) ).
tcf(c_453,plain,
a = iPr_def_11,
inference(demodulation,[status(thm)],[c_251,c_104]) ).
tcf(c_463,plain,
! [X0: $i] : join(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_318,c_132]) ).
tcf(c_464,plain,
! [X0: $i] : join(iPr_def_31,join(X0,iPr_def_11)) = join(X0,iPr_def_32),
inference(demodulation,[status(thm)],[c_375,c_453]) ).
tcf(c_466,plain,
! [X0: $i] : join(iPr_def_12,join(X0,iPr_def_11)) = join(X0,iPr_def_13),
inference(demodulation,[status(thm)],[c_369,c_453]) ).
tcf(c_467,plain,
! [X0: $i] : join(iPr_def_11,join(X0,iPr_def_12)) = join(X0,iPr_def_13),
inference(theory_normalisation,[status(thm)],[c_466,c_133,c_134]) ).
tcf(c_468,plain,
! [X0: $i] : join(X0,iPr_def_13) = join(X0,iPr_def_22),
inference(ac_demodulation,[status(thm)],[c_467,c_115,c_133,c_134]) ).
tcf(c_476,plain,
! [X0: $i] : join(iPr_def_31,join(iPr_def_11,X0)) = join(iPr_def_32,X0),
inference(demodulation,[status(thm)],[c_346,c_453]) ).
tcf(c_477,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_14,X0)) = join(iPr_def_19,X0),
inference(demodulation,[status(thm)],[c_341,c_451]) ).
tcf(c_498,plain,
! [X0: $i,X1: $i] : join(X0,join(X1,complement(X0))) = n1,
inference(demodulation,[status(thm)],[c_376,c_235]) ).
tcf(c_634,plain,
join(iPr_def_31,iPr_def_11) = iPr_def_32,
inference(superposition,[status(thm)],[c_453,c_232]) ).
tcf(c_635,plain,
join(iPr_def_12,iPr_def_11) = iPr_def_13,
inference(superposition,[status(thm)],[c_453,c_226]) ).
tcf(c_636,plain,
join(iPr_def_11,b) = iPr_def_15,
inference(superposition,[status(thm)],[c_453,c_108]) ).
tcf(c_639,plain,
complement(iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_253,c_132]) ).
tcf(c_643,plain,
complement(iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_255,c_132]) ).
tcf(c_649,plain,
complement(iPr_def_22) = iPr_def_23,
inference(superposition,[status(thm)],[c_259,c_132]) ).
tcf(c_653,plain,
complement(iPr_def_25) = iPr_def_26,
inference(superposition,[status(thm)],[c_261,c_132]) ).
tcf(c_657,plain,
complement(iPr_def_29) = iPr_def_30,
inference(superposition,[status(thm)],[c_263,c_132]) ).
tcf(c_733,plain,
join(iPr_def_13,iPr_def_22) = iPr_def_13,
inference(superposition,[status(thm)],[c_468,c_463]) ).
tcf(c_879,plain,
! [X0: $i] : join(iPr_def_10,complement(join(iPr_def_11,X0))) = iPr_def_10,
inference(superposition,[status(thm)],[c_132,c_291]) ).
tcf(c_887,plain,
join(iPr_def_10,complement(join(iPr_def_11,iPr_def_24))) = iPr_def_10,
inference(superposition,[status(thm)],[c_117,c_291]) ).
tcf(c_1050,plain,
join(iPr_def_22,iPr_def_13) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_733,c_133,c_134]) ).
tcf(c_1051,plain,
iPr_def_13 = iPr_def_22,
inference(demodulation,[status(thm)],[c_1050,c_463,c_468]) ).
tcf(c_1059,plain,
iPr_def_15 = iPr_def_25,
inference(demodulation,[status(thm)],[c_636,c_134,c_229,c_452]) ).
tcf(c_1060,plain,
join(iPr_def_12,iPr_def_11) = iPr_def_22,
inference(demodulation,[status(thm)],[c_635,c_1051]) ).
tcf(c_1061,plain,
join(iPr_def_11,iPr_def_12) = iPr_def_22,
inference(theory_normalisation,[status(thm)],[c_1060,c_133,c_134]) ).
tcf(c_1152,plain,
join(iPr_def_10,complement(join(iPr_def_24,iPr_def_11))) = iPr_def_10,
inference(theory_normalisation,[status(thm)],[c_887,c_133,c_134]) ).
tcf(c_1153,plain,
join(iPr_def_26,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_1152,c_134,c_119,c_229]) ).
tcf(c_1539,plain,
complement(iPr_def_22) = iPr_def_14,
inference(superposition,[status(thm)],[c_1051,c_107]) ).
tcf(c_1565,plain,
iPr_def_16 = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_653,c_643,c_1059]) ).
tcf(c_1614,plain,
join(iPr_def_16,iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_1153,c_1565]) ).
tcf(c_2084,plain,
iPr_def_14 = iPr_def_23,
inference(superposition,[status(thm)],[c_1539,c_649]) ).
tcf(c_2146,plain,
join(iPr_def_10,complement(iPr_def_22)) = iPr_def_10,
inference(superposition,[status(thm)],[c_1061,c_879]) ).
tcf(c_2335,plain,
! [X0: $i] : join(iPr_def_18,complement(join(iPr_def_19,X0))) = iPr_def_18,
inference(superposition,[status(thm)],[c_132,c_295]) ).
tcf(c_2411,plain,
join(iPr_def_20,complement(join(iPr_def_21,iPr_def_30))) = iPr_def_20,
inference(superposition,[status(thm)],[c_657,c_296]) ).
tcf(c_2530,plain,
join(iPr_def_14,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_2146,c_134,c_1539]) ).
tcf(c_2593,plain,
join(iPr_def_20,complement(iPr_def_31)) = iPr_def_20,
inference(demodulation,[status(thm)],[c_2411,c_124]) ).
tcf(c_2929,plain,
join(iPr_def_26,iPr_def_14) = iPr_def_27,
inference(superposition,[status(thm)],[c_2084,c_230]) ).
tcf(c_3122,plain,
join(iPr_def_31,iPr_def_20) = n1,
inference(superposition,[status(thm)],[c_2593,c_498]) ).
tcf(c_3553,plain,
join(iPr_def_14,iPr_def_26) = iPr_def_27,
inference(theory_normalisation,[status(thm)],[c_2929,c_133,c_134]) ).
tcf(c_3554,plain,
iPr_def_19 = iPr_def_27,
inference(demodulation,[status(thm)],[c_3553,c_134,c_227,c_451,c_1565]) ).
tcf(c_3656,plain,
complement(iPr_def_19) = iPr_def_28,
inference(superposition,[status(thm)],[c_3554,c_121]) ).
tcf(c_4180,plain,
complement(iPr_def_28) = iPr_def_19,
inference(superposition,[status(thm)],[c_3656,c_132]) ).
tcf(c_4181,plain,
iPr_def_18 = iPr_def_28,
inference(superposition,[status(thm)],[c_3656,c_257]) ).
tcf(c_4614,plain,
join(iPr_def_21,iPr_def_30) = join(iPr_def_31,iPr_def_30),
inference(superposition,[status(thm)],[c_463,c_339]) ).
tcf(c_4710,plain,
join(iPr_def_31,iPr_def_30) = iPr_def_31,
inference(demodulation,[status(thm)],[c_4614,c_124]) ).
tcf(c_5064,plain,
join(iPr_def_19,iPr_def_32) = join(iPr_def_31,iPr_def_20),
inference(superposition,[status(thm)],[c_634,c_371]) ).
tcf(c_5200,plain,
join(iPr_def_31,iPr_def_20) = join(iPr_def_32,iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_5064,c_133,c_134]) ).
tcf(c_5201,plain,
join(iPr_def_32,iPr_def_19) = n1,
inference(demodulation,[status(thm)],[c_5200,c_3122]) ).
tcf(c_5759,plain,
! [X0: $i] : join(iPr_def_32,join(X0,iPr_def_19)) = join(X0,n1),
inference(superposition,[status(thm)],[c_5201,c_236]) ).
tcf(c_5784,plain,
join(iPr_def_31,iPr_def_11) = join(iPr_def_32,iPr_def_11),
inference(superposition,[status(thm)],[c_463,c_476]) ).
tcf(c_5812,plain,
join(iPr_def_16,iPr_def_10) = join(iPr_def_19,iPr_def_10),
inference(superposition,[status(thm)],[c_2530,c_477]) ).
tcf(c_5833,plain,
join(iPr_def_19,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_5812,c_1614]) ).
tcf(c_5840,plain,
join(iPr_def_32,iPr_def_11) = iPr_def_32,
inference(demodulation,[status(thm)],[c_5784,c_634]) ).
tcf(c_5871,plain,
! [X0: $i] : join(iPr_def_32,join(X0,iPr_def_19)) = n1,
inference(demodulation,[status(thm)],[c_5759,c_235]) ).
tcf(c_6328,plain,
join(iPr_def_18,complement(iPr_def_10)) = iPr_def_18,
inference(superposition,[status(thm)],[c_5833,c_2335]) ).
tcf(c_6415,plain,
join(iPr_def_31,iPr_def_32) = join(iPr_def_32,iPr_def_32),
inference(superposition,[status(thm)],[c_5840,c_464]) ).
tcf(c_6558,plain,
iPr_def_28 = iPr_def_29,
inference(demodulation,[status(thm)],[c_6328,c_231,c_639,c_4181]) ).
tcf(c_6563,plain,
join(iPr_def_32,iPr_def_31) = join(iPr_def_32,iPr_def_32),
inference(theory_normalisation,[status(thm)],[c_6415,c_133,c_134]) ).
tcf(c_6564,plain,
join(iPr_def_32,iPr_def_31) = iPr_def_32,
inference(demodulation,[status(thm)],[c_6563,c_463]) ).
tcf(c_6785,plain,
complement(iPr_def_28) = iPr_def_30,
inference(superposition,[status(thm)],[c_6558,c_123]) ).
tcf(c_7104,plain,
iPr_def_19 = iPr_def_30,
inference(demodulation,[status(thm)],[c_6785,c_4180]) ).
tcf(c_7180,plain,
join(iPr_def_31,iPr_def_19) = iPr_def_31,
inference(superposition,[status(thm)],[c_7104,c_4710]) ).
tcf(c_8044,plain,
join(iPr_def_32,iPr_def_31) = n1,
inference(superposition,[status(thm)],[c_7180,c_5871]) ).
tcf(c_8297,plain,
n1 = iPr_def_32,
inference(demodulation,[status(thm)],[c_8044,c_6564]) ).
tcf(c_8511,plain,
$false,
inference(superposition,[status(thm)],[c_8297,c_126]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/5.37 % Computer : n003.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Wed Sep 23 20:03:29 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/5.41 Running UEQ theorem proving
% 0.12/5.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.42
% 0.12/5.42 % ======== iProver multi-core TPTP/SMT =========
% 0.12/5.42
% 0.12/5.42 % Detected problem language: tptp
% 0.12/5.43 % Proving...
% 6.80/6.68 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 6.80/6.68 % SZS status Started for theBenchmark.p
% 6.80/6.68 % SZS status Unsatisfiable for theBenchmark.p
% 6.80/6.68
% 6.80/6.68 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.80/6.68
% 6.80/6.68 % ------ iProver source info
% 6.80/6.68
% 6.80/6.68 % git: date: 2026-07-19 20:42:38 +0200
% 6.80/6.68 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.80/6.68 % git: non_committed_changes: false
% 6.80/6.68
% 6.80/6.68 % ------ Parsing...% successful
% 6.80/6.68
% 6.80/6.68
% 6.80/6.68 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.80/6.68
% 6.80/6.68 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.80/6.68
% 6.80/6.68 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.80/6.68
% 6.80/6.68 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.80/6.68 % ------ Proving...
% 6.80/6.68 % ------ Problem Properties
% 6.80/6.68
% 6.80/6.68 %
% 6.80/6.68 % clauses 33
% 6.80/6.68 % conjectures 1
% 6.80/6.68 % EPR 1
% 6.80/6.68 % Horn 33
% 6.80/6.68 % unary 33
% 6.80/6.68 % binary 0
% 6.80/6.68 % lits 33
% 6.80/6.68 % lits eq 33
% 6.80/6.68 % fd_pure 0
% 6.80/6.68 % fd_pseudo 0
% 6.80/6.68 % fd_cond 0
% 6.80/6.68 % fd_pseudo_cond 0
% 6.80/6.68 % AC symbols 1
% 6.80/6.68
% 6.80/6.68 % ------ Input Options Time Limit: Unbounded
% 6.80/6.68
% 6.80/6.68
% 6.80/6.68 % ------
% 6.80/6.68 % Current options:
% 6.80/6.68 % ------
% 6.80/6.68
% 6.80/6.68
% 6.80/6.68 %
% 6.80/6.68
% 6.80/6.68 % ------ Proving...
% 6.80/6.68 %
% 6.80/6.68
% 6.80/6.68 % SZS status Unsatisfiable for theBenchmark.p
% 6.80/6.68
% 6.80/6.68 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.80/6.69
% 6.80/6.69
%------------------------------------------------------------------------------