%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR036+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:18:12 EDT 2024
% Result : Theorem 36.72s 36.90s
% Output : Refutation 36.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 35
% Syntax : Number of formulae : 143 ( 95 unt; 0 def)
% Number of atoms : 203 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 113 ( 53 ~; 50 |; 4 &)
% ( 0 <=>; 6 =>; 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 : 73 ( 0 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query36,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query36) ).
fof(c0,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(assume_negation,[status(cth)],[query36]) ).
fof(c1,negated_conjecture,
( mtvisible(c_tptp_member974_mt)
& ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(fof_nnf,[status(thm)],[c0]) ).
cnf(c3,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(split_conjunct,[status(thm)],[c1]) ).
fof(just85,axiom,
! [OLD,ARG2,NEW] :
( ( disjointwith(OLD,ARG2)
& genls(NEW,OLD) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just85) ).
fof(c276,plain,
! [OLD,ARG2,NEW] :
( ~ disjointwith(OLD,ARG2)
| ~ genls(NEW,OLD)
| disjointwith(NEW,ARG2) ),
inference(fof_nnf,[status(thm)],[just85]) ).
fof(c277,plain,
! [X111,X112,X113] :
( ~ disjointwith(X111,X112)
| ~ genls(X113,X111)
| disjointwith(X113,X112) ),
inference(variable_rename,[status(thm)],[c276]) ).
cnf(c278,plain,
( ~ disjointwith(X341,X342)
| ~ genls(X343,X341)
| disjointwith(X343,X342) ),
inference(split_conjunct,[status(thm)],[c277]) ).
fof(just16,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just16) ).
cnf(c439,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(split_conjunct,[status(thm)],[just16]) ).
fof(just156,axiom,
! [ARG1,OLD,NEW] :
( ( genls(ARG1,OLD)
& genls(OLD,NEW) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just156) ).
fof(c59,plain,
! [ARG1,OLD,NEW] :
( ~ genls(ARG1,OLD)
| ~ genls(OLD,NEW)
| genls(ARG1,NEW) ),
inference(fof_nnf,[status(thm)],[just156]) ).
fof(c60,plain,
! [X30,X31,X32] :
( ~ genls(X30,X31)
| ~ genls(X31,X32)
| genls(X30,X32) ),
inference(variable_rename,[status(thm)],[c59]) ).
cnf(c61,plain,
( ~ genls(X242,X240)
| ~ genls(X240,X241)
| genls(X242,X241) ),
inference(split_conjunct,[status(thm)],[c60]) ).
cnf(c527,plain,
( ~ genls(X403,c_tptpcol_7_21508)
| genls(X403,c_tptpcol_6_20484) ),
inference(resolution,[status(thm)],[c61,c439]) ).
fof(just18,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just18) ).
cnf(c435,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(split_conjunct,[status(thm)],[just18]) ).
cnf(c526,plain,
( ~ genls(X402,c_tptpcol_8_22020)
| genls(X402,c_tptpcol_7_21508) ),
inference(resolution,[status(thm)],[c61,c435]) ).
fof(just20,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just20) ).
cnf(c431,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(split_conjunct,[status(thm)],[just20]) ).
cnf(c529,plain,
( ~ genls(X405,c_tptpcol_9_22021)
| genls(X405,c_tptpcol_8_22020) ),
inference(resolution,[status(thm)],[c61,c431]) ).
fof(just22,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just22) ).
cnf(c427,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(split_conjunct,[status(thm)],[just22]) ).
cnf(c534,plain,
( ~ genls(X410,c_tptpcol_10_22022)
| genls(X410,c_tptpcol_9_22021) ),
inference(resolution,[status(thm)],[c61,c427]) ).
fof(just24,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just24) ).
cnf(c423,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(split_conjunct,[status(thm)],[just24]) ).
cnf(c540,plain,
( ~ genls(X416,c_tptpcol_11_22023)
| genls(X416,c_tptpcol_10_22022) ),
inference(resolution,[status(thm)],[c61,c423]) ).
fof(just26,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just26) ).
cnf(c419,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(split_conjunct,[status(thm)],[just26]) ).
cnf(c538,plain,
( ~ genls(X414,c_tptpcol_12_22055)
| genls(X414,c_tptpcol_11_22023) ),
inference(resolution,[status(thm)],[c61,c419]) ).
fof(just28,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just28) ).
cnf(c415,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(split_conjunct,[status(thm)],[just28]) ).
cnf(c531,plain,
( ~ genls(X407,c_tptpcol_13_22071)
| genls(X407,c_tptpcol_12_22055) ),
inference(resolution,[status(thm)],[c61,c415]) ).
fof(just32,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just32) ).
cnf(c407,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(split_conjunct,[status(thm)],[just32]) ).
fof(just30,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just30) ).
cnf(c411,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(split_conjunct,[status(thm)],[just30]) ).
cnf(c544,plain,
( ~ genls(X420,c_tptpcol_14_22072)
| genls(X420,c_tptpcol_13_22071) ),
inference(resolution,[status(thm)],[c61,c411]) ).
cnf(c1191,plain,
genls(c_tptpcol_15_22076,c_tptpcol_13_22071),
inference(resolution,[status(thm)],[c544,c407]) ).
cnf(c1303,plain,
genls(c_tptpcol_15_22076,c_tptpcol_12_22055),
inference(resolution,[status(thm)],[c1191,c531]) ).
cnf(c1479,plain,
genls(c_tptpcol_15_22076,c_tptpcol_11_22023),
inference(resolution,[status(thm)],[c1303,c538]) ).
cnf(c1663,plain,
genls(c_tptpcol_15_22076,c_tptpcol_10_22022),
inference(resolution,[status(thm)],[c1479,c540]) ).
cnf(c1816,plain,
genls(c_tptpcol_15_22076,c_tptpcol_9_22021),
inference(resolution,[status(thm)],[c1663,c534]) ).
cnf(c1952,plain,
genls(c_tptpcol_15_22076,c_tptpcol_8_22020),
inference(resolution,[status(thm)],[c1816,c529]) ).
cnf(c2038,plain,
genls(c_tptpcol_15_22076,c_tptpcol_7_21508),
inference(resolution,[status(thm)],[c1952,c526]) ).
cnf(c2132,plain,
genls(c_tptpcol_15_22076,c_tptpcol_6_20484),
inference(resolution,[status(thm)],[c2038,c527]) ).
cnf(c2215,plain,
( ~ disjointwith(c_tptpcol_6_20484,X1299)
| disjointwith(c_tptpcol_15_22076,X1299) ),
inference(resolution,[status(thm)],[c2132,c278]) ).
fof(just84,axiom,
! [ARG1,OLD,NEW] :
( ( disjointwith(ARG1,OLD)
& genls(NEW,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just84) ).
fof(c279,plain,
! [ARG1,OLD,NEW] :
( ~ disjointwith(ARG1,OLD)
| ~ genls(NEW,OLD)
| disjointwith(ARG1,NEW) ),
inference(fof_nnf,[status(thm)],[just84]) ).
fof(c280,plain,
! [X114,X115,X116] :
( ~ disjointwith(X114,X115)
| ~ genls(X116,X115)
| disjointwith(X114,X116) ),
inference(variable_rename,[status(thm)],[c279]) ).
cnf(c281,plain,
( ~ disjointwith(X347,X346)
| ~ genls(X345,X346)
| disjointwith(X347,X345) ),
inference(split_conjunct,[status(thm)],[c280]) ).
fof(just58,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just58) ).
cnf(c355,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(split_conjunct,[status(thm)],[just58]) ).
cnf(c537,plain,
( ~ genls(X413,c_tptpcol_14_72792)
| genls(X413,c_tptpcol_13_72791) ),
inference(resolution,[status(thm)],[c61,c355]) ).
fof(just62,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just62) ).
cnf(c347,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(split_conjunct,[status(thm)],[just62]) ).
fof(just60,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just60) ).
cnf(c351,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(split_conjunct,[status(thm)],[just60]) ).
cnf(c545,plain,
( ~ genls(X421,c_tptpcol_15_72793)
| genls(X421,c_tptpcol_14_72792) ),
inference(resolution,[status(thm)],[c61,c351]) ).
cnf(c1200,plain,
genls(c_tptpcol_16_72795,c_tptpcol_14_72792),
inference(resolution,[status(thm)],[c545,c347]) ).
cnf(c1317,plain,
genls(c_tptpcol_16_72795,c_tptpcol_13_72791),
inference(resolution,[status(thm)],[c1200,c537]) ).
cnf(c1507,plain,
( ~ disjointwith(X894,c_tptpcol_13_72791)
| disjointwith(X894,c_tptpcol_16_72795) ),
inference(resolution,[status(thm)],[c1317,c281]) ).
fof(just48,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just48) ).
cnf(c375,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(split_conjunct,[status(thm)],[just48]) ).
cnf(c911,plain,
( ~ disjointwith(X598,c_tptpcol_8_72708)
| disjointwith(X598,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[c281,c375]) ).
fof(just46,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just46) ).
cnf(c379,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(split_conjunct,[status(thm)],[just46]) ).
fof(just44,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
cnf(c383,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(split_conjunct,[status(thm)],[just44]) ).
cnf(c525,plain,
( ~ genls(X401,c_tptpcol_7_72707)
| genls(X401,c_tptpcol_6_71683) ),
inference(resolution,[status(thm)],[c61,c383]) ).
cnf(c976,plain,
genls(c_tptpcol_8_72708,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[c525,c379]) ).
cnf(c993,plain,
( ~ disjointwith(X637,c_tptpcol_6_71683)
| disjointwith(X637,c_tptpcol_8_72708) ),
inference(resolution,[status(thm)],[c976,c281]) ).
fof(just42,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just42) ).
cnf(c387,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(split_conjunct,[status(thm)],[just42]) ).
cnf(c899,plain,
( ~ disjointwith(X586,c_tptpcol_5_69635)
| disjointwith(X586,c_tptpcol_6_71683) ),
inference(resolution,[status(thm)],[c281,c387]) ).
fof(just40,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just40) ).
cnf(c391,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(split_conjunct,[status(thm)],[just40]) ).
cnf(c909,plain,
( ~ disjointwith(X596,c_tptpcol_4_65539)
| disjointwith(X596,c_tptpcol_5_69635) ),
inference(resolution,[status(thm)],[c281,c391]) ).
fof(just14,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just14) ).
cnf(c443,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(split_conjunct,[status(thm)],[just14]) ).
cnf(c823,plain,
( ~ disjointwith(c_tptpcol_5_20483,X512)
| disjointwith(c_tptpcol_6_20484,X512) ),
inference(resolution,[status(thm)],[c278,c443]) ).
fof(just12,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just12) ).
cnf(c447,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(split_conjunct,[status(thm)],[just12]) ).
cnf(c868,plain,
( ~ disjointwith(c_tptpcol_4_16387,X557)
| disjointwith(c_tptpcol_5_20483,X557) ),
inference(resolution,[status(thm)],[c278,c447]) ).
fof(just10,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just10) ).
cnf(c451,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(split_conjunct,[status(thm)],[just10]) ).
cnf(c863,plain,
( ~ disjointwith(c_tptpcol_3_16386,X552)
| disjointwith(c_tptpcol_4_16387,X552) ),
inference(resolution,[status(thm)],[c278,c451]) ).
fof(just83,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just83) ).
fof(c282,plain,
! [X,Y] :
( ~ disjointwith(X,Y)
| disjointwith(Y,X) ),
inference(fof_nnf,[status(thm)],[just83]) ).
fof(c283,plain,
! [X117,X118] :
( ~ disjointwith(X117,X118)
| disjointwith(X118,X117) ),
inference(variable_rename,[status(thm)],[c282]) ).
cnf(c284,plain,
( ~ disjointwith(X340,X339)
| disjointwith(X339,X340) ),
inference(split_conjunct,[status(thm)],[c283]) ).
fof(just38,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just38) ).
cnf(c395,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(split_conjunct,[status(thm)],[just38]) ).
cnf(c850,plain,
( ~ disjointwith(c_tptpcol_3_65538,X539)
| disjointwith(c_tptpcol_4_65539,X539) ),
inference(resolution,[status(thm)],[c278,c395]) ).
fof(just6,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just6) ).
cnf(c459,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(split_conjunct,[status(thm)],[just6]) ).
cnf(c831,plain,
( ~ disjointwith(c_tptpcol_1_1,X520)
| disjointwith(c_tptpcol_2_2,X520) ),
inference(resolution,[status(thm)],[c278,c459]) ).
fof(just64,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just64) ).
cnf(c343,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[just64]) ).
cnf(c808,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolution,[status(thm)],[c284,c343]) ).
fof(just34,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just34) ).
cnf(c403,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[just34]) ).
cnf(c830,plain,
( ~ disjointwith(c_tptpcol_1_65536,X519)
| disjointwith(c_tptpcol_2_65537,X519) ),
inference(resolution,[status(thm)],[c278,c403]) ).
cnf(c2297,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_1_1),
inference(resolution,[status(thm)],[c830,c808]) ).
cnf(c2339,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[c2297,c284]) ).
cnf(c2378,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[c2339,c831]) ).
fof(just8,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just8) ).
cnf(c455,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(split_conjunct,[status(thm)],[just8]) ).
cnf(c857,plain,
( ~ disjointwith(c_tptpcol_2_2,X546)
| disjointwith(c_tptpcol_3_16386,X546) ),
inference(resolution,[status(thm)],[c278,c455]) ).
cnf(c2452,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[c857,c2378]) ).
cnf(c2455,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[c2452,c284]) ).
fof(just36,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just36) ).
cnf(c399,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(split_conjunct,[status(thm)],[just36]) ).
cnf(c862,plain,
( ~ disjointwith(c_tptpcol_2_65537,X551)
| disjointwith(c_tptpcol_3_65538,X551) ),
inference(resolution,[status(thm)],[c278,c399]) ).
cnf(c2473,plain,
disjointwith(c_tptpcol_3_65538,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[c862,c2455]) ).
cnf(c2488,plain,
disjointwith(c_tptpcol_4_65539,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[c2473,c850]) ).
cnf(c2527,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[c2488,c284]) ).
cnf(c2578,plain,
disjointwith(c_tptpcol_4_16387,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[c2527,c863]) ).
cnf(c2638,plain,
disjointwith(c_tptpcol_5_20483,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[c2578,c868]) ).
cnf(c2729,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[c2638,c823]) ).
cnf(c2833,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_5_69635),
inference(resolution,[status(thm)],[c2729,c909]) ).
cnf(c2977,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[c2833,c899]) ).
cnf(c3177,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_8_72708),
inference(resolution,[status(thm)],[c2977,c993]) ).
cnf(c3516,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[c3177,c911]) ).
fof(just56,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just56) ).
cnf(c359,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(split_conjunct,[status(thm)],[just56]) ).
fof(just54,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just54) ).
cnf(c363,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(split_conjunct,[status(thm)],[just54]) ).
cnf(c524,plain,
( ~ genls(X400,c_tptpcol_12_72775)
| genls(X400,c_tptpcol_11_72774) ),
inference(resolution,[status(thm)],[c61,c363]) ).
cnf(c970,plain,
genls(c_tptpcol_13_72791,c_tptpcol_11_72774),
inference(resolution,[status(thm)],[c524,c359]) ).
fof(just52,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just52) ).
cnf(c367,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(split_conjunct,[status(thm)],[just52]) ).
cnf(c530,plain,
( ~ genls(X406,c_tptpcol_11_72774)
| genls(X406,c_tptpcol_10_72710) ),
inference(resolution,[status(thm)],[c61,c367]) ).
cnf(c1029,plain,
genls(c_tptpcol_13_72791,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[c530,c970]) ).
fof(just50,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just50) ).
cnf(c371,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(split_conjunct,[status(thm)],[just50]) ).
cnf(c543,plain,
( ~ genls(X419,c_tptpcol_10_72710)
| genls(X419,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[c61,c371]) ).
cnf(c1175,plain,
genls(c_tptpcol_13_72791,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[c543,c1029]) ).
cnf(c1271,plain,
( ~ disjointwith(X771,c_tptpcol_9_72709)
| disjointwith(X771,c_tptpcol_13_72791) ),
inference(resolution,[status(thm)],[c1175,c281]) ).
cnf(c4380,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_13_72791),
inference(resolution,[status(thm)],[c1271,c3516]) ).
cnf(c6324,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c4380,c1507]) ).
cnf(c10482,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c6324,c2215]) ).
cnf(c12328,plain,
$false,
inference(resolution,[status(thm)],[c10482,c3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR036+1 : TPTP v8.1.2. Released v3.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n025.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 02:01:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 36.72/36.90 % Version: 1.5
% 36.72/36.90 % SZS status Theorem
% 36.72/36.90 % SZS output start CNFRefutation
% See solution above
% 36.72/36.91
% 36.72/36.91 % Initial clauses : 175
% 36.72/36.91 % Processed clauses : 2054
% 36.72/36.91 % Factors computed : 4
% 36.72/36.91 % Resolvents computed: 11863
% 36.72/36.91 % Tautologies deleted: 145
% 36.72/36.91 % Forward subsumed : 8170
% 36.72/36.91 % Backward subsumed : 4
% 36.72/36.91 % -------- CPU Time ---------
% 36.72/36.91 % User time : 36.531 s
% 36.72/36.91 % System time : 0.027 s
% 36.72/36.91 % Total time : 36.558 s
%------------------------------------------------------------------------------