%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SEU148+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:58:12 AM UTC 2026
% Result : Theorem 100.44s 100.95s
% Output : Proof 100.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of formulae : 88 ( 37 unt; 0 def)
% Number of atoms : 281 ( 89 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 320 ( 127 ~; 111 |; 72 &)
% ( 8 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 165 ( 8 sgn 130 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d1_tarski,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('theBenchmark.p',d1_tarski) ).
fof(d4_xboole_0,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('theBenchmark.p',d4_xboole_0) ).
fof(d7_xboole_0,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_intersection2(A,B) = empty_set ),
file('theBenchmark.p',d7_xboole_0) ).
fof(d8_xboole_0,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('theBenchmark.p',d8_xboole_0) ).
fof(fc1_xboole_0,axiom,
empty(empty_set),
file('theBenchmark.p',fc1_xboole_0) ).
fof(irreflexivity_r2_xboole_0,axiom,
! [A,B] : ~ proper_subset(A,A),
file('theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(l2_zfmisc_1,lemma,
! [A,B] :
( subset(singleton(A),B)
<=> in(A,B) ),
file('theBenchmark.p',l2_zfmisc_1) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : subset(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t2_boole,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('theBenchmark.p',t2_boole) ).
fof(t6_zfmisc_1,conjecture,
! [A,B] :
( subset(singleton(A),singleton(B))
=> A = B ),
file('theBenchmark.p',t6_zfmisc_1) ).
fof(t7_boole,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('theBenchmark.p',t7_boole) ).
fof(t83_xboole_1,lemma,
! [A,B] :
( disjoint(A,B)
<=> set_difference(A,B) = A ),
file('theBenchmark.p',t83_xboole_1) ).
fof(f_7_1,plain,
! [A,B] :
( ( B = singleton(A)
| ? [C] :
( ( ~ in(C,B)
& C = A )
| ( C != A
& in(C,B) ) ) )
& ( ! [C] :
( ( in(C,B)
| C != A )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(fof_nnf,[status(thm)],[d1_tarski]) ).
fof(f_7_2,plain,
! [U_19,U_18] :
( ( U_18 = singleton(U_19)
| ? [U_17] :
( ( ~ in(U_17,U_18)
& U_17 = U_19 )
| ( U_17 != U_19
& in(U_17,U_18) ) ) )
& ( ! [U_16] :
( ( in(U_16,U_18)
| U_16 != U_19 )
& ( U_16 = U_19
| ~ in(U_16,U_18) ) )
| U_18 != singleton(U_19) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_27,U_25] :
( U_25 = singleton(U_27)
| ? [U_23] :
( ~ in(U_23,U_25)
& U_23 = U_27 )
| ? [U_22] :
( U_22 != U_27
& in(U_22,U_25) ) )
& ! [U_26,U_24] :
( ( ! [U_21] :
( in(U_21,U_24)
| U_21 != U_26 )
& ! [U_20] :
( U_20 = U_26
| ~ in(U_20,U_24) ) )
| U_24 != singleton(U_26) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_27,U_25] :
( U_25 = singleton(U_27)
| ? [U_23] :
( ~ in(U_23,U_25)
& U_23 = U_27 )
| ( sK1(U_27,U_25) != U_27
& in(sK1(U_27,U_25),U_25) ) )
& ! [U_26,U_24] :
( ( ! [U_21] :
( in(U_21,U_24)
| U_21 != U_26 )
& ! [U_20] :
( U_20 = U_26
| ~ in(U_20,U_24) ) )
| U_24 != singleton(U_26) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_22,sK1(U_27,U_25))],[f_7_3]) ).
fof(f_7_5,plain,
( ! [U_27,U_25] :
( U_25 = singleton(U_27)
| ( ~ in(sK2(U_27,U_25),U_25)
& sK2(U_27,U_25) = U_27 )
| ( sK1(U_27,U_25) != U_27
& in(sK1(U_27,U_25),U_25) ) )
& ! [U_26,U_24] :
( ( ! [U_21] :
( in(U_21,U_24)
| U_21 != U_26 )
& ! [U_20] :
( U_20 = U_26
| ~ in(U_20,U_24) ) )
| U_24 != singleton(U_26) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_23,sK2(U_27,U_25))],[f_7_4]) ).
cnf(f_7_6,plain,
( U_20 = U_26
| ~ in(U_20,U_24)
| U_24 != singleton(U_26) ),
inference(clausify,[status(thm)],[f_7_5]) ).
fof(f_14_1,plain,
! [A,B,C] :
( ( C = set_difference(A,B)
| ? [D] :
( ( ~ in(D,C)
& ~ in(D,B)
& in(D,A) )
| ( ( in(D,B)
| ~ in(D,A) )
& in(D,C) ) ) )
& ( ! [D] :
( ( in(D,C)
| in(D,B)
| ~ in(D,A) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(fof_nnf,[status(thm)],[d4_xboole_0]) ).
fof(f_14_2,plain,
! [U_102,U_101,U_100] :
( ( U_100 = set_difference(U_102,U_101)
| ? [U_99] :
( ( ~ in(U_99,U_100)
& ~ in(U_99,U_101)
& in(U_99,U_102) )
| ( ( in(U_99,U_101)
| ~ in(U_99,U_102) )
& in(U_99,U_100) ) ) )
& ( ! [U_98] :
( ( in(U_98,U_100)
| in(U_98,U_101)
| ~ in(U_98,U_102) )
& ( ( ~ in(U_98,U_101)
& in(U_98,U_102) )
| ~ in(U_98,U_100) ) )
| U_100 != set_difference(U_102,U_101) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_112,U_110,U_108] :
( U_108 = set_difference(U_112,U_110)
| ? [U_106] :
( ~ in(U_106,U_108)
& ~ in(U_106,U_110)
& in(U_106,U_112) )
| ? [U_105] :
( ( in(U_105,U_110)
| ~ in(U_105,U_112) )
& in(U_105,U_108) ) )
& ! [U_111,U_109,U_107] :
( ( ! [U_104] :
( in(U_104,U_107)
| in(U_104,U_109)
| ~ in(U_104,U_111) )
& ! [U_103] :
( ( ~ in(U_103,U_109)
& in(U_103,U_111) )
| ~ in(U_103,U_107) ) )
| U_107 != set_difference(U_111,U_109) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_112,U_110,U_108] :
( U_108 = set_difference(U_112,U_110)
| ? [U_106] :
( ~ in(U_106,U_108)
& ~ in(U_106,U_110)
& in(U_106,U_112) )
| ( ( in(sK13(U_112,U_110,U_108),U_110)
| ~ in(sK13(U_112,U_110,U_108),U_112) )
& in(sK13(U_112,U_110,U_108),U_108) ) )
& ! [U_111,U_109,U_107] :
( ( ! [U_104] :
( in(U_104,U_107)
| in(U_104,U_109)
| ~ in(U_104,U_111) )
& ! [U_103] :
( ( ~ in(U_103,U_109)
& in(U_103,U_111) )
| ~ in(U_103,U_107) ) )
| U_107 != set_difference(U_111,U_109) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_105,sK13(U_112,U_110,U_108))],[f_14_3]) ).
fof(f_14_5,plain,
( ! [U_112,U_110,U_108] :
( U_108 = set_difference(U_112,U_110)
| ( ~ in(sK14(U_112,U_110,U_108),U_108)
& ~ in(sK14(U_112,U_110,U_108),U_110)
& in(sK14(U_112,U_110,U_108),U_112) )
| ( ( in(sK13(U_112,U_110,U_108),U_110)
| ~ in(sK13(U_112,U_110,U_108),U_112) )
& in(sK13(U_112,U_110,U_108),U_108) ) )
& ! [U_111,U_109,U_107] :
( ( ! [U_104] :
( in(U_104,U_107)
| in(U_104,U_109)
| ~ in(U_104,U_111) )
& ! [U_103] :
( ( ~ in(U_103,U_109)
& in(U_103,U_111) )
| ~ in(U_103,U_107) ) )
| U_107 != set_difference(U_111,U_109) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_106,sK14(U_112,U_110,U_108))],[f_14_4]) ).
cnf(f_14_8,plain,
( in(U_104,U_107)
| in(U_104,U_109)
| ~ in(U_104,U_111)
| U_107 != set_difference(U_111,U_109) ),
inference(clausify,[status(thm)],[f_14_5]) ).
fof(f_15_1,plain,
! [A,B] :
( ( disjoint(A,B)
| set_intersection2(A,B) != empty_set )
& ( set_intersection2(A,B) = empty_set
| ~ disjoint(A,B) ) ),
inference(fof_nnf,[status(thm)],[d7_xboole_0]) ).
fof(f_15_2,plain,
! [U_114,U_113] :
( ( disjoint(U_114,U_113)
| set_intersection2(U_114,U_113) != empty_set )
& ( set_intersection2(U_114,U_113) = empty_set
| ~ disjoint(U_114,U_113) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_118,U_116] :
( disjoint(U_118,U_116)
| set_intersection2(U_118,U_116) != empty_set )
& ! [U_117,U_115] :
( set_intersection2(U_117,U_115) = empty_set
| ~ disjoint(U_117,U_115) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
cnf(f_15_5,plain,
( disjoint(U_118,U_116)
| set_intersection2(U_118,U_116) != empty_set ),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
! [A,B] :
( ( proper_subset(A,B)
| A = B
| ~ subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(fof_nnf,[status(thm)],[d8_xboole_0]) ).
fof(f_16_2,plain,
! [U_120,U_119] :
( ( proper_subset(U_120,U_119)
| U_120 = U_119
| ~ subset(U_120,U_119) )
& ( ( U_120 != U_119
& subset(U_120,U_119) )
| ~ proper_subset(U_120,U_119) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_124,U_122] :
( proper_subset(U_124,U_122)
| U_124 = U_122
| ~ subset(U_124,U_122) )
& ! [U_123,U_121] :
( ( U_123 != U_121
& subset(U_123,U_121) )
| ~ proper_subset(U_123,U_121) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_6,plain,
( proper_subset(U_124,U_122)
| U_124 = U_122
| ~ subset(U_124,U_122) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_24_1,plain,
empty(empty_set),
inference(fof_nnf,[status(thm)],[fc1_xboole_0]) ).
cnf(f_24_2,plain,
empty(empty_set),
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_29_1,plain,
! [A,B] : ~ proper_subset(A,A),
inference(fof_nnf,[status(thm)],[irreflexivity_r2_xboole_0]) ).
fof(f_29_2,plain,
! [U_134,U_133] : ~ proper_subset(U_134,U_134),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
! [U_134] : ~ proper_subset(U_134,U_134),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
~ proper_subset(U_134,U_134),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_31_1,plain,
! [A,B] :
( ( subset(singleton(A),B)
| ~ in(A,B) )
& ( in(A,B)
| ~ subset(singleton(A),B) ) ),
inference(fof_nnf,[status(thm)],[l2_zfmisc_1]) ).
fof(f_31_2,plain,
! [U_137,U_136] :
( ( subset(singleton(U_137),U_136)
| ~ in(U_137,U_136) )
& ( in(U_137,U_136)
| ~ subset(singleton(U_137),U_136) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_141,U_139] :
( subset(singleton(U_141),U_139)
| ~ in(U_141,U_139) )
& ! [U_140,U_138] :
( in(U_140,U_138)
| ~ subset(singleton(U_140),U_138) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( in(U_140,U_138)
| ~ subset(singleton(U_140),U_138) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_37_1,plain,
! [A,B] : subset(A,A),
inference(fof_nnf,[status(thm)],[reflexivity_r1_tarski]) ).
fof(f_37_2,plain,
! [U_160,U_159] : subset(U_160,U_160),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
! [U_160] : subset(U_160,U_160),
inference(miniscope,[status(thm)],[f_37_2]) ).
cnf(f_37_4,plain,
subset(U_160,U_160),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_47_1,plain,
! [A] : set_intersection2(A,empty_set) = empty_set,
inference(fof_nnf,[status(thm)],[t2_boole]) ).
fof(f_47_2,plain,
! [U_179] : set_intersection2(U_179,empty_set) = empty_set,
inference(variable_rename,[status(thm)],[f_47_1]) ).
cnf(f_47_3,plain,
set_intersection2(U_179,empty_set) = empty_set,
inference(clausify,[status(thm)],[f_47_2]) ).
fof(f_66_1,negated_conjecture,
~ ! [A,B] :
( subset(singleton(A),singleton(B))
=> A = B ),
inference(negate,[status(cth)],[t6_zfmisc_1]) ).
fof(f_66_2,negated_conjecture,
? [A,B] :
( A != B
& subset(singleton(A),singleton(B)) ),
inference(fof_nnf,[status(thm)],[f_66_1]) ).
fof(f_66_3,negated_conjecture,
? [U_232,U_231] :
( U_232 != U_231
& subset(singleton(U_232),singleton(U_231)) ),
inference(variable_rename,[status(thm)],[f_66_2]) ).
fof(f_66_4,negated_conjecture,
? [U_231] :
( sK21 != U_231
& subset(singleton(sK21),singleton(U_231)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_232,sK21)],[f_66_3]) ).
fof(f_66_5,negated_conjecture,
( sK21 != sK22
& subset(singleton(sK21),singleton(sK22)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_231,sK22)],[f_66_4]) ).
cnf(f_66_6,negated_conjecture,
subset(singleton(sK21),singleton(sK22)),
inference(clausify,[status(thm)],[f_66_5]) ).
cnf(f_66_7,negated_conjecture,
sK21 != sK22,
inference(clausify,[status(thm)],[f_66_5]) ).
fof(f_67_1,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(fof_nnf,[status(thm)],[t7_boole]) ).
fof(f_67_2,plain,
! [U_234,U_233] :
( ~ empty(U_233)
| ~ in(U_234,U_233) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
cnf(f_67_3,plain,
( ~ empty(U_233)
| ~ in(U_234,U_233) ),
inference(clausify,[status(thm)],[f_67_2]) ).
fof(f_69_1,plain,
! [A,B] :
( ( disjoint(A,B)
| set_difference(A,B) != A )
& ( set_difference(A,B) = A
| ~ disjoint(A,B) ) ),
inference(fof_nnf,[status(thm)],[t83_xboole_1]) ).
fof(f_69_2,plain,
! [U_238,U_237] :
( ( disjoint(U_238,U_237)
| set_difference(U_238,U_237) != U_238 )
& ( set_difference(U_238,U_237) = U_238
| ~ disjoint(U_238,U_237) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_242,U_240] :
( disjoint(U_242,U_240)
| set_difference(U_242,U_240) != U_242 )
& ! [U_241,U_239] :
( set_difference(U_241,U_239) = U_241
| ~ disjoint(U_241,U_239) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
cnf(f_69_4,plain,
( set_difference(U_241,U_239) = U_241
| ~ disjoint(U_241,U_239) ),
inference(clausify,[status(thm)],[f_69_3]) ).
cnf(t1,plain,
sK21 != sK22,
inference(start,[status(thm),parent(0:0)],[f_66_7]) ).
cnf(t2,plain,
( ~ in(sK21,set_difference(singleton(sK22),empty_set))
| set_difference(singleton(sK22),empty_set) != singleton(sK22)
| sK21 = sK22 ),
inference(extension,[status(thm),parent(t1:1)],[f_7_6]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ disjoint(singleton(sK22),empty_set)
| set_difference(singleton(sK22),empty_set) = singleton(sK22) ),
inference(extension,[status(thm),parent(t2:2)],[f_69_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( set_intersection2(singleton(sK22),empty_set) != empty_set
| disjoint(singleton(sK22),empty_set) ),
inference(extension,[status(thm),parent(t4:2)],[f_15_5]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
set_intersection2(singleton(sK22),empty_set) = empty_set,
inference(extension,[status(thm),parent(t6:2)],[f_47_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( ~ in(sK21,singleton(sK22))
| in(sK21,empty_set)
| set_difference(singleton(sK22),empty_set) != set_difference(singleton(sK22),empty_set)
| in(sK21,set_difference(singleton(sK22),empty_set)) ),
inference(extension,[status(thm),parent(t2:3)],[f_14_8]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t2:3]) ).
cnf(t12,plain,
( proper_subset(set_difference(singleton(sK22),empty_set),set_difference(singleton(sK22),empty_set))
| ~ subset(set_difference(singleton(sK22),empty_set),set_difference(singleton(sK22),empty_set))
| set_difference(singleton(sK22),empty_set) = set_difference(singleton(sK22),empty_set) ),
inference(extension,[status(thm),parent(t10:2)],[f_16_6]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
subset(set_difference(singleton(sK22),empty_set),set_difference(singleton(sK22),empty_set)),
inference(extension,[status(thm),parent(t12:2)],[f_37_4]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
~ proper_subset(set_difference(singleton(sK22),empty_set),set_difference(singleton(sK22),empty_set)),
inference(extension,[status(thm),parent(t12:3)],[f_29_4]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t12:3]) ).
cnf(t18,plain,
( ~ empty(empty_set)
| ~ in(sK21,empty_set) ),
inference(extension,[status(thm),parent(t10:3)],[f_67_3]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t10:3]) ).
cnf(t20,plain,
empty(empty_set),
inference(extension,[status(thm),parent(t18:2)],[f_24_2]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t18:2]) ).
cnf(t22,plain,
( ~ subset(singleton(sK21),singleton(sK22))
| in(sK21,singleton(sK22)) ),
inference(extension,[status(thm),parent(t10:4)],[f_31_4]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t10:4]) ).
cnf(t24,plain,
subset(singleton(sK21),singleton(sK22)),
inference(extension,[status(thm),parent(t22:2)],[f_66_6]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU148+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n013.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Sat Sep 19 23:22:23 UTC 2026
% 0.09/0.58 % CPUTime :
% 100.44/100.95 % SZS status Theorem for theBenchmark
% 100.44/100.95 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------