%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET945+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:44:21 PM UTC 2026
% Result : Theorem 39.04s 5.79s
% Output : Proof 39.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 12
% Syntax : Number of formulae : 112 ( 87 unt; 0 def)
% Number of atoms : 205 ( 96 equ)
% Maximal formula atoms : 14 ( 1 avg)
% Number of connectives : 162 ( 69 ~; 51 |; 33 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-4 aty)
% Number of variables : 198 ( 24 sgn 53 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A,B,C] :
( C = set_intersection2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f2_nnf,plain,
! [A,B,C] :
( ( ? [D] :
( ( in(D,B)
& in(D,A)
& ~ in(D,C) )
| ( ( ~ in(D,B)
| ~ in(D,A) )
& in(D,C) ) )
| C = set_intersection2(A,B) )
& ( ! [D] :
( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [C,A,B,D] :
( ( ( in(sk0(A,B,C),B)
& in(sk0(A,B,C),A)
& ~ in(sk0(A,B,C),C) )
| ( ( ~ in(sk0(A,B,C),B)
| ~ in(sk0(A,B,C),A) )
& in(sk0(A,B,C),C) )
| C = set_intersection2(A,B) )
& ( ( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f2_nnf]) ).
cnf(c4,plain,
( ~ in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2)
| X2 != set_intersection2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t33,plain,
ifeq(X1,set_intersection2(X2,X3),ifeq(in(X4,X2),true,ifeq(in(X4,X3),true,in(X4,X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t43,plain,
ifeq(X1,set_intersection2(X2,X3),ifeq(in(X4,X2),true,ifeq(in(X4,X3),true,in(X4,X1),true),true),true) = true,
inference(orient,[status(thm)],[t33]) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t38,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t44,plain,
true = ifeq(in(X1,X2),true,ifeq(in(X1,X3),true,in(X1,set_intersection2(X2,X3)),true),true),
inference(cp,[status(thm)],[t43,t38]) ).
cnf(t173,plain,
ifeq(in(X1,X2),true,ifeq(in(X1,X3),true,in(X1,set_intersection2(X2,X3)),true),true) = true,
inference(orient,[status(thm)],[t44]) ).
cnf(c2,plain,
( in(X3,X0)
| ~ in(X3,X2)
| X2 != set_intersection2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t23,plain,
ifeq(X1,set_intersection2(X2,X3),ifeq(in(X4,X1),true,in(X4,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t49,plain,
ifeq(X1,set_intersection2(X2,X3),ifeq(in(X4,X1),true,in(X4,X2),true),true) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t50,plain,
true = ifeq(in(X1,set_intersection2(X2,X3)),true,in(X1,X2),true),
inference(cp,[status(thm)],[t49,t38]) ).
cnf(t406,plain,
ifeq(in(X1,set_intersection2(X2,X3)),true,in(X1,X2),true) = true,
inference(orient,[status(thm)],[t50]) ).
fof(f8,axiom,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f8_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( ? [C] : in(C,set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk6(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6])],[f8_nnf]) ).
cnf(c24,plain,
( in(sk6(X0,X1),set_intersection2(X0,X1))
| disjoint(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t20,plain,
or(disjoint(X1,X2),in(sk6(X1,X2),set_intersection2(X1,X2))) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t70,plain,
or(disjoint(X1,X2),in(sk6(X1,X2),set_intersection2(X1,X2))) = true,
inference(orient,[status(thm)],[t20]) ).
fof(f9,conjecture,
! [A,B] :
( ! [C] :
( in(C,A)
=> disjoint(C,B) )
=> disjoint(union(A),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t98_zfmisc_1) ).
fof(f9_neg,negated_conjecture,
~ ! [A,B] :
( ! [C] :
( in(C,A)
=> disjoint(C,B) )
=> disjoint(union(A),B) ),
inference(negated_conjecture,[status(cth)],[f9]) ).
fof(f9_nnf,plain,
? [A,B] :
( ~ disjoint(union(A),B)
& ! [C] :
( disjoint(C,B)
| ~ in(C,A) ) ),
inference(nnf_transformation,[status(thm)],[f9_neg]) ).
fof(f9_sk,plain,
! [C] :
( ~ disjoint(union(sk7),sk8)
& ( disjoint(C,sk8)
| ~ in(C,sk7) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7,sk8])],[f9_nnf]) ).
cnf(c27,plain,
~ disjoint(union(sk7),sk8),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t10,plain,
disjoint(union(sk7),sk8) = false,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t102,plain,
disjoint(union(sk7),sk8) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t106,plain,
true = or(false,in(sk6(union(sk7),sk8),set_intersection2(union(sk7),sk8))),
inference(cp,[status(thm)],[t70,t102]) ).
cnf(t7,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t41,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t7939,plain,
true = in(sk6(union(sk7),sk8),set_intersection2(union(sk7),sk8)),
inference(step,[status(thm)],[t106,t41]) ).
fof(f1,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f1_nnf,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t12,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t92,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
inference(orient,[status(thm)],[t12]) ).
cnf(t7940,plain,
true = in(sk6(union(sk7),sk8),set_intersection2(sk8,union(sk7))),
inference(step,[status(thm)],[t7939,t92]) ).
cnf(t123,plain,
in(sk6(union(sk7),sk8),set_intersection2(sk8,union(sk7))) = true,
inference(orient,[status(thm)],[t7940]) ).
cnf(t407,plain,
true = ifeq(true,true,in(sk6(union(sk7),sk8),sk8),true),
inference(cp,[status(thm)],[t406,t123]) ).
cnf(t7972,plain,
true = in(sk6(union(sk7),sk8),sk8),
inference(step,[status(thm)],[t407,t38]) ).
cnf(t421,plain,
in(sk6(union(sk7),sk8),sk8) = true,
inference(orient,[status(thm)],[t7972]) ).
cnf(t436,plain,
true = ifeq(true,true,ifeq(in(sk6(union(sk7),sk8),X1),true,in(sk6(union(sk7),sk8),set_intersection2(sk8,X1)),true),true),
inference(cp,[status(thm)],[t173,t421]) ).
cnf(t8715,plain,
true = ifeq(in(sk6(union(sk7),sk8),X1),true,in(sk6(union(sk7),sk8),set_intersection2(sk8,X1)),true),
inference(step,[status(thm)],[t436,t38]) ).
cnf(t7656,plain,
ifeq(in(sk6(union(sk7),sk8),X1),true,in(sk6(union(sk7),sk8),set_intersection2(sk8,X1)),true) = true,
inference(orient,[status(thm)],[t8715]) ).
fof(f3,axiom,
! [A,B] :
( B = union(A)
<=> ! [C] :
( in(C,B)
<=> ? [D] :
( in(D,A)
& in(C,D) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_tarski) ).
fof(f3_nnf,plain,
! [A,B] :
( ( ? [C] :
( ( ? [D] :
( in(D,A)
& in(C,D) )
& ~ in(C,B) )
| ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
& in(C,B) ) )
| B = union(A) )
& ( ! [C] :
( ( ! [D] :
( ~ in(D,A)
| ~ in(C,D) )
| in(C,B) )
& ( ? [D] :
( in(D,A)
& in(C,D) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [B,A,C,D] :
( ( ( in(sk3(A,B),A)
& in(sk2(A,B),sk3(A,B))
& ~ in(sk2(A,B),B) )
| ( ( ~ in(D,A)
| ~ in(sk2(A,B),D) )
& in(sk2(A,B),B) )
| B = union(A) )
& ( ( ( ~ in(D,A)
| ~ in(C,D)
| in(C,B) )
& ( ( in(sk1(A,B,C),A)
& in(C,sk1(A,B,C)) )
| ~ in(C,B) ) )
| B != union(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3])],[f3_nnf]) ).
cnf(c11,plain,
( in(X2,sk1(X0,X1,X2))
| ~ in(X2,X1)
| X1 != union(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t27,plain,
ifeq(X1,union(X2),ifeq(in(X3,X1),true,in(X3,sk1(X2,X1,X3)),true),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t54,plain,
ifeq(X1,union(X2),ifeq(in(X3,X1),true,in(X3,sk1(X2,X1,X3)),true),true) = true,
inference(orient,[status(thm)],[t27]) ).
cnf(t55,plain,
true = ifeq(in(X1,union(X2)),true,in(X1,sk1(X2,union(X2),X1)),true),
inference(cp,[status(thm)],[t54,t38]) ).
cnf(t891,plain,
ifeq(in(X1,union(X2)),true,in(X1,sk1(X2,union(X2),X1)),true) = true,
inference(orient,[status(thm)],[t55]) ).
cnf(c3,plain,
( in(X3,X1)
| ~ in(X3,X2)
| X2 != set_intersection2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t24,plain,
ifeq(X1,set_intersection2(X2,X3),ifeq(in(X4,X1),true,in(X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t46,plain,
ifeq(X1,set_intersection2(X2,X3),ifeq(in(X4,X1),true,in(X4,X3),true),true) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t47,plain,
true = ifeq(in(X1,set_intersection2(X2,X3)),true,in(X1,X3),true),
inference(cp,[status(thm)],[t46,t38]) ).
cnf(t233,plain,
ifeq(in(X1,set_intersection2(X2,X3)),true,in(X1,X3),true) = true,
inference(orient,[status(thm)],[t47]) ).
cnf(t234,plain,
true = ifeq(true,true,in(sk6(union(sk7),sk8),union(sk7)),true),
inference(cp,[status(thm)],[t233,t123]) ).
cnf(t7955,plain,
true = in(sk6(union(sk7),sk8),union(sk7)),
inference(step,[status(thm)],[t234,t38]) ).
cnf(t246,plain,
in(sk6(union(sk7),sk8),union(sk7)) = true,
inference(orient,[status(thm)],[t7955]) ).
cnf(t893,plain,
true = ifeq(true,true,in(sk6(union(sk7),sk8),sk1(sk7,union(sk7),sk6(union(sk7),sk8))),true),
inference(cp,[status(thm)],[t891,t246]) ).
cnf(t8059,plain,
true = in(sk6(union(sk7),sk8),sk1(sk7,union(sk7),sk6(union(sk7),sk8))),
inference(step,[status(thm)],[t893,t38]) ).
cnf(t918,plain,
in(sk6(union(sk7),sk8),sk1(sk7,union(sk7),sk6(union(sk7),sk8))) = true,
inference(orient,[status(thm)],[t8059]) ).
cnf(t7658,plain,
true = ifeq(true,true,in(sk6(union(sk7),sk8),set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8)))),true),
inference(cp,[status(thm)],[t7656,t918]) ).
cnf(t8716,plain,
true = in(sk6(union(sk7),sk8),set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8)))),
inference(step,[status(thm)],[t7658,t38]) ).
cnf(t14,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t91,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t14]) ).
cnf(c25,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t21,plain,
or(not(in(X1,set_intersection2(X2,X3))),not(disjoint(X2,X3))) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t79,plain,
or(not(in(X1,set_intersection2(X2,X3))),not(disjoint(X2,X3))) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(t96,plain,
true = or(not(in(X1,set_intersection2(X2,X3))),not(disjoint(X3,X2))),
inference(cp,[status(thm)],[t79,t92]) ).
cnf(t573,plain,
or(not(in(X1,set_intersection2(X2,X3))),not(disjoint(X3,X2))) = true,
inference(orient,[status(thm)],[t96]) ).
cnf(c26,plain,
( disjoint(X2,sk8)
| ~ in(X2,sk7) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t18,plain,
ifeq(in(X1,sk7),true,disjoint(X1,sk8),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t61,plain,
ifeq(in(X1,sk7),true,disjoint(X1,sk8),true) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(c12,plain,
( in(sk1(X0,X1,X2),X0)
| ~ in(X2,X1)
| X1 != union(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t28,plain,
ifeq(X1,union(X2),ifeq(in(X3,X1),true,in(sk1(X2,X1,X3),X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t56,plain,
ifeq(X1,union(X2),ifeq(in(X3,X1),true,in(sk1(X2,X1,X3),X2),true),true) = true,
inference(orient,[status(thm)],[t28]) ).
cnf(t57,plain,
true = ifeq(in(X1,union(X2)),true,in(sk1(X2,union(X2),X1),X2),true),
inference(cp,[status(thm)],[t56,t38]) ).
cnf(t992,plain,
ifeq(in(X1,union(X2)),true,in(sk1(X2,union(X2),X1),X2),true) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(t994,plain,
true = ifeq(true,true,in(sk1(sk7,union(sk7),sk6(union(sk7),sk8)),sk7),true),
inference(cp,[status(thm)],[t992,t246]) ).
cnf(t8068,plain,
true = in(sk1(sk7,union(sk7),sk6(union(sk7),sk8)),sk7),
inference(step,[status(thm)],[t994,t38]) ).
cnf(t998,plain,
in(sk1(sk7,union(sk7),sk6(union(sk7),sk8)),sk7) = true,
inference(orient,[status(thm)],[t8068]) ).
cnf(t999,plain,
true = ifeq(true,true,disjoint(sk1(sk7,union(sk7),sk6(union(sk7),sk8)),sk8),true),
inference(cp,[status(thm)],[t61,t998]) ).
cnf(t8093,plain,
true = disjoint(sk1(sk7,union(sk7),sk6(union(sk7),sk8)),sk8),
inference(step,[status(thm)],[t999,t38]) ).
cnf(t1232,plain,
disjoint(sk1(sk7,union(sk7),sk6(union(sk7),sk8)),sk8) = true,
inference(orient,[status(thm)],[t8093]) ).
cnf(t1236,plain,
true = or(not(in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8))))),not(true)),
inference(cp,[status(thm)],[t573,t1232]) ).
cnf(t3,plain,
not(true) = false,
introduced(definition) ).
cnf(t109,plain,
not(true) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t8121,plain,
true = or(not(in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8))))),false),
inference(step,[status(thm)],[t1236,t109]) ).
cnf(t5,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t40,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t8122,plain,
true = not(in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8))))),
inference(step,[status(thm)],[t8121,t40]) ).
cnf(t1450,plain,
not(in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8))))) = true,
inference(orient,[status(thm)],[t8122]) ).
cnf(t1451,plain,
false = ifeq(true,true,in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8)))),false),
inference(cp,[status(thm)],[t91,t1450]) ).
cnf(t8126,plain,
false = in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8)))),
inference(step,[status(thm)],[t1451,t38]) ).
cnf(t1456,plain,
in(X1,set_intersection2(sk8,sk1(sk7,union(sk7),sk6(union(sk7),sk8)))) = false,
inference(orient,[status(thm)],[t8126]) ).
cnf(t8717,plain,
true = false,
inference(step,[status(thm)],[t8716,t1456]) ).
cnf(t7676,plain,
false = true,
inference(orient,[status(thm)],[t8717]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f6,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f6_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
~ empty(sk5),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f6_nnf]) ).
cnf(c22,plain,
~ empty(sk5),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c22,c25,c27]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t7676]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET945+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n013.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 12:25:06 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 39.04/5.79 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 39.04/5.79 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------