%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG039-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:37:34 PM UTC 2026
% Result : Unsatisfiable 23.46s 3.46s
% Output : Proof 23.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 16
% Syntax : Number of formulae : 164 ( 156 unt; 0 def)
% Number of atoms : 180 ( 131 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 38 ( 22 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-4 aty)
% Number of variables : 160 ( 19 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f16,axiom,
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplication_is_well_defined) ).
fof(f16_nnf,plain,
! [X,Y,U,V] :
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X,Y,U,V] :
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( X2 = X3
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t50,plain,
ifeq(product(X1,X2,X3),true,ifeq(product(X1,X2,X4),true,X3,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t61,plain,
ifeq(product(X1,X2,X3),true,ifeq(product(X1,X2,X4),true,X3,X4),X4) = X4,
inference(orient,[status(thm)],[t50]) ).
cnf(f56,axiom,
product(A,A,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f56_nnf,plain,
! [A] : product(A,A,A),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [A] : product(A,A,A),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
product(X0,X0,X0),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(t5,plain,
product(X1,X1,X1) = true,
inference(equality_encoding,[status(esa)],[c56]) ).
cnf(t71,plain,
product(X1,X1,X1) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t73,plain,
X1 = ifeq(product(X1,X1,X2),true,ifeq(true,true,X2,X1),X1),
inference(cp,[status(thm)],[t61,t71]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t60,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t2140,plain,
X1 = ifeq(product(X1,X1,X2),true,X2,X1),
inference(step,[status(thm)],[t73,t60]) ).
cnf(t1246,plain,
ifeq(product(X1,X1,X2),true,X2,X1) = X1,
inference(orient,[status(thm)],[t2140]) ).
cnf(f54,axiom,
product(add(b,a),a,add(d,a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f54_nnf,plain,
product(add(b,a),a,add(d,a)),
inference(nnf_transformation,[status(thm)],[f54]) ).
cnf(c54,plain,
product(add(b,a),a,add(d,a)),
inference(cnf_transformation,[status(esa)],[f54_nnf]) ).
cnf(t41,plain,
product(add(b,a),a,add(d,a)) = true,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t160,plain,
product(add(b,a),a,add(d,a)) = true,
inference(orient,[status(thm)],[t41]) ).
cnf(f57,negated_conjecture,
product(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_times_b) ).
fof(f57_nnf,plain,
product(a,b,c),
inference(nnf_transformation,[status(thm)],[f57]) ).
cnf(c57,plain,
product(a,b,c),
inference(cnf_transformation,[status(esa)],[f57_nnf]) ).
cnf(t6,plain,
product(a,b,c) = true,
inference(equality_encoding,[status(esa)],[c57]) ).
cnf(t111,plain,
product(a,b,c) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t112,plain,
X1 = ifeq(true,true,ifeq(product(a,b,X1),true,c,X1),X1),
inference(cp,[status(thm)],[t61,t111]) ).
cnf(t2147,plain,
X1 = ifeq(product(a,b,X1),true,c,X1),
inference(step,[status(thm)],[t112,t60]) ).
cnf(t1303,plain,
ifeq(product(a,b,X1),true,c,X1) = X1,
inference(orient,[status(thm)],[t2147]) ).
cnf(f31,axiom,
product(a,multiply(b,A),multiply(B,A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f31_nnf,plain,
! [A,B] : product(a,multiply(b,A),multiply(B,A)),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A,B] : product(a,multiply(b,A),multiply(B,A)),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
product(a,multiply(b,X0),multiply(X1,X0)),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t38,plain,
product(a,multiply(b,X1),multiply(X2,X1)) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t114,plain,
product(a,multiply(b,X1),multiply(X2,X1)) = true,
inference(orient,[status(thm)],[t38]) ).
cnf(f22,axiom,
multiply(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f22_nnf,plain,
! [A] : multiply(A,A) = A,
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A] : multiply(A,A) = A,
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
multiply(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t2,plain,
multiply(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t65,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t115,plain,
true = product(a,b,multiply(X1,b)),
inference(cp,[status(thm)],[t114,t65]) ).
cnf(t1086,plain,
product(a,b,multiply(X1,b)) = true,
inference(orient,[status(thm)],[t115]) ).
cnf(t1087,plain,
true = product(a,b,b),
inference(cp,[status(thm)],[t1086,t65]) ).
cnf(t1110,plain,
product(a,b,b) = true,
inference(orient,[status(thm)],[t1087]) ).
cnf(t1304,plain,
b = ifeq(true,true,c,b),
inference(cp,[status(thm)],[t1303,t1110]) ).
cnf(t2148,plain,
b = c,
inference(step,[status(thm)],[t1304,t60]) ).
cnf(t1307,plain,
b = c,
inference(orient,[status(thm)],[t2148]) ).
cnf(t2167,plain,
product(add(c,a),a,add(d,a)) = true,
inference(step,[status(thm)],[t160,t1307]) ).
cnf(t1322,plain,
product(add(c,a),a,add(d,a)) = true,
inference(rw,[status(thm)],[t2167]) ).
cnf(f24,axiom,
multiply(b,a) = d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f24_nnf,plain,
multiply(b,a) = d,
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
multiply(b,a) = d,
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(t4,plain,
multiply(b,a) = d,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t1058,plain,
multiply(b,a) = d,
inference(orient,[status(thm)],[t4]) ).
cnf(t1060,plain,
true = product(a,multiply(b,a),d),
inference(cp,[status(thm)],[t114,t1058]) ).
cnf(t2136,plain,
true = product(a,d,d),
inference(step,[status(thm)],[t1060,t1058]) ).
cnf(t1063,plain,
product(a,d,d) = true,
inference(orient,[status(thm)],[t2136]) ).
cnf(t1064,plain,
X1 = ifeq(true,true,ifeq(product(a,d,X1),true,d,X1),X1),
inference(cp,[status(thm)],[t61,t1063]) ).
cnf(t2205,plain,
X1 = ifeq(product(a,d,X1),true,d,X1),
inference(step,[status(thm)],[t1064,t60]) ).
cnf(t1638,plain,
ifeq(product(a,d,X1),true,d,X1) = X1,
inference(orient,[status(thm)],[t2205]) ).
cnf(t116,plain,
true = product(a,multiply(b,X1),X1),
inference(cp,[status(thm)],[t114,t65]) ).
cnf(t1133,plain,
product(a,multiply(b,X1),X1) = true,
inference(orient,[status(thm)],[t116]) ).
cnf(t1134,plain,
true = product(a,d,a),
inference(cp,[status(thm)],[t1133,t1058]) ).
cnf(t1157,plain,
product(a,d,a) = true,
inference(orient,[status(thm)],[t1134]) ).
cnf(t1641,plain,
a = ifeq(true,true,d,a),
inference(cp,[status(thm)],[t1638,t1157]) ).
cnf(t2206,plain,
a = d,
inference(step,[status(thm)],[t1641,t60]) ).
cnf(t1643,plain,
a = d,
inference(orient,[status(thm)],[t2206]) ).
cnf(t2220,plain,
product(add(c,d),a,add(d,a)) = true,
inference(step,[status(thm)],[t1322,t1643]) ).
cnf(t2221,plain,
product(add(c,d),d,add(d,a)) = true,
inference(step,[status(thm)],[t2220,t1643]) ).
cnf(t2222,plain,
product(add(c,d),d,add(d,d)) = true,
inference(step,[status(thm)],[t2221,t1643]) ).
cnf(f21,axiom,
add(A,A) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f21_nnf,plain,
! [A] : add(A,A) = additive_identity,
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A] : add(A,A) = additive_identity,
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
add(X0,X0) = additive_identity,
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t0,plain,
add(X1,X1) = additive_identity,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t1062,plain,
add(X1,X1) = additive_identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t2223,plain,
product(add(c,d),d,additive_identity) = true,
inference(step,[status(thm)],[t2222,t1062]) ).
cnf(t1796,plain,
product(add(c,d),d,additive_identity) = true,
inference(orient,[status(thm)],[t2223]) ).
cnf(f2,axiom,
product(X,Y,multiply(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_multiplication) ).
fof(f2_nnf,plain,
! [X,Y] : product(X,Y,multiply(X,Y)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : product(X,Y,multiply(X,Y)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
product(X0,X1,multiply(X0,X1)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t18,plain,
product(X1,X2,multiply(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t67,plain,
product(X1,X2,multiply(X1,X2)) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(f26,axiom,
product(a,c,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f26_nnf,plain,
product(a,c,c),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
product(a,c,c),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(t7,plain,
product(a,c,c) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t131,plain,
product(a,c,c) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t132,plain,
X1 = ifeq(true,true,ifeq(product(a,c,X1),true,c,X1),X1),
inference(cp,[status(thm)],[t61,t131]) ).
cnf(t2193,plain,
X1 = ifeq(product(a,c,X1),true,c,X1),
inference(step,[status(thm)],[t132,t60]) ).
cnf(t1578,plain,
ifeq(product(a,c,X1),true,c,X1) = X1,
inference(orient,[status(thm)],[t2193]) ).
cnf(t2160,plain,
product(a,c,multiply(X1,b)) = true,
inference(step,[status(thm)],[t1086,t1307]) ).
cnf(t2161,plain,
product(a,c,multiply(X1,c)) = true,
inference(step,[status(thm)],[t2160,t1307]) ).
cnf(t1319,plain,
product(a,c,multiply(X1,c)) = true,
inference(rw,[status(thm)],[t2161]) ).
cnf(t1437,plain,
product(a,c,multiply(X1,c)) = true,
inference(orient,[status(thm)],[t1319]) ).
cnf(t1579,plain,
multiply(X1,c) = ifeq(true,true,c,multiply(X1,c)),
inference(cp,[status(thm)],[t1578,t1437]) ).
cnf(t2194,plain,
multiply(X1,c) = c,
inference(step,[status(thm)],[t1579,t60]) ).
cnf(t1580,plain,
multiply(X1,c) = c,
inference(orient,[status(thm)],[t2194]) ).
cnf(t1581,plain,
true = product(X1,c,c),
inference(cp,[status(thm)],[t67,t1580]) ).
cnf(t1583,plain,
product(X1,c,c) = true,
inference(orient,[status(thm)],[t1581]) ).
cnf(t1584,plain,
X1 = ifeq(true,true,ifeq(product(X2,c,X1),true,c,X1),X1),
inference(cp,[status(thm)],[t61,t1583]) ).
cnf(t2234,plain,
X1 = ifeq(product(X2,c,X1),true,c,X1),
inference(step,[status(thm)],[t1584,t60]) ).
cnf(t1957,plain,
ifeq(product(X1,c,X2),true,c,X2) = X2,
inference(orient,[status(thm)],[t2234]) ).
cnf(f53,axiom,
product(add(b,a),b,add(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f53_nnf,plain,
product(add(b,a),b,add(b,c)),
inference(nnf_transformation,[status(thm)],[f53]) ).
cnf(c53,plain,
product(add(b,a),b,add(b,c)),
inference(cnf_transformation,[status(esa)],[f53_nnf]) ).
cnf(t42,plain,
product(add(b,a),b,add(b,c)) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t157,plain,
product(add(b,a),b,add(b,c)) = true,
inference(orient,[status(thm)],[t42]) ).
cnf(t2168,plain,
product(add(c,a),b,add(b,c)) = true,
inference(step,[status(thm)],[t157,t1307]) ).
cnf(t2169,plain,
product(add(c,a),c,add(b,c)) = true,
inference(step,[status(thm)],[t2168,t1307]) ).
cnf(t2170,plain,
product(add(c,a),c,add(c,c)) = true,
inference(step,[status(thm)],[t2169,t1307]) ).
cnf(t2171,plain,
product(add(c,a),c,additive_identity) = true,
inference(step,[status(thm)],[t2170,t1062]) ).
cnf(t1323,plain,
product(add(c,a),c,additive_identity) = true,
inference(rw,[status(thm)],[t2171]) ).
cnf(t1483,plain,
product(add(c,a),c,additive_identity) = true,
inference(orient,[status(thm)],[t1323]) ).
cnf(t2208,plain,
product(add(c,d),c,additive_identity) = true,
inference(step,[status(thm)],[t1483,t1643]) ).
cnf(t1645,plain,
product(add(c,d),c,additive_identity) = true,
inference(rw,[status(thm)],[t2208]) ).
cnf(t1650,plain,
product(add(c,d),c,additive_identity) = true,
inference(orient,[status(thm)],[t1645]) ).
cnf(t1958,plain,
additive_identity = ifeq(true,true,c,additive_identity),
inference(cp,[status(thm)],[t1957,t1650]) ).
cnf(t2235,plain,
additive_identity = c,
inference(step,[status(thm)],[t1958,t60]) ).
cnf(t1960,plain,
additive_identity = c,
inference(orient,[status(thm)],[t2235]) ).
cnf(t2245,plain,
product(add(c,d),d,c) = true,
inference(step,[status(thm)],[t1796,t1960]) ).
cnf(t1969,plain,
product(add(c,d),d,c) = true,
inference(rw,[status(thm)],[t2245]) ).
cnf(f15,axiom,
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addition_is_well_defined) ).
fof(f15_nnf,plain,
! [X,Y,U,V] :
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X,Y,U,V] :
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( X2 = X3
| ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t51,plain,
ifeq(sum(X1,X2,X3),true,ifeq(sum(X1,X2,X4),true,X3,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t63,plain,
ifeq(sum(X1,X2,X3),true,ifeq(sum(X1,X2,X4),true,X3,X4),X4) = X4,
inference(orient,[status(thm)],[t51]) ).
cnf(f1,axiom,
sum(X,additive_identity,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity2) ).
fof(f1_nnf,plain,
! [X] : sum(X,additive_identity,X),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : sum(X,additive_identity,X),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
sum(X0,additive_identity,X0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t13,plain,
sum(X1,additive_identity,X1) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t957,plain,
sum(X1,additive_identity,X1) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t960,plain,
X1 = ifeq(true,true,ifeq(sum(X2,additive_identity,X1),true,X2,X1),X1),
inference(cp,[status(thm)],[t63,t957]) ).
cnf(t2199,plain,
X1 = ifeq(sum(X2,additive_identity,X1),true,X2,X1),
inference(step,[status(thm)],[t960,t60]) ).
cnf(t1610,plain,
ifeq(sum(X1,additive_identity,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t2199]) ).
cnf(f25,axiom,
sum(A,B,add(B,A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f25_nnf,plain,
! [A,B] : sum(A,B,add(B,A)),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A,B] : sum(A,B,add(B,A)),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
sum(X0,X1,add(X1,X0)),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t32,plain,
sum(X1,X2,add(X2,X1)) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t875,plain,
sum(X1,X2,add(X2,X1)) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(t1611,plain,
add(additive_identity,X1) = ifeq(true,true,X1,add(additive_identity,X1)),
inference(cp,[status(thm)],[t1610,t875]) ).
cnf(t2201,plain,
add(additive_identity,X1) = X1,
inference(step,[status(thm)],[t1611,t60]) ).
cnf(t1626,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t2201]) ).
cnf(t2238,plain,
add(c,X1) = X1,
inference(step,[status(thm)],[t1626,t1960]) ).
cnf(t1963,plain,
add(c,X1) = X1,
inference(rw,[status(thm)],[t2238]) ).
cnf(t1980,plain,
add(c,X1) = X1,
inference(orient,[status(thm)],[t1963]) ).
cnf(t2256,plain,
product(d,d,c) = true,
inference(step,[status(thm)],[t1969,t1980]) ).
cnf(t2093,plain,
product(d,d,c) = true,
inference(orient,[status(thm)],[t2256]) ).
cnf(t2094,plain,
d = ifeq(true,true,c,d),
inference(cp,[status(thm)],[t1246,t2093]) ).
cnf(t2257,plain,
d = c,
inference(step,[status(thm)],[t2094,t60]) ).
cnf(t2118,plain,
c = d,
inference(orient,[status(thm)],[t2257]) ).
cnf(f59,negated_conjecture,
c != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_c_equals_d) ).
fof(f59_nnf,plain,
c != d,
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
c != d,
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
c != d,
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(goal_0,negated_conjecture,
d != c,
inference(equality_encoding,[status(esa)],[c59]) ).
cnf(g0_0,plain,
d != d,
inference(rw,[status(thm)],[goal_0,t2118]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG039-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.20/0.43 % Computer : n009.cluster.edu
% 0.20/0.43 % Model : x86_64 x86_64
% 0.20/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.43 % Memory : 8046.5625MB
% 0.20/0.43 % OS : Linux 6.8.0-71-generic
% 0.20/0.43 % CPULimit : 300
% 0.20/0.43 % WCLimit : 300
% 0.20/0.43 % DateTime : Thu Sep 24 07:55:28 UTC 2026
% 0.20/0.43 % CPUTime :
% 0.20/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.46/3.46 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.46/3.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------