%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV013-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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 01:37:49 PM UTC 2026
% Result : Unsatisfiable 11.07s 1.88s
% Output : Proof 11.07s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t117,axiom,
sF2 = p_Wr(x_139),
introduced(definition) ).
cnf(f93,negated_conjecture,
p_Wr(x_139),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_4) ).
fof(f93_nnf,plain,
p_Wr(x_139),
inference(nnf_transformation,[status(thm)],[f93]) ).
cnf(c93,plain,
p_Wr(x_139),
inference(cnf_transformation,[status(esa)],[f93_nnf]) ).
cnf(t4,plain,
p_Wr(x_139) = true,
inference(equality_encoding,[status(esa)],[c93]) ).
cnf(t131,plain,
p_Wr(x_139) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t2469,plain,
sF2 = true,
inference(step,[status(thm)],[t117,t131]) ).
cnf(t141,plain,
true = sF2,
inference(orient,[status(thm)],[t2469]) ).
cnf(f34,axiom,
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_35) ).
fof(f34_nnf,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t91,plain,
ifeq(p_Wr(X1),true,ifeq(gt(fifo_length,int_level(X1)),true,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t3122,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),true,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t91,t141]) ).
cnf(t3123,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t3122,t141]) ).
cnf(t3124,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),true) = true,
inference(step,[status(thm)],[t3123,t141]) ).
cnf(t3125,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),sF2) = true,
inference(step,[status(thm)],[t3124,t141]) ).
cnf(t3126,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),sF2) = sF2,
inference(step,[status(thm)],[t3125,t141]) ).
cnf(t2006,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),sF2) = sF2,
inference(orient,[status(thm)],[t3126]) ).
cnf(f92,negated_conjecture,
~ p_Rd(x_139),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_3) ).
fof(f92_nnf,plain,
~ p_Rd(x_139),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
~ p_Rd(x_139),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c92,plain,
~ p_Rd(x_139),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(t2,plain,
p_Rd(x_139) = false,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t129,plain,
p_Rd(x_139) = false,
inference(orient,[status(thm)],[t2]) ).
cnf(t115,axiom,
sF0 = p_Rd(x_139),
introduced(definition) ).
cnf(t2460,plain,
sF0 = false,
inference(step,[status(thm)],[t115,t129]) ).
cnf(t132,plain,
false = sF0,
inference(orient,[status(thm)],[t2460]) ).
cnf(t2464,plain,
p_Rd(x_139) = sF0,
inference(step,[status(thm)],[t129,t132]) ).
cnf(t136,plain,
p_Rd(x_139) = sF0,
inference(orient,[status(thm)],[t2464]) ).
cnf(t2007,plain,
sF2 = ifeq(p_Wr(x_139),sF2,ifeq(gt(fifo_length,int_level(x_139)),sF2,or(p_Reset(x_139),or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),sF2),sF2),
inference(cp,[status(thm)],[t2006,t136]) ).
cnf(t2471,plain,
p_Wr(x_139) = sF2,
inference(step,[status(thm)],[t131,t141]) ).
cnf(t143,plain,
p_Wr(x_139) = sF2,
inference(orient,[status(thm)],[t2471]) ).
cnf(t3127,plain,
sF2 = ifeq(sF2,sF2,ifeq(gt(fifo_length,int_level(x_139)),sF2,or(p_Reset(x_139),or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),sF2),sF2),
inference(step,[status(thm)],[t2007,t143]) ).
cnf(t16,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t174,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t3128,plain,
sF2 = ifeq(gt(fifo_length,int_level(x_139)),sF2,or(p_Reset(x_139),or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),sF2),
inference(step,[status(thm)],[t3127,t174]) ).
cnf(t118,axiom,
sF3 = int_level(x_139),
introduced(definition) ).
cnf(t145,plain,
int_level(x_139) = sF3,
inference(orient,[status(thm)],[t118]) ).
cnf(t3129,plain,
sF2 = ifeq(gt(fifo_length,sF3),sF2,or(p_Reset(x_139),or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),sF2),
inference(step,[status(thm)],[t3128,t145]) ).
cnf(f91,negated_conjecture,
gt(fifo_length,level(x_139)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
gt(fifo_length,level(x_139)),
inference(nnf_transformation,[status(thm)],[f91]) ).
cnf(c91,plain,
gt(fifo_length,level(x_139)),
inference(cnf_transformation,[status(esa)],[f91_nnf]) ).
cnf(u0,axiom,
gt(fifo_length,level(x_139)) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(f20,axiom,
level(X_t_32) = int_level(X_t_32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
fof(f20_nnf,plain,
! [X_t_32] : level(X_t_32) = int_level(X_t_32),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X_t_32] : level(X_t_32) = int_level(X_t_32),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
level(X0) = int_level(X0),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(d0,axiom,
level(X0) = int_level(X0),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t13,plain,
gt(fifo_length,int_level(x_139)) = true,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t2482,plain,
gt(fifo_length,sF3) = true,
inference(step,[status(thm)],[t13,t145]) ).
cnf(t2483,plain,
gt(fifo_length,sF3) = sF2,
inference(step,[status(thm)],[t2482,t141]) ).
cnf(t156,plain,
gt(fifo_length,sF3) = sF2,
inference(orient,[status(thm)],[t2483]) ).
cnf(t3130,plain,
sF2 = ifeq(sF2,sF2,or(p_Reset(x_139),or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),sF2),
inference(step,[status(thm)],[t3129,t156]) ).
cnf(t3131,plain,
sF2 = or(p_Reset(x_139),or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),
inference(step,[status(thm)],[t3130,t174]) ).
cnf(f90,negated_conjecture,
~ p_Reset(x_139),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_1) ).
fof(f90_nnf,plain,
~ p_Reset(x_139),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
~ p_Reset(x_139),
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c90,plain,
~ p_Reset(x_139),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
cnf(t3,plain,
p_Reset(x_139) = false,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t130,plain,
p_Reset(x_139) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t2466,plain,
p_Reset(x_139) = sF0,
inference(step,[status(thm)],[t130,t132]) ).
cnf(t138,plain,
p_Reset(x_139) = sF0,
inference(orient,[status(thm)],[t2466]) ).
cnf(t3132,plain,
sF2 = or(sF0,or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)))),
inference(step,[status(thm)],[t3131,t138]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t2479,plain,
or(sF0,X1) = X1,
inference(step,[status(thm)],[t9,t132]) ).
cnf(t152,plain,
or(sF0,X1) = X1,
inference(orient,[status(thm)],[t2479]) ).
cnf(t3133,plain,
sF2 = or(sF0,eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1))),
inference(step,[status(thm)],[t3132,t152]) ).
cnf(t3134,plain,
sF2 = eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)),
inference(step,[status(thm)],[t3133,t152]) ).
cnf(t122,axiom,
sF7 = plus(x_139,n1),
introduced(definition) ).
cnf(t155,plain,
plus(x_139,n1) = sF7,
inference(orient,[status(thm)],[t122]) ).
cnf(t3135,plain,
sF2 = eq(int_level(sF7),plus(int_level(x_139),n1)),
inference(step,[status(thm)],[t3134,t155]) ).
cnf(t123,axiom,
sF8 = int_level(plus(x_139,n1)),
introduced(definition) ).
cnf(t2487,plain,
sF8 = int_level(sF7),
inference(step,[status(thm)],[t123,t155]) ).
cnf(t163,plain,
int_level(sF7) = sF8,
inference(orient,[status(thm)],[t2487]) ).
cnf(t3136,plain,
sF2 = eq(sF8,plus(int_level(x_139),n1)),
inference(step,[status(thm)],[t3135,t163]) ).
cnf(t3137,plain,
sF2 = eq(sF8,plus(sF3,n1)),
inference(step,[status(thm)],[t3136,t145]) ).
cnf(t124,axiom,
sF9 = plus(int_level(x_139),n1),
introduced(definition) ).
cnf(t2488,plain,
sF9 = plus(sF3,n1),
inference(step,[status(thm)],[t124,t145]) ).
cnf(t164,plain,
plus(sF3,n1) = sF9,
inference(orient,[status(thm)],[t2488]) ).
cnf(t3138,plain,
sF2 = eq(sF8,sF9),
inference(step,[status(thm)],[t3137,t164]) ).
cnf(f94,negated_conjecture,
level(plus(x_139,n1)) != plus(level(x_139),n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_5) ).
fof(f94_nnf,plain,
level(plus(x_139,n1)) != plus(level(x_139),n1),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
level(plus(x_139,n1)) != plus(level(x_139),n1),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
level(plus(x_139,n1)) != plus(level(x_139),n1),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(u2,axiom,
eq(level(plus(x_139,n1)),plus(level(x_139),n1)) = false,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(t28,plain,
eq(int_level(plus(x_139,n1)),plus(int_level(x_139),n1)) = false,
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(t2519,plain,
eq(int_level(sF7),plus(int_level(x_139),n1)) = false,
inference(step,[status(thm)],[t28,t155]) ).
cnf(t2520,plain,
eq(sF8,plus(int_level(x_139),n1)) = false,
inference(step,[status(thm)],[t2519,t163]) ).
cnf(t2521,plain,
eq(sF8,plus(sF3,n1)) = false,
inference(step,[status(thm)],[t2520,t145]) ).
cnf(t2522,plain,
eq(sF8,sF9) = false,
inference(step,[status(thm)],[t2521,t164]) ).
cnf(t2523,plain,
eq(sF8,sF9) = sF0,
inference(step,[status(thm)],[t2522,t132]) ).
cnf(t218,plain,
eq(sF8,sF9) = sF0,
inference(orient,[status(thm)],[t2523]) ).
cnf(t3139,plain,
sF2 = sF0,
inference(step,[status(thm)],[t3138,t218]) ).
cnf(t2011,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t3139]) ).
cnf(t3142,plain,
true = sF0,
inference(step,[status(thm)],[t141,t2011]) ).
cnf(t2014,plain,
true = sF0,
inference(orient,[status(thm)],[t3142]) ).
cnf(f0,axiom,
plus(X_0,n1) != n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f0_nnf,plain,
! [X_0] : plus(X_0,n1) != n0,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X_0] : plus(X_0,n1) != n0,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
plus(X0,n1) != n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f5,axiom,
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
fof(f5_nnf,plain,
! [Y_4,X_3] :
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [Y_4,X_3] :
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ gt(X1,X0)
| ~ def_10(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f6,axiom,
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
fof(f6_nnf,plain,
! [Y_4,X_3] :
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Y_4,X_3] :
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( X1 != X0
| ~ def_10(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f16,axiom,
~ gt(X_28,X_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_17) ).
fof(f16_nnf,plain,
! [X_28] : ~ gt(X_28,X_28),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X_28] : ~ gt(X_28,X_28),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
~ gt(X0,X0),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f28,axiom,
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
fof(f28_nnf,plain,
! [X_t_37] :
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X_t_37] :
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ~ p_Wr_error(plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(f29,axiom,
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f29_nnf,plain,
! [X_t_37] :
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X_t_37] :
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ p_Rd_error(plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f30,axiom,
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_31) ).
fof(f30_nnf,plain,
! [X_t_37,X_k1_38,X_k2_39] :
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X_t_37,X_k1_38,X_k2_39] :
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ p_Mem(X1,X2,plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f31,axiom,
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_32) ).
fof(f31_nnf,plain,
! [X_t_37,X_k1_40] :
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X_t_37,X_k1_40] :
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( ~ p_Data_out(X1,plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c5,c6,c16,c28,c29,c30,c31,c90,c92,c94]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t2014]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t132]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV013-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.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 : Wed Sep 23 16:29:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 11.07/1.88 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.07/1.88 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------