%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Thu Sep 24 08:19:14 AM UTC 2026
% Result : Theorem 1.96s 2.27s
% Output : Proof 1.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 35
% Syntax : Number of formulae : 229 ( 181 unt; 0 def)
% Number of atoms : 322 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 179 ( 86 ~; 82 |; 6 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 48 ( 0 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just6,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('theBenchmark.p',just6) ).
fof(just8,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('theBenchmark.p',just8) ).
fof(just10,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('theBenchmark.p',just10) ).
fof(just12,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('theBenchmark.p',just12) ).
fof(just14,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('theBenchmark.p',just14) ).
fof(just16,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('theBenchmark.p',just16) ).
fof(just18,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('theBenchmark.p',just18) ).
fof(just20,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('theBenchmark.p',just20) ).
fof(just22,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('theBenchmark.p',just22) ).
fof(just24,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('theBenchmark.p',just24) ).
fof(just26,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('theBenchmark.p',just26) ).
fof(just28,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('theBenchmark.p',just28) ).
fof(just30,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('theBenchmark.p',just30) ).
fof(just32,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('theBenchmark.p',just32) ).
fof(just34,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('theBenchmark.p',just34) ).
fof(just36,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('theBenchmark.p',just36) ).
fof(just38,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('theBenchmark.p',just38) ).
fof(just40,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('theBenchmark.p',just40) ).
fof(just42,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('theBenchmark.p',just42) ).
fof(just44,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('theBenchmark.p',just44) ).
fof(just46,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('theBenchmark.p',just46) ).
fof(just48,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('theBenchmark.p',just48) ).
fof(just50,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('theBenchmark.p',just50) ).
fof(just52,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('theBenchmark.p',just52) ).
fof(just54,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('theBenchmark.p',just54) ).
fof(just56,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('theBenchmark.p',just56) ).
fof(just58,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('theBenchmark.p',just58) ).
fof(just60,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('theBenchmark.p',just60) ).
fof(just62,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('theBenchmark.p',just62) ).
fof(just64,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('theBenchmark.p',just64) ).
fof(just84,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('theBenchmark.p',just84) ).
fof(just85,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('theBenchmark.p',just85) ).
fof(just155,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& genls(OLD,ARG2) )
=> genls(NEW,ARG2) ),
file('theBenchmark.p',just155) ).
fof(just156,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('theBenchmark.p',just156) ).
fof(query36,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('theBenchmark.p',query36) ).
fof(f_6_1,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(fof_nnf,[status(thm)],[just6]) ).
cnf(f_6_2,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(clausify,[status(thm)],[f_6_1]) ).
fof(f_8_1,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(fof_nnf,[status(thm)],[just8]) ).
cnf(f_8_2,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(clausify,[status(thm)],[f_8_1]) ).
fof(f_10_1,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(fof_nnf,[status(thm)],[just10]) ).
cnf(f_10_2,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(clausify,[status(thm)],[f_10_1]) ).
fof(f_12_1,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(fof_nnf,[status(thm)],[just12]) ).
cnf(f_12_2,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(clausify,[status(thm)],[f_12_1]) ).
fof(f_14_1,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(fof_nnf,[status(thm)],[just14]) ).
cnf(f_14_2,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(clausify,[status(thm)],[f_14_1]) ).
fof(f_16_1,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(fof_nnf,[status(thm)],[just16]) ).
cnf(f_16_2,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(clausify,[status(thm)],[f_16_1]) ).
fof(f_18_1,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(fof_nnf,[status(thm)],[just18]) ).
cnf(f_18_2,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(clausify,[status(thm)],[f_18_1]) ).
fof(f_20_1,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(fof_nnf,[status(thm)],[just20]) ).
cnf(f_20_2,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(clausify,[status(thm)],[f_20_1]) ).
fof(f_22_1,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(fof_nnf,[status(thm)],[just22]) ).
cnf(f_22_2,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(clausify,[status(thm)],[f_22_1]) ).
fof(f_24_1,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(fof_nnf,[status(thm)],[just24]) ).
cnf(f_24_2,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_26_1,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(fof_nnf,[status(thm)],[just26]) ).
cnf(f_26_2,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(clausify,[status(thm)],[f_26_1]) ).
fof(f_28_1,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(fof_nnf,[status(thm)],[just28]) ).
cnf(f_28_2,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(clausify,[status(thm)],[f_28_1]) ).
fof(f_30_1,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(fof_nnf,[status(thm)],[just30]) ).
cnf(f_30_2,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(clausify,[status(thm)],[f_30_1]) ).
fof(f_32_1,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(fof_nnf,[status(thm)],[just32]) ).
cnf(f_32_2,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(clausify,[status(thm)],[f_32_1]) ).
fof(f_34_1,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(fof_nnf,[status(thm)],[just34]) ).
cnf(f_34_2,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_36_1,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(fof_nnf,[status(thm)],[just36]) ).
cnf(f_36_2,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(clausify,[status(thm)],[f_36_1]) ).
fof(f_38_1,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(fof_nnf,[status(thm)],[just38]) ).
cnf(f_38_2,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(clausify,[status(thm)],[f_38_1]) ).
fof(f_40_1,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(fof_nnf,[status(thm)],[just40]) ).
cnf(f_40_2,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(clausify,[status(thm)],[f_40_1]) ).
fof(f_42_1,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(fof_nnf,[status(thm)],[just42]) ).
cnf(f_42_2,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_44_1,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(fof_nnf,[status(thm)],[just44]) ).
cnf(f_44_2,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(clausify,[status(thm)],[f_44_1]) ).
fof(f_46_1,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(fof_nnf,[status(thm)],[just46]) ).
cnf(f_46_2,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(clausify,[status(thm)],[f_46_1]) ).
fof(f_48_1,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(fof_nnf,[status(thm)],[just48]) ).
cnf(f_48_2,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(clausify,[status(thm)],[f_48_1]) ).
fof(f_50_1,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(fof_nnf,[status(thm)],[just50]) ).
cnf(f_50_2,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(clausify,[status(thm)],[f_50_1]) ).
fof(f_52_1,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(fof_nnf,[status(thm)],[just52]) ).
cnf(f_52_2,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(clausify,[status(thm)],[f_52_1]) ).
fof(f_54_1,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(fof_nnf,[status(thm)],[just54]) ).
cnf(f_54_2,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(clausify,[status(thm)],[f_54_1]) ).
fof(f_56_1,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(fof_nnf,[status(thm)],[just56]) ).
cnf(f_56_2,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(clausify,[status(thm)],[f_56_1]) ).
fof(f_58_1,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(fof_nnf,[status(thm)],[just58]) ).
cnf(f_58_2,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(clausify,[status(thm)],[f_58_1]) ).
fof(f_60_1,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(fof_nnf,[status(thm)],[just60]) ).
cnf(f_60_2,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(clausify,[status(thm)],[f_60_1]) ).
fof(f_62_1,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(fof_nnf,[status(thm)],[just62]) ).
cnf(f_62_2,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(clausify,[status(thm)],[f_62_1]) ).
fof(f_64_1,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(fof_nnf,[status(thm)],[just64]) ).
cnf(f_64_2,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[f_64_1]) ).
fof(f_84_1,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(fof_nnf,[status(thm)],[just84]) ).
fof(f_84_2,plain,
! [U_67,U_66,U_65] :
( disjointwith(U_67,U_65)
| ~ genls(U_65,U_66)
| ~ disjointwith(U_67,U_66) ),
inference(variable_rename,[status(thm)],[f_84_1]) ).
cnf(f_84_3,plain,
( disjointwith(U_67,U_65)
| ~ genls(U_65,U_66)
| ~ disjointwith(U_67,U_66) ),
inference(clausify,[status(thm)],[f_84_2]) ).
fof(f_85_1,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(fof_nnf,[status(thm)],[just85]) ).
fof(f_85_2,plain,
! [U_70,U_69,U_68] :
( disjointwith(U_68,U_69)
| ~ genls(U_68,U_70)
| ~ disjointwith(U_70,U_69) ),
inference(variable_rename,[status(thm)],[f_85_1]) ).
cnf(f_85_3,plain,
( disjointwith(U_68,U_69)
| ~ genls(U_68,U_70)
| ~ disjointwith(U_70,U_69) ),
inference(clausify,[status(thm)],[f_85_2]) ).
fof(f_155_1,plain,
! [OLD,ARG2,NEW] :
( genls(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ genls(OLD,ARG2) ),
inference(fof_nnf,[status(thm)],[just155]) ).
fof(f_155_2,plain,
! [U_148,U_147,U_146] :
( genls(U_146,U_147)
| ~ genls(U_146,U_148)
| ~ genls(U_148,U_147) ),
inference(variable_rename,[status(thm)],[f_155_1]) ).
cnf(f_155_3,plain,
( genls(U_146,U_147)
| ~ genls(U_146,U_148)
| ~ genls(U_148,U_147) ),
inference(clausify,[status(thm)],[f_155_2]) ).
fof(f_156_1,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(fof_nnf,[status(thm)],[just156]) ).
fof(f_156_2,plain,
! [U_151,U_150,U_149] :
( genls(U_151,U_149)
| ~ genls(U_150,U_149)
| ~ genls(U_151,U_150) ),
inference(variable_rename,[status(thm)],[f_156_1]) ).
cnf(f_156_3,plain,
( genls(U_151,U_149)
| ~ genls(U_150,U_149)
| ~ genls(U_151,U_150) ),
inference(clausify,[status(thm)],[f_156_2]) ).
fof(f_174_1,negated_conjecture,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(negate,[status(cth)],[query36]) ).
fof(f_174_2,negated_conjecture,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(definitional_conversion,[status(esa)],[f_174_1]) ).
cnf(f_174_4,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(clausify,[status(thm)],[f_174_2]) ).
cnf(t1,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(start,[status(thm),parent(0:0)],[f_174_4]) ).
cnf(t2,plain,
( ~ genls(c_tptpcol_16_72795,c_tptpcol_1_65536)
| ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536)
| disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(extension,[status(thm),parent(t1:1)],[f_84_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ genls(c_tptpcol_15_22076,c_tptpcol_8_22020)
| ~ disjointwith(c_tptpcol_8_22020,c_tptpcol_1_65536)
| disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t2:2)],[f_85_3]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ genls(c_tptpcol_8_22020,c_tptpcol_4_16387)
| ~ disjointwith(c_tptpcol_4_16387,c_tptpcol_1_65536)
| disjointwith(c_tptpcol_8_22020,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t4:2)],[f_85_3]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ genls(c_tptpcol_4_16387,c_tptpcol_2_2)
| ~ disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)
| disjointwith(c_tptpcol_4_16387,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t6:2)],[f_85_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( ~ genls(c_tptpcol_2_2,c_tptpcol_1_1)
| ~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)
| disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t8:2)],[f_85_3]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(extension,[status(thm),parent(t10:2)],[f_64_2]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(extension,[status(thm),parent(t10:3)],[f_6_2]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t10:3]) ).
cnf(t16,plain,
( ~ genls(c_tptpcol_4_16387,c_tptpcol_3_16386)
| ~ genls(c_tptpcol_3_16386,c_tptpcol_2_2)
| genls(c_tptpcol_4_16387,c_tptpcol_2_2) ),
inference(extension,[status(thm),parent(t8:3)],[f_155_3]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t8:3]) ).
cnf(t18,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(extension,[status(thm),parent(t16:2)],[f_8_2]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t16:2]) ).
cnf(t20,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(extension,[status(thm),parent(t16:3)],[f_10_2]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t16:3]) ).
cnf(t22,plain,
( ~ genls(c_tptpcol_8_22020,c_tptpcol_6_20484)
| ~ genls(c_tptpcol_6_20484,c_tptpcol_4_16387)
| genls(c_tptpcol_8_22020,c_tptpcol_4_16387) ),
inference(extension,[status(thm),parent(t6:3)],[f_155_3]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t6:3]) ).
cnf(t24,plain,
( ~ genls(c_tptpcol_6_20484,c_tptpcol_5_20483)
| ~ genls(c_tptpcol_5_20483,c_tptpcol_4_16387)
| genls(c_tptpcol_6_20484,c_tptpcol_4_16387) ),
inference(extension,[status(thm),parent(t22:2)],[f_155_3]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(extension,[status(thm),parent(t24:2)],[f_12_2]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t24:2]) ).
cnf(t28,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(extension,[status(thm),parent(t24:3)],[f_14_2]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t24:3]) ).
cnf(t30,plain,
( ~ genls(c_tptpcol_8_22020,c_tptpcol_7_21508)
| ~ genls(c_tptpcol_7_21508,c_tptpcol_6_20484)
| genls(c_tptpcol_8_22020,c_tptpcol_6_20484) ),
inference(extension,[status(thm),parent(t22:3)],[f_155_3]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t22:3]) ).
cnf(t32,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(extension,[status(thm),parent(t30:2)],[f_16_2]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(extension,[status(thm),parent(t30:3)],[f_18_2]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t30:3]) ).
cnf(t36,plain,
( ~ genls(c_tptpcol_11_22023,c_tptpcol_8_22020)
| ~ genls(c_tptpcol_15_22076,c_tptpcol_11_22023)
| genls(c_tptpcol_15_22076,c_tptpcol_8_22020) ),
inference(extension,[status(thm),parent(t4:3)],[f_156_3]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t4:3]) ).
cnf(t38,plain,
( ~ genls(c_tptpcol_13_22071,c_tptpcol_11_22023)
| ~ genls(c_tptpcol_15_22076,c_tptpcol_13_22071)
| genls(c_tptpcol_15_22076,c_tptpcol_11_22023) ),
inference(extension,[status(thm),parent(t36:2)],[f_156_3]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t36:2]) ).
cnf(t40,plain,
( ~ genls(c_tptpcol_14_22072,c_tptpcol_13_22071)
| ~ genls(c_tptpcol_15_22076,c_tptpcol_14_22072)
| genls(c_tptpcol_15_22076,c_tptpcol_13_22071) ),
inference(extension,[status(thm),parent(t38:2)],[f_156_3]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t38:2]) ).
cnf(t42,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(extension,[status(thm),parent(t40:2)],[f_32_2]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
cnf(t44,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(extension,[status(thm),parent(t40:3)],[f_30_2]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t40:3]) ).
cnf(t46,plain,
( ~ genls(c_tptpcol_12_22055,c_tptpcol_11_22023)
| ~ genls(c_tptpcol_13_22071,c_tptpcol_12_22055)
| genls(c_tptpcol_13_22071,c_tptpcol_11_22023) ),
inference(extension,[status(thm),parent(t38:3)],[f_156_3]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t38:3]) ).
cnf(t48,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(extension,[status(thm),parent(t46:2)],[f_28_2]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t46:2]) ).
cnf(t50,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(extension,[status(thm),parent(t46:3)],[f_26_2]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t46:3]) ).
cnf(t52,plain,
( ~ genls(c_tptpcol_9_22021,c_tptpcol_8_22020)
| ~ genls(c_tptpcol_11_22023,c_tptpcol_9_22021)
| genls(c_tptpcol_11_22023,c_tptpcol_8_22020) ),
inference(extension,[status(thm),parent(t36:3)],[f_156_3]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t36:3]) ).
cnf(t54,plain,
( ~ genls(c_tptpcol_10_22022,c_tptpcol_9_22021)
| ~ genls(c_tptpcol_11_22023,c_tptpcol_10_22022)
| genls(c_tptpcol_11_22023,c_tptpcol_9_22021) ),
inference(extension,[status(thm),parent(t52:2)],[f_156_3]) ).
cnf(t55,plain,
$false,
inference(connection,[status(thm),parent(t54:1)],[t54:1,t52:2]) ).
cnf(t56,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(extension,[status(thm),parent(t54:2)],[f_24_2]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t54:2]) ).
cnf(t58,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(extension,[status(thm),parent(t54:3)],[f_22_2]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t54:3]) ).
cnf(t60,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(extension,[status(thm),parent(t52:3)],[f_20_2]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t52:3]) ).
cnf(t62,plain,
( ~ genls(c_tptpcol_8_72708,c_tptpcol_1_65536)
| ~ genls(c_tptpcol_16_72795,c_tptpcol_8_72708)
| genls(c_tptpcol_16_72795,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t2:3)],[f_156_3]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t2:3]) ).
cnf(t64,plain,
( ~ genls(c_tptpcol_12_72775,c_tptpcol_8_72708)
| ~ genls(c_tptpcol_16_72795,c_tptpcol_12_72775)
| genls(c_tptpcol_16_72795,c_tptpcol_8_72708) ),
inference(extension,[status(thm),parent(t62:2)],[f_156_3]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
( ~ genls(c_tptpcol_14_72792,c_tptpcol_12_72775)
| ~ genls(c_tptpcol_16_72795,c_tptpcol_14_72792)
| genls(c_tptpcol_16_72795,c_tptpcol_12_72775) ),
inference(extension,[status(thm),parent(t64:2)],[f_156_3]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t64:2]) ).
cnf(t68,plain,
( ~ genls(c_tptpcol_15_72793,c_tptpcol_14_72792)
| ~ genls(c_tptpcol_16_72795,c_tptpcol_15_72793)
| genls(c_tptpcol_16_72795,c_tptpcol_14_72792) ),
inference(extension,[status(thm),parent(t66:2)],[f_156_3]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t66:2]) ).
cnf(t70,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(extension,[status(thm),parent(t68:2)],[f_62_2]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t68:2]) ).
cnf(t72,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(extension,[status(thm),parent(t68:3)],[f_60_2]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t68:3]) ).
cnf(t74,plain,
( ~ genls(c_tptpcol_13_72791,c_tptpcol_12_72775)
| ~ genls(c_tptpcol_14_72792,c_tptpcol_13_72791)
| genls(c_tptpcol_14_72792,c_tptpcol_12_72775) ),
inference(extension,[status(thm),parent(t66:3)],[f_156_3]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t66:3]) ).
cnf(t76,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(extension,[status(thm),parent(t74:2)],[f_58_2]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(extension,[status(thm),parent(t74:3)],[f_56_2]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t74:3]) ).
cnf(t80,plain,
( ~ genls(c_tptpcol_10_72710,c_tptpcol_8_72708)
| ~ genls(c_tptpcol_12_72775,c_tptpcol_10_72710)
| genls(c_tptpcol_12_72775,c_tptpcol_8_72708) ),
inference(extension,[status(thm),parent(t64:3)],[f_156_3]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t64:3]) ).
cnf(t82,plain,
( ~ genls(c_tptpcol_11_72774,c_tptpcol_10_72710)
| ~ genls(c_tptpcol_12_72775,c_tptpcol_11_72774)
| genls(c_tptpcol_12_72775,c_tptpcol_10_72710) ),
inference(extension,[status(thm),parent(t80:2)],[f_156_3]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t80:2]) ).
cnf(t84,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(extension,[status(thm),parent(t82:2)],[f_54_2]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t82:2]) ).
cnf(t86,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(extension,[status(thm),parent(t82:3)],[f_52_2]) ).
cnf(t87,plain,
$false,
inference(connection,[status(thm),parent(t86:1)],[t86:1,t82:3]) ).
cnf(t88,plain,
( ~ genls(c_tptpcol_9_72709,c_tptpcol_8_72708)
| ~ genls(c_tptpcol_10_72710,c_tptpcol_9_72709)
| genls(c_tptpcol_10_72710,c_tptpcol_8_72708) ),
inference(extension,[status(thm),parent(t80:3)],[f_156_3]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t80:3]) ).
cnf(t90,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(extension,[status(thm),parent(t88:2)],[f_50_2]) ).
cnf(t91,plain,
$false,
inference(connection,[status(thm),parent(t90:1)],[t90:1,t88:2]) ).
cnf(t92,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(extension,[status(thm),parent(t88:3)],[f_48_2]) ).
cnf(t93,plain,
$false,
inference(connection,[status(thm),parent(t92:1)],[t92:1,t88:3]) ).
cnf(t94,plain,
( ~ genls(c_tptpcol_4_65539,c_tptpcol_1_65536)
| ~ genls(c_tptpcol_8_72708,c_tptpcol_4_65539)
| genls(c_tptpcol_8_72708,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t62:3)],[f_156_3]) ).
cnf(t95,plain,
$false,
inference(connection,[status(thm),parent(t94:1)],[t94:1,t62:3]) ).
cnf(t96,plain,
( ~ genls(c_tptpcol_6_71683,c_tptpcol_4_65539)
| ~ genls(c_tptpcol_8_72708,c_tptpcol_6_71683)
| genls(c_tptpcol_8_72708,c_tptpcol_4_65539) ),
inference(extension,[status(thm),parent(t94:2)],[f_156_3]) ).
cnf(t97,plain,
$false,
inference(connection,[status(thm),parent(t96:1)],[t96:1,t94:2]) ).
cnf(t98,plain,
( ~ genls(c_tptpcol_7_72707,c_tptpcol_6_71683)
| ~ genls(c_tptpcol_8_72708,c_tptpcol_7_72707)
| genls(c_tptpcol_8_72708,c_tptpcol_6_71683) ),
inference(extension,[status(thm),parent(t96:2)],[f_156_3]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t96:2]) ).
cnf(t100,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(extension,[status(thm),parent(t98:2)],[f_46_2]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t98:2]) ).
cnf(t102,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(extension,[status(thm),parent(t98:3)],[f_44_2]) ).
cnf(t103,plain,
$false,
inference(connection,[status(thm),parent(t102:1)],[t102:1,t98:3]) ).
cnf(t104,plain,
( ~ genls(c_tptpcol_5_69635,c_tptpcol_4_65539)
| ~ genls(c_tptpcol_6_71683,c_tptpcol_5_69635)
| genls(c_tptpcol_6_71683,c_tptpcol_4_65539) ),
inference(extension,[status(thm),parent(t96:3)],[f_156_3]) ).
cnf(t105,plain,
$false,
inference(connection,[status(thm),parent(t104:1)],[t104:1,t96:3]) ).
cnf(t106,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(extension,[status(thm),parent(t104:2)],[f_42_2]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t104:2]) ).
cnf(t108,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(extension,[status(thm),parent(t104:3)],[f_40_2]) ).
cnf(t109,plain,
$false,
inference(connection,[status(thm),parent(t108:1)],[t108:1,t104:3]) ).
cnf(t110,plain,
( ~ genls(c_tptpcol_2_65537,c_tptpcol_1_65536)
| ~ genls(c_tptpcol_4_65539,c_tptpcol_2_65537)
| genls(c_tptpcol_4_65539,c_tptpcol_1_65536) ),
inference(extension,[status(thm),parent(t94:3)],[f_156_3]) ).
cnf(t111,plain,
$false,
inference(connection,[status(thm),parent(t110:1)],[t110:1,t94:3]) ).
cnf(t112,plain,
( ~ genls(c_tptpcol_3_65538,c_tptpcol_2_65537)
| ~ genls(c_tptpcol_4_65539,c_tptpcol_3_65538)
| genls(c_tptpcol_4_65539,c_tptpcol_2_65537) ),
inference(extension,[status(thm),parent(t110:2)],[f_156_3]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t110:2]) ).
cnf(t114,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(extension,[status(thm),parent(t112:2)],[f_38_2]) ).
cnf(t115,plain,
$false,
inference(connection,[status(thm),parent(t114:1)],[t114:1,t112:2]) ).
cnf(t116,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(extension,[status(thm),parent(t112:3)],[f_36_2]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t112:3]) ).
cnf(t118,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(extension,[status(thm),parent(t110:3)],[f_34_2]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t110:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 15:47:42 UTC 2026
% 0.11/0.36 % CPUTime :
% 1.96/2.27 % SZS status Theorem for theBenchmark
% 1.96/2.27 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------