%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Sun Sep 27 07:06:42 AM UTC 2026
% Result : Theorem 0.67s 0.52s
% Output : CNFRefutation 0.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 33
% Syntax : Number of formulae : 130 ( 95 unt; 0 def)
% Number of atoms : 167 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 89 ( 52 ~; 32 |; 1 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 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 : 39 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just83,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('theBenchmark.p',just83) ).
fof(just84,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('theBenchmark.p',just84) ).
fof(query36,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('theBenchmark.p',query36) ).
fof(query36_neg,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(assume_negation,[status(cth)],[query36]) ).
fof(just6,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('theBenchmark.p',just6) ).
cnf(c_163,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(clausify,[status(thm)],[just6]) ).
fof(just8,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('theBenchmark.p',just8) ).
cnf(c_165,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(clausify,[status(thm)],[just8]) ).
fof(just10,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('theBenchmark.p',just10) ).
cnf(c_167,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(clausify,[status(thm)],[just10]) ).
fof(just12,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('theBenchmark.p',just12) ).
cnf(c_169,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(clausify,[status(thm)],[just12]) ).
fof(just14,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('theBenchmark.p',just14) ).
cnf(c_171,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(clausify,[status(thm)],[just14]) ).
fof(just16,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('theBenchmark.p',just16) ).
cnf(c_173,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(clausify,[status(thm)],[just16]) ).
fof(just18,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('theBenchmark.p',just18) ).
cnf(c_175,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(clausify,[status(thm)],[just18]) ).
fof(just20,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('theBenchmark.p',just20) ).
cnf(c_177,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(clausify,[status(thm)],[just20]) ).
fof(just22,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('theBenchmark.p',just22) ).
cnf(c_179,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(clausify,[status(thm)],[just22]) ).
fof(just24,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('theBenchmark.p',just24) ).
cnf(c_181,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(clausify,[status(thm)],[just24]) ).
fof(just26,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('theBenchmark.p',just26) ).
cnf(c_183,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(clausify,[status(thm)],[just26]) ).
fof(just28,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('theBenchmark.p',just28) ).
cnf(c_185,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(clausify,[status(thm)],[just28]) ).
fof(just30,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('theBenchmark.p',just30) ).
cnf(c_187,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(clausify,[status(thm)],[just30]) ).
fof(just32,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('theBenchmark.p',just32) ).
cnf(c_189,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(clausify,[status(thm)],[just32]) ).
fof(just34,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('theBenchmark.p',just34) ).
cnf(c_191,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[just34]) ).
fof(just36,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('theBenchmark.p',just36) ).
cnf(c_193,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(clausify,[status(thm)],[just36]) ).
fof(just38,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('theBenchmark.p',just38) ).
cnf(c_195,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(clausify,[status(thm)],[just38]) ).
fof(just40,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('theBenchmark.p',just40) ).
cnf(c_197,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(clausify,[status(thm)],[just40]) ).
fof(just42,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('theBenchmark.p',just42) ).
cnf(c_199,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(clausify,[status(thm)],[just42]) ).
fof(just44,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('theBenchmark.p',just44) ).
cnf(c_201,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(clausify,[status(thm)],[just44]) ).
fof(just46,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('theBenchmark.p',just46) ).
cnf(c_203,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(clausify,[status(thm)],[just46]) ).
fof(just48,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('theBenchmark.p',just48) ).
cnf(c_205,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(clausify,[status(thm)],[just48]) ).
fof(just50,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('theBenchmark.p',just50) ).
cnf(c_207,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(clausify,[status(thm)],[just50]) ).
fof(just52,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('theBenchmark.p',just52) ).
cnf(c_209,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(clausify,[status(thm)],[just52]) ).
fof(just54,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('theBenchmark.p',just54) ).
cnf(c_211,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(clausify,[status(thm)],[just54]) ).
fof(just56,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('theBenchmark.p',just56) ).
cnf(c_213,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(clausify,[status(thm)],[just56]) ).
fof(just58,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('theBenchmark.p',just58) ).
cnf(c_215,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(clausify,[status(thm)],[just58]) ).
fof(just60,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('theBenchmark.p',just60) ).
cnf(c_217,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(clausify,[status(thm)],[just60]) ).
fof(just62,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('theBenchmark.p',just62) ).
cnf(c_219,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(clausify,[status(thm)],[just62]) ).
fof(just64,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('theBenchmark.p',just64) ).
cnf(c_221,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[just64]) ).
cnf(c_228,plain,
( disjointwith(B,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just83]) ).
cnf(c_229,plain,
( disjointwith(A,C)
| ~ genls(C,B)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just84]) ).
cnf(c_304,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(clausify,[status(thm)],[query36_neg]) ).
cnf(c_349,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolve,[status(thm)],[c_228,c_221]) ).
cnf(c_1658,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_1_1) ),
inference(resolve,[status(thm)],[c_229,c_349]) ).
cnf(c_367,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(resolve,[status(thm)],[c_1658,c_163]) ).
cnf(c_1659,plain,
( disjointwith(A,c_tptpcol_16_72795)
| ~ disjointwith(A,c_tptpcol_15_72793) ),
inference(resolve,[status(thm)],[c_229,c_219]) ).
cnf(c_368,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(resolve,[status(thm)],[c_1659,c_304]) ).
cnf(c_1660,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_2_2) ),
inference(resolve,[status(thm)],[c_229,c_367]) ).
cnf(c_371,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_1660,c_165]) ).
cnf(c_1661,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_3_16386) ),
inference(resolve,[status(thm)],[c_229,c_371]) ).
cnf(c_375,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_4_16387),
inference(resolve,[status(thm)],[c_1661,c_167]) ).
cnf(c_379,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_15_22076),
inference(resolve,[status(thm)],[c_368,c_228]) ).
cnf(c_1662,plain,
( disjointwith(A,c_tptpcol_15_22076)
| ~ disjointwith(A,c_tptpcol_14_22072) ),
inference(resolve,[status(thm)],[c_229,c_189]) ).
cnf(c_384,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_14_22072),
inference(resolve,[status(thm)],[c_1662,c_379]) ).
cnf(c_1663,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_4_16387) ),
inference(resolve,[status(thm)],[c_229,c_375]) ).
cnf(c_389,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_5_20483),
inference(resolve,[status(thm)],[c_1663,c_169]) ).
cnf(c_1664,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_5_20483) ),
inference(resolve,[status(thm)],[c_229,c_389]) ).
cnf(c_394,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_6_20484),
inference(resolve,[status(thm)],[c_1664,c_171]) ).
cnf(c_403,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_1_65536),
inference(resolve,[status(thm)],[c_228,c_394]) ).
cnf(c_1665,plain,
( disjointwith(A,c_tptpcol_14_22072)
| ~ disjointwith(A,c_tptpcol_13_22071) ),
inference(resolve,[status(thm)],[c_229,c_187]) ).
cnf(c_410,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_13_22071),
inference(resolve,[status(thm)],[c_1665,c_384]) ).
cnf(c_1666,plain,
( disjointwith(A,c_tptpcol_13_22071)
| ~ disjointwith(A,c_tptpcol_12_22055) ),
inference(resolve,[status(thm)],[c_229,c_185]) ).
cnf(c_414,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_12_22055),
inference(resolve,[status(thm)],[c_1666,c_410]) ).
cnf(c_1667,plain,
( disjointwith(A,c_tptpcol_12_22055)
| ~ disjointwith(A,c_tptpcol_11_22023) ),
inference(resolve,[status(thm)],[c_229,c_183]) ).
cnf(c_421,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_11_22023),
inference(resolve,[status(thm)],[c_1667,c_414]) ).
cnf(c_1668,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_1_65536) ),
inference(resolve,[status(thm)],[c_229,c_403]) ).
cnf(c_428,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1668,c_191]) ).
cnf(c_1669,plain,
( disjointwith(A,c_tptpcol_11_22023)
| ~ disjointwith(A,c_tptpcol_10_22022) ),
inference(resolve,[status(thm)],[c_229,c_181]) ).
cnf(c_452,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_10_22022),
inference(resolve,[status(thm)],[c_1669,c_421]) ).
cnf(c_1670,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_2_65537) ),
inference(resolve,[status(thm)],[c_229,c_428]) ).
cnf(c_464,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_3_65538),
inference(resolve,[status(thm)],[c_1670,c_193]) ).
cnf(c_1671,plain,
( disjointwith(A,c_tptpcol_10_22022)
| ~ disjointwith(A,c_tptpcol_9_22021) ),
inference(resolve,[status(thm)],[c_229,c_179]) ).
cnf(c_472,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_9_22021),
inference(resolve,[status(thm)],[c_1671,c_452]) ).
cnf(c_1672,plain,
( disjointwith(A,c_tptpcol_9_22021)
| ~ disjointwith(A,c_tptpcol_8_22020) ),
inference(resolve,[status(thm)],[c_229,c_177]) ).
cnf(c_499,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_8_22020),
inference(resolve,[status(thm)],[c_1672,c_472]) ).
cnf(c_1673,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_3_65538) ),
inference(resolve,[status(thm)],[c_229,c_464]) ).
cnf(c_506,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_4_65539),
inference(resolve,[status(thm)],[c_1673,c_195]) ).
cnf(c_1674,plain,
( disjointwith(A,c_tptpcol_8_22020)
| ~ disjointwith(A,c_tptpcol_7_21508) ),
inference(resolve,[status(thm)],[c_229,c_175]) ).
cnf(c_516,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_7_21508),
inference(resolve,[status(thm)],[c_1674,c_499]) ).
cnf(c_1675,plain,
( disjointwith(A,c_tptpcol_7_21508)
| ~ disjointwith(A,c_tptpcol_6_20484) ),
inference(resolve,[status(thm)],[c_229,c_173]) ).
cnf(c_535,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_6_20484),
inference(resolve,[status(thm)],[c_1675,c_516]) ).
cnf(c_565,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_15_72793),
inference(resolve,[status(thm)],[c_535,c_228]) ).
cnf(c_1676,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_4_65539) ),
inference(resolve,[status(thm)],[c_229,c_506]) ).
cnf(c_569,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_5_69635),
inference(resolve,[status(thm)],[c_1676,c_197]) ).
cnf(c_1677,plain,
( disjointwith(A,c_tptpcol_15_72793)
| ~ disjointwith(A,c_tptpcol_14_72792) ),
inference(resolve,[status(thm)],[c_229,c_217]) ).
cnf(c_605,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_14_72792),
inference(resolve,[status(thm)],[c_1677,c_565]) ).
cnf(c_1678,plain,
( disjointwith(A,c_tptpcol_14_72792)
| ~ disjointwith(A,c_tptpcol_13_72791) ),
inference(resolve,[status(thm)],[c_229,c_215]) ).
cnf(c_625,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_13_72791),
inference(resolve,[status(thm)],[c_1678,c_605]) ).
cnf(c_1679,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_5_69635) ),
inference(resolve,[status(thm)],[c_229,c_569]) ).
cnf(c_640,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_6_71683),
inference(resolve,[status(thm)],[c_1679,c_199]) ).
cnf(c_1680,plain,
( disjointwith(A,c_tptpcol_13_72791)
| ~ disjointwith(A,c_tptpcol_12_72775) ),
inference(resolve,[status(thm)],[c_229,c_213]) ).
cnf(c_822,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_12_72775),
inference(resolve,[status(thm)],[c_1680,c_625]) ).
cnf(c_1681,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_6_71683) ),
inference(resolve,[status(thm)],[c_229,c_640]) ).
cnf(c_847,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_7_72707),
inference(resolve,[status(thm)],[c_1681,c_201]) ).
cnf(c_1682,plain,
( disjointwith(A,c_tptpcol_12_72775)
| ~ disjointwith(A,c_tptpcol_11_72774) ),
inference(resolve,[status(thm)],[c_229,c_211]) ).
cnf(c_1032,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_11_72774),
inference(resolve,[status(thm)],[c_1682,c_822]) ).
cnf(c_1683,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_7_72707) ),
inference(resolve,[status(thm)],[c_229,c_847]) ).
cnf(c_1070,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_8_72708),
inference(resolve,[status(thm)],[c_1683,c_203]) ).
cnf(c_1684,plain,
( disjointwith(A,c_tptpcol_11_72774)
| ~ disjointwith(A,c_tptpcol_10_72710) ),
inference(resolve,[status(thm)],[c_229,c_209]) ).
cnf(c_1265,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_10_72710),
inference(resolve,[status(thm)],[c_1684,c_1032]) ).
cnf(c_1685,plain,
( disjointwith(c_tptpcol_6_20484,A)
| ~ genls(A,c_tptpcol_8_72708) ),
inference(resolve,[status(thm)],[c_229,c_1070]) ).
cnf(c_1293,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_9_72709),
inference(resolve,[status(thm)],[c_1685,c_205]) ).
cnf(c_1686,plain,
( disjointwith(A,c_tptpcol_10_72710)
| ~ disjointwith(A,c_tptpcol_9_72709) ),
inference(resolve,[status(thm)],[c_229,c_207]) ).
cnf(c_1687,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_9_72709),
inference(resolve,[status(thm)],[c_1686,c_1265]) ).
cnf(c_1657,plain,
$false,
inference(resolve,[status(thm)],[c_1293,c_1687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 00:05:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2414686 was started by sandbox2 on n006,
% 0.10/0.37 % Sun Sep 27 00:05:43 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.39
% 0.10/0.39 % From the command line: assign(max_seconds, 300).
% 0.10/0.39
% 0.10/0.39 % SInE: 150 to sos, 23 to usable, of 173 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.67/0.52
% 0.67/0.52 % given #500 (T,wt=8): 1068 disjointwith(c_tptpcol_6_71683,c_tptpcol_8_22020). [ur(228,a,844,a)].
% 0.67/0.52
% 0.67/0.52 % SZS status Theorem for theBenchmark
% 0.67/0.52
% 0.67/0.52 % Proof 1 at 0.09 (+ 0.03) seconds.
% 0.67/0.52 % Length of proof is 69.
% 0.67/0.52 % Level of proof is 19.
% 0.67/0.52 % Maximum clause weight is 708.000.
% 0.67/0.52 % Given clauses 587.
% 0.67/0.52
% 0.67/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------