%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% 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:10:03 PM UTC 2026
% Result : Theorem 118.64s 17.01s
% Output : CNFRefutation 118.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 34
% Syntax : Number of formulae : 154 ( 93 unt; 0 def)
% Number of atoms : 273 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 233 ( 114 ~; 110 |; 4 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 68 ( 0 sgn 68 !; 0 ?; 32 :)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_6) ).
fof(f21,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_21) ).
fof(f26,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_26) ).
fof(f28,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_28) ).
fof(f30,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_30) ).
fof(f74,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_74) ).
fof(f145,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_145) ).
fof(f152,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_152) ).
fof(f168,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_168) ).
fof(f189,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_189) ).
fof(f193,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_193) ).
fof(f199,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_199) ).
fof(f224,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_224) ).
fof(f230,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_230) ).
fof(f280,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_280) ).
fof(f285,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_285) ).
fof(f305,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_305) ).
fof(f311,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_311) ).
fof(f335,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_335) ).
fof(f348,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_348) ).
fof(f385,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_385) ).
fof(f395,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_395) ).
fof(f397,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_397) ).
fof(f403,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_403) ).
fof(f405,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_405) ).
fof(f436,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_436) ).
fof(f442,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_442) ).
fof(f449,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_449) ).
fof(f456,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_456) ).
fof(f491,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_491) ).
fof(f1112,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& genls(X0,X1) )
=> genls(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_1112) ).
fof(f1121,axiom,
! [X0,X1,X2] :
( ( genls(X2,X1)
& disjointwith(X0,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_1121) ).
fof(f1122,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& disjointwith(X0,X1) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+1.ax',ax1_1122) ).
fof(f1132,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query86) ).
fof(f1133,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1997,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ genls(X0,X1)
| genls(X2,X1) ),
inference(ennf_transformation,[],[f1112]) ).
fof(f1998,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ genls(X0,X1)
| genls(X2,X1) ),
inference(flattening,[],[f1997]) ).
fof(f2008,plain,
! [X0,X1,X2] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(ennf_transformation,[],[f1121]) ).
fof(f2009,plain,
! [X0,X1,X2] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(flattening,[],[f2008]) ).
fof(f2010,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(ennf_transformation,[],[f1122]) ).
fof(f2011,plain,
! [X0,X1,X2] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(flattening,[],[f2010]) ).
fof(f2022,plain,
( mtvisible(c_tptp_member974_mt)
& ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(ennf_transformation,[],[f1133]) ).
fof(f2028,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[],[f6]) ).
fof(f2043,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[],[f21]) ).
fof(f2048,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[],[f26]) ).
fof(f2050,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[],[f28]) ).
fof(f2052,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[],[f30]) ).
fof(f2095,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[],[f74]) ).
fof(f2166,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f145]) ).
fof(f2173,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f152]) ).
fof(f2189,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[],[f168]) ).
fof(f2210,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[],[f189]) ).
fof(f2214,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[],[f193]) ).
fof(f2220,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[],[f199]) ).
fof(f2245,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[],[f224]) ).
fof(f2251,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[],[f230]) ).
fof(f2301,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[],[f280]) ).
fof(f2306,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f285]) ).
fof(f2325,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[],[f305]) ).
fof(f2331,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f311]) ).
fof(f2355,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[],[f335]) ).
fof(f2368,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f348]) ).
fof(f2405,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f385]) ).
fof(f2415,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[],[f395]) ).
fof(f2417,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[],[f397]) ).
fof(f2423,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[],[f403]) ).
fof(f2425,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[],[f405]) ).
fof(f2456,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[],[f436]) ).
fof(f2462,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[],[f442]) ).
fof(f2469,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[],[f449]) ).
fof(f2476,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[],[f456]) ).
fof(f2511,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[],[f491]) ).
fof(f3042,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ genls(X0,X1)
| genls(X2,X1) ),
inference(cnf_transformation,[],[f1998]) ).
fof(f3051,plain,
! [X2,X0,X1] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(cnf_transformation,[],[f2009]) ).
fof(f3052,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(cnf_transformation,[],[f2011]) ).
fof(f3063,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[],[f2022]) ).
tcf(c_54,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[],[f2028]) ).
tcf(c_69,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[],[f2043]) ).
tcf(c_74,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[],[f2048]) ).
tcf(c_76,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[],[f2050]) ).
tcf(c_78,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[],[f2052]) ).
tcf(c_121,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[],[f2095]) ).
tcf(c_192,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f2166]) ).
tcf(c_199,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f2173]) ).
tcf(c_215,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[],[f2189]) ).
tcf(c_236,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[],[f2210]) ).
tcf(c_240,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[],[f2214]) ).
tcf(c_246,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[],[f2220]) ).
tcf(c_271,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[],[f2245]) ).
tcf(c_277,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[],[f2251]) ).
tcf(c_327,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[],[f2301]) ).
tcf(c_332,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f2306]) ).
tcf(c_351,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[],[f2325]) ).
tcf(c_357,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f2331]) ).
tcf(c_381,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[],[f2355]) ).
tcf(c_394,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f2368]) ).
tcf(c_431,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f2405]) ).
tcf(c_441,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[],[f2415]) ).
tcf(c_443,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[],[f2417]) ).
tcf(c_449,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[],[f2423]) ).
tcf(c_451,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[],[f2425]) ).
tcf(c_482,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[],[f2456]) ).
tcf(c_488,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[],[f2462]) ).
tcf(c_495,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[],[f2469]) ).
tcf(c_502,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[],[f2476]) ).
tcf(c_537,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[],[f2511]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i,X2: $i] :
( genls(X2,X1)
| ~ genls(X2,X0)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[],[f3042]) ).
tcf(c_1077,plain,
! [X0: $i,X1: $i,X2: $i] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[],[f3051]) ).
tcf(c_1078,plain,
! [X0: $i,X1: $i,X2: $i] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[],[f3052]) ).
tcf(c_1088,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[],[f3063]) ).
tcf(c_32828,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1,X2_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( disjointwith(X2_iProver_partiallytangible_1,X1_iProver_partiallytangible_1)
| ~ genls(X2_iProver_partiallytangible_1,X0_iProver_partiallytangible_1)
| ~ disjointwith(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(subtyping,[status(esa)],[c_1078]) ).
tcf(c_32829,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1,X2_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( disjointwith(X0_iProver_partiallytangible_1,X2_iProver_partiallytangible_1)
| ~ genls(X2_iProver_partiallytangible_1,X1_iProver_partiallytangible_1)
| ~ disjointwith(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(subtyping,[status(esa)],[c_1077]) ).
tcf(c_32834,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1,X2_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(X0_iProver_partiallytangible_1,X2_iProver_partiallytangible_1)
| ~ genls(X1_iProver_partiallytangible_1,X2_iProver_partiallytangible_1)
| ~ genls(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(subtyping,[status(esa)],[c_1068]) ).
tcf(c_33321,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( disjointwith(c_tptpcol_15_22076,X1_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_15_22076,X0_iProver_partiallytangible_1)
| ~ disjointwith(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32828]) ).
tcf(c_33323,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( disjointwith(c_tptpcol_15_22076,X0_iProver_partiallytangible_1)
| ~ disjointwith(c_tptpcol_15_22076,X1_iProver_partiallytangible_1)
| ~ genls(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32829]) ).
tcf(c_33492,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536)
| ~ genls(c_tptpcol_15_22076,c_tptpcol_1_1)
| ~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
inference(instantiation,[status(thm)],[c_33321]) ).
tcf(c_33497,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_10_72710)
| ~ genls(c_tptpcol_10_72710,c_tptpcol_9_72709)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_9_72709) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33503,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_14_72792)
| ~ genls(c_tptpcol_14_72792,c_tptpcol_13_72791)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_13_72791) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33518,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_8_72708)
| ~ genls(c_tptpcol_8_72708,c_tptpcol_7_72707)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33551,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_9_72709)
| ~ genls(c_tptpcol_9_72709,c_tptpcol_8_72708)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_8_72708) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33558,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_5_69635)
| ~ genls(c_tptpcol_5_69635,c_tptpcol_4_65539)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_4_65539) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33573,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793)
| ~ genls(c_tptpcol_15_72793,c_tptpcol_14_72792)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_14_72792) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33580,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_3_65538)
| ~ genls(c_tptpcol_3_65538,c_tptpcol_2_65537)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_2_65537) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33590,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_2_65537)
| ~ genls(c_tptpcol_2_65537,c_tptpcol_1_65536)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33607,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_12_72775)
| ~ genls(c_tptpcol_12_72775,c_tptpcol_11_72774)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_11_72774) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33608,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707)
| ~ genls(c_tptpcol_7_72707,c_tptpcol_6_71683)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_6_71683) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33611,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
| ~ genls(c_tptpcol_16_72795,c_tptpcol_15_72793)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33612,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_6_71683)
| ~ genls(c_tptpcol_6_71683,c_tptpcol_5_69635)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_5_69635) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33620,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_4_65539)
| ~ genls(c_tptpcol_4_65539,c_tptpcol_3_65538)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_3_65538) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33624,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_11_72774)
| ~ genls(c_tptpcol_11_72774,c_tptpcol_10_72710)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_10_72710) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_33636,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_13_72791)
| ~ genls(c_tptpcol_13_72791,c_tptpcol_12_72775)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_12_72775) ),
inference(instantiation,[status(thm)],[c_33323]) ).
tcf(c_34546,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_9_22021,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_9_22021,c_tptpcol_8_22020)
| ~ genls(c_tptpcol_8_22020,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_34552,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_5_20483,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_5_20483,c_tptpcol_4_16387)
| ~ genls(c_tptpcol_4_16387,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_34554,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_11_22023,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_11_22023,c_tptpcol_10_22022)
| ~ genls(c_tptpcol_10_22022,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_34638,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_14_22072,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_13_22071)
| ~ genls(c_tptpcol_13_22071,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_34662,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_13_22071,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_13_22071,c_tptpcol_12_22055)
| ~ genls(c_tptpcol_12_22055,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_34748,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_3_16386,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_3_16386,c_tptpcol_2_2)
| ~ genls(c_tptpcol_2_2,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_34792,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_7_21508,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_7_21508,c_tptpcol_6_20484)
| ~ genls(c_tptpcol_6_20484,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_36881,plain,
( genls(c_tptpcol_9_22021,c_tptpcol_7_21508)
| ~ genls(c_tptpcol_8_22020,c_tptpcol_7_21508)
| ~ genls(c_tptpcol_9_22021,c_tptpcol_8_22020) ),
inference(instantiation,[status(thm)],[c_34546]) ).
tcf(c_36884,plain,
( genls(c_tptpcol_5_20483,c_tptpcol_3_16386)
| ~ genls(c_tptpcol_5_20483,c_tptpcol_4_16387)
| ~ genls(c_tptpcol_4_16387,c_tptpcol_3_16386) ),
inference(instantiation,[status(thm)],[c_34552]) ).
tcf(c_36885,plain,
( genls(c_tptpcol_11_22023,c_tptpcol_9_22021)
| ~ genls(c_tptpcol_10_22022,c_tptpcol_9_22021)
| ~ genls(c_tptpcol_11_22023,c_tptpcol_10_22022) ),
inference(instantiation,[status(thm)],[c_34554]) ).
tcf(c_36935,plain,
( genls(c_tptpcol_13_22071,c_tptpcol_11_22023)
| ~ genls(c_tptpcol_13_22071,c_tptpcol_12_22055)
| ~ genls(c_tptpcol_12_22055,c_tptpcol_11_22023) ),
inference(instantiation,[status(thm)],[c_34662]) ).
tcf(c_36970,plain,
( genls(c_tptpcol_3_16386,c_tptpcol_1_1)
| ~ genls(c_tptpcol_3_16386,c_tptpcol_2_2)
| ~ genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
inference(instantiation,[status(thm)],[c_34748]) ).
tcf(c_36992,plain,
( genls(c_tptpcol_7_21508,c_tptpcol_5_20483)
| ~ genls(c_tptpcol_6_20484,c_tptpcol_5_20483)
| ~ genls(c_tptpcol_7_21508,c_tptpcol_6_20484) ),
inference(instantiation,[status(thm)],[c_34792]) ).
tcf(c_63472,plain,
( genls(c_tptpcol_14_22072,c_tptpcol_11_22023)
| ~ genls(c_tptpcol_13_22071,c_tptpcol_11_22023)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_13_22071) ),
inference(instantiation,[status(thm)],[c_34638]) ).
tcf(c_66420,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_15_22076,X0_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_15_22076,c_tptpcol_14_22072)
| ~ genls(c_tptpcol_14_22072,X0_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_66776,plain,
! [X0_iProver_partiallytangible_1: iProver_partiallytangible_1,X1_iProver_partiallytangible_1: iProver_partiallytangible_1] :
( genls(c_tptpcol_14_22072,X1_iProver_partiallytangible_1)
| ~ genls(c_tptpcol_14_22072,X0_iProver_partiallytangible_1)
| ~ genls(X0_iProver_partiallytangible_1,X1_iProver_partiallytangible_1) ),
inference(instantiation,[status(thm)],[c_32834]) ).
tcf(c_66962,plain,
( genls(c_tptpcol_15_22076,c_tptpcol_1_1)
| ~ genls(c_tptpcol_15_22076,c_tptpcol_14_22072)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_1_1) ),
inference(instantiation,[status(thm)],[c_66420]) ).
tcf(c_74170,plain,
( genls(c_tptpcol_14_22072,c_tptpcol_7_21508)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_9_22021)
| ~ genls(c_tptpcol_9_22021,c_tptpcol_7_21508) ),
inference(instantiation,[status(thm)],[c_66776]) ).
tcf(c_74173,plain,
( genls(c_tptpcol_14_22072,c_tptpcol_3_16386)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_5_20483)
| ~ genls(c_tptpcol_5_20483,c_tptpcol_3_16386) ),
inference(instantiation,[status(thm)],[c_66776]) ).
tcf(c_74174,plain,
( genls(c_tptpcol_14_22072,c_tptpcol_9_22021)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_11_22023)
| ~ genls(c_tptpcol_11_22023,c_tptpcol_9_22021) ),
inference(instantiation,[status(thm)],[c_66776]) ).
tcf(c_74259,plain,
( genls(c_tptpcol_14_22072,c_tptpcol_1_1)
| ~ genls(c_tptpcol_3_16386,c_tptpcol_1_1)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_3_16386) ),
inference(instantiation,[status(thm)],[c_66776]) ).
tcf(c_74279,plain,
( genls(c_tptpcol_14_22072,c_tptpcol_5_20483)
| ~ genls(c_tptpcol_7_21508,c_tptpcol_5_20483)
| ~ genls(c_tptpcol_14_22072,c_tptpcol_7_21508) ),
inference(instantiation,[status(thm)],[c_66776]) ).
tcf(c_74280,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_74279,c_74259,c_74174,c_74173,c_74170,c_66962,c_63472,c_36992,c_36970,c_36935,c_36885,c_36884,c_36881,c_33636,c_33624,c_33620,c_33612,c_33611,c_33608,c_33607,c_33590,c_33580,c_33573,c_33558,c_33551,c_33518,c_33503,c_33497,c_33492,c_1088,c_54,c_69,c_74,c_76,c_78,c_121,c_192,c_199,c_215,c_236,c_240,c_246,c_271,c_277,c_327,c_332,c_351,c_357,c_381,c_394,c_431,c_441,c_443,c_449,c_451,c_482,c_488,c_495,c_502,c_537]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 08:21:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 118.64/17.01 % SZS status Started for theBenchmark.p
% 118.64/17.01 % SZS status Theorem for theBenchmark.p
% 118.64/17.01
% 118.64/17.01 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 118.64/17.01
% 118.64/17.01 % ------ iProver source info
% 118.64/17.01
% 118.64/17.01 % git: date: 2026-07-19 20:42:38 +0200
% 118.64/17.01 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 118.64/17.01 % git: non_committed_changes: false
% 118.64/17.01
% 118.64/17.01 % ------ Parsing...
% 118.64/17.01 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 118.64/17.01
% 118.64/17.01 % ------ Preprocessing... sf_s rm: 30 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe:64:0s pe:128:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 118.64/17.01
% 118.64/17.01 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 118.64/17.01 % ------ Proving...
% 118.64/17.01 % ------ Problem Properties
% 118.64/17.01
% 118.64/17.01 %
% 118.64/17.01 % clauses 770
% 118.64/17.01 % conjectures 2
% 118.64/17.01 % EPR 722
% 118.64/17.01 % Horn 770
% 118.64/17.01 % unary 273
% 118.64/17.01 % binary 461
% 118.64/17.01 % lits 1303
% 118.64/17.01 % lits eq 0
% 118.64/17.01 % fd_pure 0
% 118.64/17.01 % fd_pseudo 0
% 118.64/17.01 % fd_cond 0
% 118.64/17.01 % fd_pseudo_cond 0
% 118.64/17.01 % AC symbols 0
% 118.64/17.01
% 118.64/17.01 % ------ Input Options Time Limit: Unbounded
% 118.64/17.01
% 118.64/17.01
% 118.64/17.01 % ------
% 118.64/17.01 % Current options:
% 118.64/17.01 % ------
% 118.64/17.01
% 118.64/17.01
% 118.64/17.01 %
% 118.64/17.01
% 118.64/17.01 % ------ Proving...
% 118.64/17.01 %
% 118.64/17.01
% 118.64/17.01 % SZS status Theorem for theBenchmark.p
% 118.64/17.01
% 118.64/17.01 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 118.64/17.01
% 118.64/17.01
%------------------------------------------------------------------------------