%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR061+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:30 EDT 2024
% Result : Theorem 1.97s 2.23s
% Output : Refutation 1.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 22
% Syntax : Number of formulae : 89 ( 54 unt; 0 def)
% Number of atoms : 136 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 87 ( 40 ~; 37 |; 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 : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 60 ( 0 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query61,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query61) ).
fof(c0,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(assume_negation,[status(cth)],[query61]) ).
fof(c1,negated_conjecture,
( mtvisible(c_timehasnoendmt)
& ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(fof_nnf,[status(thm)],[c0]) ).
cnf(c3,negated_conjecture,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(split_conjunct,[status(thm)],[c1]) ).
fof(just55,axiom,
! [ARG1,OLD,NEW] :
( ( disjointwith(ARG1,OLD)
& genls(NEW,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just55) ).
fof(c201,plain,
! [ARG1,OLD,NEW] :
( ~ disjointwith(ARG1,OLD)
| ~ genls(NEW,OLD)
| disjointwith(ARG1,NEW) ),
inference(fof_nnf,[status(thm)],[just55]) ).
fof(c202,plain,
! [X88,X89,X90] :
( ~ disjointwith(X88,X89)
| ~ genls(X90,X89)
| disjointwith(X88,X90) ),
inference(variable_rename,[status(thm)],[c201]) ).
cnf(c203,plain,
( ~ disjointwith(X267,X269)
| ~ genls(X268,X269)
| disjointwith(X267,X268) ),
inference(split_conjunct,[status(thm)],[c202]) ).
fof(just35,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just35) ).
cnf(c267,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(split_conjunct,[status(thm)],[just35]) ).
fof(just33,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just33) ).
cnf(c271,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(split_conjunct,[status(thm)],[just33]) ).
fof(just101,axiom,
! [ARG1,OLD,NEW] :
( ( genls(ARG1,OLD)
& genls(OLD,NEW) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just101) ).
fof(c59,plain,
! [ARG1,OLD,NEW] :
( ~ genls(ARG1,OLD)
| ~ genls(OLD,NEW)
| genls(ARG1,NEW) ),
inference(fof_nnf,[status(thm)],[just101]) ).
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(X193,X192)
| ~ genls(X192,X194)
| genls(X193,X194) ),
inference(split_conjunct,[status(thm)],[c60]) ).
cnf(c413,plain,
( ~ genls(X314,c_tptpcol_13_118117)
| genls(X314,c_tptpcol_12_118116) ),
inference(resolution,[status(thm)],[c61,c271]) ).
cnf(c646,plain,
genls(c_tptpcol_14_118118,c_tptpcol_12_118116),
inference(resolution,[status(thm)],[c413,c267]) ).
fof(just31,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just31) ).
cnf(c275,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(split_conjunct,[status(thm)],[just31]) ).
cnf(c419,plain,
( ~ genls(X320,c_tptpcol_12_118116)
| genls(X320,c_tptpcol_11_118084) ),
inference(resolution,[status(thm)],[c61,c275]) ).
cnf(c693,plain,
genls(c_tptpcol_14_118118,c_tptpcol_11_118084),
inference(resolution,[status(thm)],[c419,c646]) ).
fof(just29,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just29) ).
cnf(c279,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(split_conjunct,[status(thm)],[just29]) ).
cnf(c421,plain,
( ~ genls(X322,c_tptpcol_11_118084)
| genls(X322,c_tptpcol_10_118020) ),
inference(resolution,[status(thm)],[c61,c279]) ).
cnf(c719,plain,
genls(c_tptpcol_14_118118,c_tptpcol_10_118020),
inference(resolution,[status(thm)],[c421,c693]) ).
cnf(c738,plain,
( ~ disjointwith(X493,c_tptpcol_10_118020)
| disjointwith(X493,c_tptpcol_14_118118) ),
inference(resolution,[status(thm)],[c719,c203]) ).
fof(just23,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just23) ).
cnf(c291,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(split_conjunct,[status(thm)],[just23]) ).
fof(just21,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just21) ).
cnf(c295,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(split_conjunct,[status(thm)],[just21]) ).
cnf(c410,plain,
( ~ genls(X311,c_tptpcol_7_117762)
| genls(X311,c_tptpcol_6_116738) ),
inference(resolution,[status(thm)],[c61,c295]) ).
cnf(c629,plain,
genls(c_tptpcol_8_117763,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[c410,c291]) ).
cnf(c632,plain,
( ~ disjointwith(X441,c_tptpcol_6_116738)
| disjointwith(X441,c_tptpcol_8_117763) ),
inference(resolution,[status(thm)],[c629,c203]) ).
fof(just13,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just13) ).
cnf(c311,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(split_conjunct,[status(thm)],[just13]) ).
fof(just56,axiom,
! [OLD,ARG2,NEW] :
( ( disjointwith(OLD,ARG2)
& genls(NEW,OLD) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just56) ).
fof(c198,plain,
! [OLD,ARG2,NEW] :
( ~ disjointwith(OLD,ARG2)
| ~ genls(NEW,OLD)
| disjointwith(NEW,ARG2) ),
inference(fof_nnf,[status(thm)],[just56]) ).
fof(c199,plain,
! [X85,X86,X87] :
( ~ disjointwith(X85,X86)
| ~ genls(X87,X85)
| disjointwith(X87,X86) ),
inference(variable_rename,[status(thm)],[c198]) ).
cnf(c200,plain,
( ~ disjointwith(X263,X264)
| ~ genls(X265,X263)
| disjointwith(X265,X264) ),
inference(split_conjunct,[status(thm)],[c199]) ).
cnf(c549,plain,
( ~ disjointwith(c_tptpcol_7_113665,X379)
| disjointwith(c_tptpcol_8_114177,X379) ),
inference(resolution,[status(thm)],[c200,c311]) ).
fof(just11,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just11) ).
cnf(c315,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(split_conjunct,[status(thm)],[just11]) ).
cnf(c537,plain,
( ~ disjointwith(c_tptpcol_6_112641,X367)
| disjointwith(c_tptpcol_7_113665,X367) ),
inference(resolution,[status(thm)],[c200,c315]) ).
fof(just9,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just9) ).
cnf(c319,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(split_conjunct,[status(thm)],[just9]) ).
cnf(c566,plain,
( ~ disjointwith(c_tptpcol_5_110593,X396)
| disjointwith(c_tptpcol_6_112641,X396) ),
inference(resolution,[status(thm)],[c200,c319]) ).
fof(just7,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just7) ).
cnf(c323,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(split_conjunct,[status(thm)],[just7]) ).
cnf(c567,plain,
( ~ disjointwith(c_tptpcol_4_106497,X397)
| disjointwith(c_tptpcol_5_110593,X397) ),
inference(resolution,[status(thm)],[c200,c323]) ).
fof(just54,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just54) ).
fof(c204,plain,
! [X,Y] :
( ~ disjointwith(X,Y)
| disjointwith(Y,X) ),
inference(fof_nnf,[status(thm)],[just54]) ).
fof(c205,plain,
! [X91,X92] :
( ~ disjointwith(X91,X92)
| disjointwith(X92,X91) ),
inference(variable_rename,[status(thm)],[c204]) ).
cnf(c206,plain,
( ~ disjointwith(X262,X261)
| disjointwith(X261,X262) ),
inference(split_conjunct,[status(thm)],[c205]) ).
fof(just19,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just19) ).
cnf(c299,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(split_conjunct,[status(thm)],[just19]) ).
cnf(c536,plain,
( ~ disjointwith(c_tptpcol_5_114690,X366)
| disjointwith(c_tptpcol_6_116738,X366) ),
inference(resolution,[status(thm)],[c200,c299]) ).
fof(just17,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
cnf(c303,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(split_conjunct,[status(thm)],[just17]) ).
cnf(c544,plain,
( ~ disjointwith(c_tptpcol_4_114689,X374)
| disjointwith(c_tptpcol_5_114690,X374) ),
inference(resolution,[status(thm)],[c200,c303]) ).
fof(just37,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just37) ).
cnf(c263,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(split_conjunct,[status(thm)],[just37]) ).
fof(just5,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just5) ).
cnf(c327,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(split_conjunct,[status(thm)],[just5]) ).
cnf(c561,plain,
( ~ disjointwith(c_tptpcol_3_98305,X391)
| disjointwith(c_tptpcol_4_106497,X391) ),
inference(resolution,[status(thm)],[c200,c327]) ).
cnf(c1099,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_3_114688),
inference(resolution,[status(thm)],[c561,c263]) ).
cnf(c1101,plain,
disjointwith(c_tptpcol_3_114688,c_tptpcol_4_106497),
inference(resolution,[status(thm)],[c1099,c206]) ).
fof(just15,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
cnf(c307,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(split_conjunct,[status(thm)],[just15]) ).
cnf(c565,plain,
( ~ disjointwith(c_tptpcol_3_114688,X395)
| disjointwith(c_tptpcol_4_114689,X395) ),
inference(resolution,[status(thm)],[c200,c307]) ).
cnf(c1108,plain,
disjointwith(c_tptpcol_4_114689,c_tptpcol_4_106497),
inference(resolution,[status(thm)],[c565,c1101]) ).
cnf(c1111,plain,
disjointwith(c_tptpcol_5_114690,c_tptpcol_4_106497),
inference(resolution,[status(thm)],[c1108,c544]) ).
cnf(c1121,plain,
disjointwith(c_tptpcol_6_116738,c_tptpcol_4_106497),
inference(resolution,[status(thm)],[c1111,c536]) ).
cnf(c1143,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[c1121,c206]) ).
cnf(c1174,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[c1143,c567]) ).
cnf(c1226,plain,
disjointwith(c_tptpcol_6_112641,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[c1174,c566]) ).
cnf(c1287,plain,
disjointwith(c_tptpcol_7_113665,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[c1226,c537]) ).
cnf(c1370,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[c1287,c549]) ).
cnf(c1493,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_8_117763),
inference(resolution,[status(thm)],[c1370,c632]) ).
fof(just27,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just27) ).
cnf(c283,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(split_conjunct,[status(thm)],[just27]) ).
fof(just25,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just25) ).
cnf(c287,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(split_conjunct,[status(thm)],[just25]) ).
cnf(c418,plain,
( ~ genls(X319,c_tptpcol_9_118019)
| genls(X319,c_tptpcol_8_117763) ),
inference(resolution,[status(thm)],[c61,c287]) ).
cnf(c685,plain,
genls(c_tptpcol_10_118020,c_tptpcol_8_117763),
inference(resolution,[status(thm)],[c418,c283]) ).
cnf(c689,plain,
( ~ disjointwith(X469,c_tptpcol_8_117763)
| disjointwith(X469,c_tptpcol_10_118020) ),
inference(resolution,[status(thm)],[c685,c203]) ).
cnf(c1698,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_10_118020),
inference(resolution,[status(thm)],[c689,c1493]) ).
cnf(c1930,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(resolution,[status(thm)],[c1698,c738]) ).
cnf(c2403,plain,
$false,
inference(resolution,[status(thm)],[c1930,c3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : CSR061+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 01:50:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.97/2.23 % Version: 1.5
% 1.97/2.23 % SZS status Theorem
% 1.97/2.23 % SZS output start CNFRefutation
% See solution above
% 1.97/2.23
% 1.97/2.23 % Initial clauses : 120
% 1.97/2.23 % Processed clauses : 543
% 1.97/2.23 % Factors computed : 4
% 1.97/2.23 % Resolvents computed: 2071
% 1.97/2.23 % Tautologies deleted: 87
% 1.97/2.23 % Forward subsumed : 910
% 1.97/2.23 % Backward subsumed : 1
% 1.97/2.23 % -------- CPU Time ---------
% 1.97/2.23 % User time : 1.857 s
% 1.97/2.23 % System time : 0.017 s
% 1.97/2.23 % Total time : 1.874 s
%------------------------------------------------------------------------------