%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PUZ046-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:02:46 PM UTC 2026
% Result : Satisfiable 1.25s 1.70s
% Output : Saturation 1.25s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(b_up,axiom,
( state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X1)),X2),e2(s(s(X1)),s(X2)))
| ~ state(bb(s(X1),X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(X1,s(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',b_up) ).
cnf(b_left,axiom,
( state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,s(s(X2))),e2(s(X1),s(s(X2))))
| ~ state(bb(X1,s(X2)),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(s(X1),X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',b_left) ).
cnf(v1_left,axiom,
( state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,s(X3)),e2(s(X2),s(X3)))
| ~ state(X1,v1(X2,s(X3)),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),e2(s(X2),X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v1_left) ).
cnf(v2_left,axiom,
( state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,s(X4)),e2(s(X3),s(X4)))
| ~ state(X1,X2,v2(X3,s(X4)),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),e2(s(X3),X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v2_left) ).
cnf(v3_left,axiom,
( state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(X4,s(X5)),e2(s(X4),s(X5)))
| ~ state(X1,X2,X3,v3(X4,s(X5)),X6,X7,X8,X9,X10,X11,e1(X4,X5),e2(s(X4),X5)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v3_left) ).
cnf(b_down,axiom,
( state(bb(s(X1),X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(X1,s(X2)))
| ~ state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X1)),X2),e2(s(s(X1)),s(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',b_down) ).
cnf(b_right,axiom,
( state(bb(X1,s(X2)),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(s(X1),X2))
| ~ state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,s(s(X2))),e2(s(X1),s(s(X2)))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',b_right) ).
cnf(v1_right,axiom,
( state(X1,v1(X2,s(X3)),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),e2(s(X2),X3))
| ~ state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,s(X3)),e2(s(X2),s(X3))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v1_right) ).
cnf(v2_right,axiom,
( state(X1,X2,v2(X3,s(X4)),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),e2(s(X3),X4))
| ~ state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,s(X4)),e2(s(X3),s(X4))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v2_right) ).
cnf(v4_left,axiom,
( state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(X5,s(X6)),e2(s(X5),s(X6)))
| ~ state(X1,X2,X3,X4,v4(X5,s(X6)),X7,X8,X9,X10,X11,e1(X5,X6),e2(s(X5),X6)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v4_left) ).
cnf(h_up,axiom,
( state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(s(X6),X7),e2(s(X6),s(X7)))
| ~ state(X1,X2,X3,X4,X5,h(s(X6),X7),X8,X9,X10,X11,e1(X6,X7),e2(X6,s(X7))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',h_up) ).
cnf(v3_right,axiom,
( state(X1,X2,X3,v3(X4,s(X5)),X6,X7,X8,X9,X10,X11,e1(X4,X5),e2(s(X4),X5))
| ~ state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(X4,s(X5)),e2(s(X4),s(X5))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v3_right) ).
cnf(v4_right,axiom,
( state(X1,X2,X3,X4,v4(X5,s(X6)),X7,X8,X9,X10,X11,e1(X5,X6),e2(s(X5),X6))
| ~ state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(X5,s(X6)),e2(s(X5),s(X6))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v4_right) ).
cnf(h_down,axiom,
( state(X1,X2,X3,X4,X5,h(s(X6),X7),X8,X9,X10,X11,e1(X6,X7),e2(X6,s(X7)))
| ~ state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(s(X6),X7),e2(s(X6),s(X7))) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',h_down) ).
cnf(v1_up,axiom,
( state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X2)),X3),X12)
| ~ state(X1,v1(s(X2),X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v1_up) ).
cnf(v2_up,axiom,
( state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(s(s(X3)),X4),X12)
| ~ state(X1,X2,v2(s(X3),X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v2_up) ).
cnf(v3_up,axiom,
( state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(s(s(X4)),X5),X12)
| ~ state(X1,X2,X3,v3(s(X4),X5),X6,X7,X8,X9,X10,X11,e1(X4,X5),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v3_up) ).
cnf(v4_up,axiom,
( state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(s(s(X5)),X6),X12)
| ~ state(X1,X2,X3,X4,v4(s(X5),X6),X7,X8,X9,X10,X11,e1(X5,X6),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v4_up) ).
cnf(h_left,axiom,
( state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(X6,s(s(X7))),X12)
| ~ state(X1,X2,X3,X4,X5,h(X6,s(X7)),X8,X9,X10,X11,e1(X6,X7),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',h_left) ).
cnf(s1_down,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(s(X7),X8),X9,X10,X11,e1(X7,X8),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(s(X7),X8),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_down) ).
cnf(s1_right,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(X7,s(X8)),X9,X10,X11,e1(X7,X8),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(X7,s(X8)),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_right) ).
cnf(s2_down,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(s(X8),X9),X10,X11,e1(X8,X9),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(s(X8),X9),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s2_down) ).
cnf(s2_right,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(X8,s(X9)),X10,X11,e1(X8,X9),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(X8,s(X9)),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s2_right) ).
cnf(s3_down,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(s(X9),X10),X11,e1(X9,X10),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(s(X9),X10),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s3_down) ).
cnf(s3_right,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,s(X10)),X11,e1(X9,X10),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(X9,s(X10)),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s3_right) ).
cnf(v1_down,axiom,
( state(X1,v1(s(X2),X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),X12)
| ~ state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X2)),X3),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v1_down) ).
cnf(s4_down,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(s(X10),X11),e1(X10,X11),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(s(X10),X11),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s4_down) ).
cnf(v2_down,axiom,
( state(X1,X2,v2(s(X3),X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),X12)
| ~ state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(s(s(X3)),X4),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v2_down) ).
cnf(v3_down,axiom,
( state(X1,X2,X3,v3(s(X4),X5),X6,X7,X8,X9,X10,X11,e1(X4,X5),X12)
| ~ state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(s(s(X4)),X5),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v3_down) ).
cnf(v4_down,axiom,
( state(X1,X2,X3,X4,v4(s(X5),X6),X7,X8,X9,X10,X11,e1(X5,X6),X12)
| ~ state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(s(s(X5)),X6),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',v4_down) ).
cnf(h_right,axiom,
( state(X1,X2,X3,X4,X5,h(X6,s(X7)),X8,X9,X10,X11,e1(X6,X7),X12)
| ~ state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(X6,s(s(X7))),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',h_right) ).
cnf(s4_right,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,s(X11)),e1(X10,X11),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(X10,s(X11)),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s4_right) ).
cnf(swap_blanks,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,e1(X13,X14),e2(X11,X12))
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,e1(X11,X12),e2(X13,X14)) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',swap_blanks) ).
cnf(s1_up,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(s(X7),X8),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(s(X7),X8),X9,X10,X11,e1(X7,X8),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_up) ).
cnf(s1_left,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(X7,s(X8)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(X7,s(X8)),X9,X10,X11,e1(X7,X8),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s1_left) ).
cnf(s2_up,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(s(X8),X9),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(s(X8),X9),X10,X11,e1(X8,X9),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s2_up) ).
cnf(s2_left,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(X8,s(X9)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(X8,s(X9)),X10,X11,e1(X8,X9),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s2_left) ).
cnf(s3_up,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(s(X9),X10),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(s(X9),X10),X11,e1(X9,X10),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s3_up) ).
cnf(s3_left,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(X9,s(X10)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,s(X10)),X11,e1(X9,X10),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s3_left) ).
cnf(s4_up,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(s(X10),X11),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(s(X10),X11),e1(X10,X11),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s4_up) ).
cnf(s4_left,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(X10,s(X11)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,s(X11)),e1(X10,X11),X12) ),
file('/export/starexec/sandbox/benchmark/Axioms/PUZ004-0.ax',s4_left) ).
cnf(c_0_41,axiom,
( state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X1)),X2),e2(s(s(X1)),s(X2)))
| ~ state(bb(s(X1),X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(X1,s(X2))) ),
b_up,
[final] ).
cnf(c_0_42,axiom,
( state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,s(s(X2))),e2(s(X1),s(s(X2))))
| ~ state(bb(X1,s(X2)),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(s(X1),X2)) ),
b_left,
[final] ).
cnf(c_0_43,axiom,
( state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,s(X3)),e2(s(X2),s(X3)))
| ~ state(X1,v1(X2,s(X3)),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),e2(s(X2),X3)) ),
v1_left,
[final] ).
cnf(c_0_44,axiom,
( state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,s(X4)),e2(s(X3),s(X4)))
| ~ state(X1,X2,v2(X3,s(X4)),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),e2(s(X3),X4)) ),
v2_left,
[final] ).
cnf(c_0_45,axiom,
( state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(X4,s(X5)),e2(s(X4),s(X5)))
| ~ state(X1,X2,X3,v3(X4,s(X5)),X6,X7,X8,X9,X10,X11,e1(X4,X5),e2(s(X4),X5)) ),
v3_left,
[final] ).
cnf(c_0_46,axiom,
( state(bb(s(X1),X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(X1,s(X2)))
| ~ state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X1)),X2),e2(s(s(X1)),s(X2))) ),
b_down,
[final] ).
cnf(c_0_47,axiom,
( state(bb(X1,s(X2)),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,X2),e2(s(X1),X2))
| ~ state(bb(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,X11,e1(X1,s(s(X2))),e2(s(X1),s(s(X2)))) ),
b_right,
[final] ).
cnf(c_0_48,axiom,
( state(X1,v1(X2,s(X3)),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),e2(s(X2),X3))
| ~ state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,s(X3)),e2(s(X2),s(X3))) ),
v1_right,
[final] ).
cnf(c_0_49,axiom,
( state(X1,X2,v2(X3,s(X4)),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),e2(s(X3),X4))
| ~ state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,s(X4)),e2(s(X3),s(X4))) ),
v2_right,
[final] ).
cnf(c_0_50,axiom,
( state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(X5,s(X6)),e2(s(X5),s(X6)))
| ~ state(X1,X2,X3,X4,v4(X5,s(X6)),X7,X8,X9,X10,X11,e1(X5,X6),e2(s(X5),X6)) ),
v4_left,
[final] ).
cnf(c_0_51,axiom,
( state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(s(X6),X7),e2(s(X6),s(X7)))
| ~ state(X1,X2,X3,X4,X5,h(s(X6),X7),X8,X9,X10,X11,e1(X6,X7),e2(X6,s(X7))) ),
h_up,
[final] ).
cnf(c_0_52,axiom,
( state(X1,X2,X3,v3(X4,s(X5)),X6,X7,X8,X9,X10,X11,e1(X4,X5),e2(s(X4),X5))
| ~ state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(X4,s(X5)),e2(s(X4),s(X5))) ),
v3_right,
[final] ).
cnf(c_0_53,axiom,
( state(X1,X2,X3,X4,v4(X5,s(X6)),X7,X8,X9,X10,X11,e1(X5,X6),e2(s(X5),X6))
| ~ state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(X5,s(X6)),e2(s(X5),s(X6))) ),
v4_right,
[final] ).
cnf(c_0_54,axiom,
( state(X1,X2,X3,X4,X5,h(s(X6),X7),X8,X9,X10,X11,e1(X6,X7),e2(X6,s(X7)))
| ~ state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(s(X6),X7),e2(s(X6),s(X7))) ),
h_down,
[final] ).
cnf(c_0_55,axiom,
( state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X2)),X3),X12)
| ~ state(X1,v1(s(X2),X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),X12) ),
v1_up,
[final] ).
cnf(c_0_56,axiom,
( state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(s(s(X3)),X4),X12)
| ~ state(X1,X2,v2(s(X3),X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),X12) ),
v2_up,
[final] ).
cnf(c_0_57,axiom,
( state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(s(s(X4)),X5),X12)
| ~ state(X1,X2,X3,v3(s(X4),X5),X6,X7,X8,X9,X10,X11,e1(X4,X5),X12) ),
v3_up,
[final] ).
cnf(c_0_58,axiom,
( state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(s(s(X5)),X6),X12)
| ~ state(X1,X2,X3,X4,v4(s(X5),X6),X7,X8,X9,X10,X11,e1(X5,X6),X12) ),
v4_up,
[final] ).
cnf(c_0_59,axiom,
( state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(X6,s(s(X7))),X12)
| ~ state(X1,X2,X3,X4,X5,h(X6,s(X7)),X8,X9,X10,X11,e1(X6,X7),X12) ),
h_left,
[final] ).
cnf(c_0_60,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(s(X7),X8),X9,X10,X11,e1(X7,X8),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(s(X7),X8),X12) ),
s1_down,
[final] ).
cnf(c_0_61,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(X7,s(X8)),X9,X10,X11,e1(X7,X8),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(X7,s(X8)),X12) ),
s1_right,
[final] ).
cnf(c_0_62,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(s(X8),X9),X10,X11,e1(X8,X9),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(s(X8),X9),X12) ),
s2_down,
[final] ).
cnf(c_0_63,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(X8,s(X9)),X10,X11,e1(X8,X9),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(X8,s(X9)),X12) ),
s2_right,
[final] ).
cnf(c_0_64,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(s(X9),X10),X11,e1(X9,X10),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(s(X9),X10),X12) ),
s3_down,
[final] ).
cnf(c_0_65,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,s(X10)),X11,e1(X9,X10),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(X9,s(X10)),X12) ),
s3_right,
[final] ).
cnf(c_0_66,axiom,
( state(X1,v1(s(X2),X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(X2,X3),X12)
| ~ state(X1,v1(X2,X3),X4,X5,X6,X7,X8,X9,X10,X11,e1(s(s(X2)),X3),X12) ),
v1_down,
[final] ).
cnf(c_0_67,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(s(X10),X11),e1(X10,X11),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(s(X10),X11),X12) ),
s4_down,
[final] ).
cnf(c_0_68,axiom,
( state(X1,X2,v2(s(X3),X4),X5,X6,X7,X8,X9,X10,X11,e1(X3,X4),X12)
| ~ state(X1,X2,v2(X3,X4),X5,X6,X7,X8,X9,X10,X11,e1(s(s(X3)),X4),X12) ),
v2_down,
[final] ).
cnf(c_0_69,axiom,
( state(X1,X2,X3,v3(s(X4),X5),X6,X7,X8,X9,X10,X11,e1(X4,X5),X12)
| ~ state(X1,X2,X3,v3(X4,X5),X6,X7,X8,X9,X10,X11,e1(s(s(X4)),X5),X12) ),
v3_down,
[final] ).
cnf(c_0_70,axiom,
( state(X1,X2,X3,X4,v4(s(X5),X6),X7,X8,X9,X10,X11,e1(X5,X6),X12)
| ~ state(X1,X2,X3,X4,v4(X5,X6),X7,X8,X9,X10,X11,e1(s(s(X5)),X6),X12) ),
v4_down,
[final] ).
cnf(c_0_71,axiom,
( state(X1,X2,X3,X4,X5,h(X6,s(X7)),X8,X9,X10,X11,e1(X6,X7),X12)
| ~ state(X1,X2,X3,X4,X5,h(X6,X7),X8,X9,X10,X11,e1(X6,s(s(X7))),X12) ),
h_right,
[final] ).
cnf(c_0_72,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,s(X11)),e1(X10,X11),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(X10,s(X11)),X12) ),
s4_right,
[final] ).
cnf(c_0_73,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,e1(X13,X14),e2(X11,X12))
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,e1(X11,X12),e2(X13,X14)) ),
swap_blanks,
[final] ).
cnf(c_0_74,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(s(X7),X8),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(s(X7),X8),X9,X10,X11,e1(X7,X8),X12) ),
s1_up,
[final] ).
cnf(c_0_75,axiom,
( state(X1,X2,X3,X4,X5,X6,s1(X7,X8),X9,X10,X11,e1(X7,s(X8)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,s1(X7,s(X8)),X9,X10,X11,e1(X7,X8),X12) ),
s1_left,
[final] ).
cnf(c_0_76,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(s(X8),X9),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(s(X8),X9),X10,X11,e1(X8,X9),X12) ),
s2_up,
[final] ).
cnf(c_0_77,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,s2(X8,X9),X10,X11,e1(X8,s(X9)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,s2(X8,s(X9)),X10,X11,e1(X8,X9),X12) ),
s2_left,
[final] ).
cnf(c_0_78,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(s(X9),X10),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(s(X9),X10),X11,e1(X9,X10),X12) ),
s3_up,
[final] ).
cnf(c_0_79,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,X10),X11,e1(X9,s(X10)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,s3(X9,s(X10)),X11,e1(X9,X10),X12) ),
s3_left,
[final] ).
cnf(c_0_80,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(s(X10),X11),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(s(X10),X11),e1(X10,X11),X12) ),
s4_up,
[final] ).
cnf(c_0_81,axiom,
( state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,X11),e1(X10,s(X11)),X12)
| ~ state(X1,X2,X3,X4,X5,X6,X7,X8,X9,s4(X10,s(X11)),e1(X10,X11),X12) ),
s4_left,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ046-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.31 % Computer : n027.cluster.edu
% 0.15/0.31 % Model : x86_64 x86_64
% 0.15/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.31 % Memory : 8042.1875MB
% 0.15/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.31 % CPULimit : 300
% 0.15/0.31 % WCLimit : 300
% 0.15/0.31 % DateTime : Tue May 5 01:34:05 EDT 2026
% 0.15/0.31 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 1.25/1.70 % Version : CSE_E---1.7
% 1.25/1.70 % Problem : theBenchmark.p
% 1.25/1.70 % SZS status Satisfiable for theBenchmark.p
% 1.25/1.70 % SZS output start Saturation
% See solution above
% 1.25/1.70 % Total time : 1.372s
%------------------------------------------------------------------------------