%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 03:32:05 PM UTC 2026
% Result : Unsatisfiable 62.31s 8.43s
% Output : Proof 62.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 19
% Syntax : Number of formulae : 201 ( 193 unt; 0 def)
% Number of atoms : 209 ( 208 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-5 aty)
% Number of variables : 521 ( 47 sgn 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f23,negated_conjecture,
eq3(prop_merge_comm(X,Y,Z),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f23_nnf,plain,
! [X,Y,Z] : eq3(prop_merge_comm(X,Y,Z),bfalse) != btrue,
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X,Y,Z] : eq3(prop_merge_comm(X,Y,Z),bfalse) != btrue,
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
eq3(prop_merge_comm(X0,X1,X2),bfalse) != btrue,
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t21,plain,
eqq(eq3(prop_merge_comm(X1,X2,X3),bfalse),btrue) = efalse,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t125,plain,
eqq(eq3(prop_merge_comm(X1,X2,X3),bfalse),btrue) = efalse,
inference(orient,[status(thm)],[t21]) ).
cnf(f10,axiom,
prop_merge_comm(X,Y,Z) = impl(eq(merge(X,Y),merge(Y,X)),impl(eq(merge(X,Z),merge(Z,X)),eq(merge(Y,Z),merge(Z,Y)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_010) ).
fof(f10_nnf,plain,
! [X,Y,Z] : prop_merge_comm(X,Y,Z) = impl(eq(merge(X,Y),merge(Y,X)),impl(eq(merge(X,Z),merge(Z,X)),eq(merge(Y,Z),merge(Z,Y)))),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y,Z] : prop_merge_comm(X,Y,Z) = impl(eq(merge(X,Y),merge(Y,X)),impl(eq(merge(X,Z),merge(Z,X)),eq(merge(Y,Z),merge(Z,Y)))),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
prop_merge_comm(X0,X1,X2) = impl(eq(merge(X0,X1),merge(X1,X0)),impl(eq(merge(X0,X2),merge(X2,X0)),eq(merge(X1,X2),merge(X2,X1)))),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t28,plain,
impl(eq(merge(X1,X2),merge(X2,X1)),impl(eq(merge(X1,X3),merge(X3,X1)),eq(merge(X2,X3),merge(X3,X2)))) = prop_merge_comm(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t108,plain,
impl(eq(merge(X1,X2),merge(X2,X1)),impl(eq(merge(X1,X3),merge(X3,X1)),eq(merge(X2,X3),merge(X3,X2)))) = prop_merge_comm(X1,X2,X3),
inference(orient,[status(thm)],[t28]) ).
cnf(f5,axiom,
merge(nil,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
fof(f5_nnf,plain,
! [Y] : merge(nil,Y) = Y,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [Y] : merge(nil,Y) = Y,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
merge(nil,X0) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t9,plain,
merge(nil,X1) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t29,plain,
merge(nil,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t110,plain,
prop_merge_comm(nil,X1,X2) = impl(eq(X1,merge(X1,nil)),impl(eq(merge(nil,X2),merge(X2,nil)),eq(merge(X1,X2),merge(X2,X1)))),
inference(cp,[status(thm)],[t108,t29]) ).
cnf(t33684,plain,
prop_merge_comm(nil,X1,X2) = impl(eq(X1,merge(X1,nil)),impl(eq(X2,merge(X2,nil)),eq(merge(X1,X2),merge(X2,X1)))),
inference(step,[status(thm)],[t110,t29]) ).
cnf(t7924,plain,
impl(eq(X1,merge(X1,nil)),impl(eq(X2,merge(X2,nil)),eq(merge(X1,X2),merge(X2,X1)))) = prop_merge_comm(nil,X1,X2),
inference(orient,[status(thm)],[t33684]) ).
cnf(f7,axiom,
merge(cons(Z,Xs),cons(Y2,Ys)) = aux(Z,Xs,Y2,Ys,leqNat(Z,Y2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
fof(f7_nnf,plain,
! [Z,Xs,Y2,Ys] : merge(cons(Z,Xs),cons(Y2,Ys)) = aux(Z,Xs,Y2,Ys,leqNat(Z,Y2)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Z,Xs,Y2,Ys] : merge(cons(Z,Xs),cons(Y2,Ys)) = aux(Z,Xs,Y2,Ys,leqNat(Z,Y2)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
merge(cons(X0,X1),cons(X2,X3)) = aux(X0,X1,X2,X3,leqNat(X0,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t26,plain,
aux(X1,X2,X3,X4,leqNat(X1,X3)) = merge(cons(X1,X2),cons(X3,X4)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t100,plain,
aux(X1,X2,X3,X4,leqNat(X1,X3)) = merge(cons(X1,X2),cons(X3,X4)),
inference(orient,[status(thm)],[t26]) ).
cnf(f2,axiom,
leqNat(z,Y) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_002) ).
fof(f2_nnf,plain,
! [Y] : leqNat(z,Y) = btrue,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Y] : leqNat(z,Y) = btrue,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
leqNat(z,X0) = btrue,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t8,plain,
leqNat(z,X1) = btrue,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t97,plain,
leqNat(z,X1) = btrue,
inference(orient,[status(thm)],[t8]) ).
cnf(t102,plain,
merge(cons(z,X1),cons(X2,X3)) = aux(z,X1,X2,X3,btrue),
inference(cp,[status(thm)],[t100,t97]) ).
cnf(t151,plain,
merge(cons(z,X1),cons(X2,X3)) = aux(z,X1,X2,X3,btrue),
inference(orient,[status(thm)],[t102]) ).
cnf(t7952,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(eq(cons(z,X1),merge(cons(z,X1),nil)),impl(eq(cons(X2,X3),merge(cons(X2,X3),nil)),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1))))),
inference(cp,[status(thm)],[t7924,t151]) ).
cnf(f6,axiom,
merge(cons(Z,Xs),nil) = cons(Z,Xs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
fof(f6_nnf,plain,
! [Z,Xs] : merge(cons(Z,Xs),nil) = cons(Z,Xs),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Z,Xs] : merge(cons(Z,Xs),nil) = cons(Z,Xs),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
merge(cons(X0,X1),nil) = cons(X0,X1),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t18,plain,
merge(cons(X1,X2),nil) = cons(X1,X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t32,plain,
merge(cons(X1,X2),nil) = cons(X1,X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t33834,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(eq(cons(z,X1),cons(z,X1)),impl(eq(cons(X2,X3),merge(cons(X2,X3),nil)),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1))))),
inference(step,[status(thm)],[t7952,t32]) ).
cnf(f20,axiom,
( eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2)
| eq2(X,Z) != btrue ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
fof(f20_nnf,plain,
! [X,Z,Y,X2] :
( eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2)
| eq2(X,Z) != btrue ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,Z,Y,X2] :
( eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2)
| eq2(X,Z) != btrue ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( eq(cons(X0,X2),cons(X1,X3)) = eq(X2,X3)
| eq2(X0,X1) != btrue ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi19,axiom,
ifeq(eq2(X0,X1),btrue,eq(cons(X0,X2),cons(X1,X3)),eq(X2,X3)) = eq(X2,X3),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(f17,axiom,
eq2(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_017) ).
fof(f17_nnf,plain,
! [X] : eq2(X,X) = btrue,
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X] : eq2(X,X) = btrue,
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
eq2(X0,X0) = btrue,
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi16,axiom,
eq2(X0,X0) = btrue,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t22,plain,
eq(cons(X1,X2),cons(X1,X3)) = eq(X2,X3),
inference(hyper_resolution,[status(thm)],[hi19,hi16]) ).
cnf(t70,plain,
eq(cons(X1,X2),cons(X1,X3)) = eq(X2,X3),
inference(orient,[status(thm)],[t22]) ).
cnf(t33835,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(eq(X1,X1),impl(eq(cons(X2,X3),merge(cons(X2,X3),nil)),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1))))),
inference(step,[status(thm)],[t33834,t70]) ).
cnf(f16,axiom,
eq(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(f16_nnf,plain,
! [X] : eq(X,X) = btrue,
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X] : eq(X,X) = btrue,
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
eq(X0,X0) = btrue,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t0,plain,
eq(X1,X1) = btrue,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t91,plain,
eq(X1,X1) = btrue,
inference(orient,[status(thm)],[t0]) ).
cnf(t33836,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(btrue,impl(eq(cons(X2,X3),merge(cons(X2,X3),nil)),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1))))),
inference(step,[status(thm)],[t33835,t91]) ).
cnf(f8,axiom,
impl(btrue,Q) = Q,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
fof(f8_nnf,plain,
! [Q] : impl(btrue,Q) = Q,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [Q] : impl(btrue,Q) = Q,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
impl(btrue,X0) = X0,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t7,plain,
impl(btrue,X1) = X1,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t30,plain,
impl(btrue,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t33837,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(eq(cons(X2,X3),merge(cons(X2,X3),nil)),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1)))),
inference(step,[status(thm)],[t33836,t30]) ).
cnf(t33838,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(eq(cons(X2,X3),cons(X2,X3)),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1)))),
inference(step,[status(thm)],[t33837,t32]) ).
cnf(t33839,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(eq(X3,X3),eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1)))),
inference(step,[status(thm)],[t33838,t70]) ).
cnf(t33840,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = impl(btrue,eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1)))),
inference(step,[status(thm)],[t33839,t91]) ).
cnf(t33841,plain,
prop_merge_comm(nil,cons(z,X1),cons(X2,X3)) = eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1))),
inference(step,[status(thm)],[t33840,t30]) ).
cnf(t9428,plain,
eq(aux(z,X1,X2,X3,btrue),merge(cons(X2,X3),cons(z,X1))) = prop_merge_comm(nil,cons(z,X1),cons(X2,X3)),
inference(orient,[status(thm)],[t33841]) ).
cnf(t9467,plain,
prop_merge_comm(nil,cons(z,X1),cons(z,X2)) = eq(aux(z,X1,z,X2,btrue),aux(z,X2,z,X1,btrue)),
inference(cp,[status(thm)],[t9428,t151]) ).
cnf(f0,axiom,
aux(Z,Xs,Y2,Ys,btrue) = cons(Z,merge(Xs,cons(Y2,Ys))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom) ).
fof(f0_nnf,plain,
! [Z,Xs,Y2,Ys] : aux(Z,Xs,Y2,Ys,btrue) = cons(Z,merge(Xs,cons(Y2,Ys))),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [Z,Xs,Y2,Ys] : aux(Z,Xs,Y2,Ys,btrue) = cons(Z,merge(Xs,cons(Y2,Ys))),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
aux(X0,X1,X2,X3,btrue) = cons(X0,merge(X1,cons(X2,X3))),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t23,plain,
cons(X1,merge(X2,cons(X3,X4))) = aux(X1,X2,X3,X4,btrue),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t33,plain,
cons(X1,merge(X2,cons(X3,X4))) = aux(X1,X2,X3,X4,btrue),
inference(orient,[status(thm)],[t23]) ).
cnf(t71,plain,
eq(merge(X1,cons(X2,X3)),X4) = eq(aux(Y4,X1,X2,X3,btrue),cons(Y4,X4)),
inference(cp,[status(thm)],[t70,t33]) ).
cnf(t347,plain,
eq(aux(X1,X2,X3,X4,btrue),cons(X1,Y4)) = eq(merge(X2,cons(X3,X4)),Y4),
inference(orient,[status(thm)],[t71]) ).
cnf(t352,plain,
eq(merge(X1,cons(X2,X3)),merge(X4,cons(Y4,Y5))) = eq(aux(Y6,X1,X2,X3,btrue),aux(Y6,X4,Y4,Y5,btrue)),
inference(cp,[status(thm)],[t347,t33]) ).
cnf(t2568,plain,
eq(aux(X1,X2,X3,X4,btrue),aux(X1,Y4,Y5,Y6,btrue)) = eq(merge(X2,cons(X3,X4)),merge(Y4,cons(Y5,Y6))),
inference(orient,[status(thm)],[t352]) ).
cnf(t33868,plain,
prop_merge_comm(nil,cons(z,X1),cons(z,X2)) = eq(merge(X1,cons(z,X2)),merge(X2,cons(z,X1))),
inference(step,[status(thm)],[t9467,t2568]) ).
cnf(t9627,plain,
eq(merge(X1,cons(z,X2)),merge(X2,cons(z,X1))) = prop_merge_comm(nil,cons(z,X1),cons(z,X2)),
inference(orient,[status(thm)],[t33868]) ).
cnf(f3,axiom,
leqNat(s(Z),z) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_003) ).
fof(f3_nnf,plain,
! [Z] : leqNat(s(Z),z) = bfalse,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [Z] : leqNat(s(Z),z) = bfalse,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
leqNat(s(X0),z) = bfalse,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t12,plain,
leqNat(s(X1),z) = bfalse,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t62,plain,
leqNat(s(X1),z) = bfalse,
inference(orient,[status(thm)],[t12]) ).
cnf(t101,plain,
merge(cons(s(X1),X2),cons(z,X3)) = aux(s(X1),X2,z,X3,bfalse),
inference(cp,[status(thm)],[t100,t62]) ).
cnf(t178,plain,
merge(cons(s(X1),X2),cons(z,X3)) = aux(s(X1),X2,z,X3,bfalse),
inference(orient,[status(thm)],[t101]) ).
cnf(t9656,plain,
prop_merge_comm(nil,cons(z,X1),cons(z,cons(s(X2),X3))) = eq(merge(X1,cons(z,cons(s(X2),X3))),aux(s(X2),X3,z,X1,bfalse)),
inference(cp,[status(thm)],[t9627,t178]) ).
cnf(t21137,plain,
eq(merge(X1,cons(z,cons(s(X2),X3))),aux(s(X2),X3,z,X1,bfalse)) = prop_merge_comm(nil,cons(z,X1),cons(z,cons(s(X2),X3))),
inference(orient,[status(thm)],[t9656]) ).
cnf(f1,axiom,
aux(Z,Xs,Y2,Ys,bfalse) = cons(Y2,merge(cons(Z,Xs),Ys)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_001) ).
fof(f1_nnf,plain,
! [Z,Xs,Y2,Ys] : aux(Z,Xs,Y2,Ys,bfalse) = cons(Y2,merge(cons(Z,Xs),Ys)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [Z,Xs,Y2,Ys] : aux(Z,Xs,Y2,Ys,bfalse) = cons(Y2,merge(cons(Z,Xs),Ys)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
aux(X0,X1,X2,X3,bfalse) = cons(X2,merge(cons(X0,X1),X3)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t24,plain,
cons(X1,merge(cons(X2,X3),X4)) = aux(X2,X3,X1,X4,bfalse),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t37,plain,
cons(X1,merge(cons(X2,X3),X4)) = aux(X2,X3,X1,X4,bfalse),
inference(orient,[status(thm)],[t24]) ).
cnf(f4,axiom,
leqNat(s(Z),s(M)) = leqNat(Z,M),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_004) ).
fof(f4_nnf,plain,
! [Z,M] : leqNat(s(Z),s(M)) = leqNat(Z,M),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [Z,M] : leqNat(s(Z),s(M)) = leqNat(Z,M),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
leqNat(s(X0),s(X1)) = leqNat(X0,X1),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t17,plain,
leqNat(s(X1),s(X2)) = leqNat(X1,X2),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t106,plain,
leqNat(s(X1),s(X2)) = leqNat(X1,X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t107,plain,
merge(cons(s(X1),X2),cons(s(X3),X4)) = aux(s(X1),X2,s(X3),X4,leqNat(X1,X3)),
inference(cp,[status(thm)],[t100,t106]) ).
cnf(t391,plain,
aux(s(X1),X2,s(X3),X4,leqNat(X1,X3)) = merge(cons(s(X1),X2),cons(s(X3),X4)),
inference(orient,[status(thm)],[t107]) ).
cnf(t394,plain,
merge(cons(s(z),X1),cons(s(X2),X3)) = aux(s(z),X1,s(X2),X3,btrue),
inference(cp,[status(thm)],[t391,t97]) ).
cnf(t395,plain,
merge(cons(s(z),X1),cons(s(X2),X3)) = aux(s(z),X1,s(X2),X3,btrue),
inference(orient,[status(thm)],[t394]) ).
cnf(t407,plain,
aux(s(z),X1,X2,cons(s(X3),X4),bfalse) = cons(X2,aux(s(z),X1,s(X3),X4,btrue)),
inference(cp,[status(thm)],[t37,t395]) ).
cnf(t406,plain,
aux(X1,cons(s(z),X2),s(X3),X4,btrue) = cons(X1,aux(s(z),X2,s(X3),X4,btrue)),
inference(cp,[status(thm)],[t33,t395]) ).
cnf(t674,plain,
cons(X1,aux(s(z),X2,s(X3),X4,btrue)) = aux(X1,cons(s(z),X2),s(X3),X4,btrue),
inference(orient,[status(thm)],[t406]) ).
cnf(t33351,plain,
aux(s(z),X1,X2,cons(s(X3),X4),bfalse) = aux(X2,cons(s(z),X1),s(X3),X4,btrue),
inference(step,[status(thm)],[t407,t674]) ).
cnf(t718,plain,
aux(s(z),X1,X2,cons(s(X3),X4),bfalse) = aux(X2,cons(s(z),X1),s(X3),X4,btrue),
inference(orient,[status(thm)],[t33351]) ).
cnf(t34,plain,
aux(X1,nil,X2,X3,btrue) = cons(X1,cons(X2,X3)),
inference(cp,[status(thm)],[t33,t29]) ).
cnf(t133,plain,
aux(X1,nil,X2,X3,btrue) = cons(X1,cons(X2,X3)),
inference(orient,[status(thm)],[t34]) ).
cnf(t677,plain,
aux(X1,cons(s(z),nil),s(X2),X3,btrue) = cons(X1,cons(s(z),cons(s(X2),X3))),
inference(cp,[status(thm)],[t674,t133]) ).
cnf(t715,plain,
aux(X1,cons(s(z),nil),s(X2),X3,btrue) = cons(X1,cons(s(z),cons(s(X2),X3))),
inference(orient,[status(thm)],[t677]) ).
cnf(t731,plain,
aux(s(z),nil,X1,cons(s(X2),X3),bfalse) = cons(X1,cons(s(z),cons(s(X2),X3))),
inference(cp,[status(thm)],[t718,t715]) ).
cnf(t744,plain,
aux(s(z),nil,X1,cons(s(X2),X3),bfalse) = cons(X1,cons(s(z),cons(s(X2),X3))),
inference(orient,[status(thm)],[t731]) ).
cnf(t21167,plain,
prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(z,cons(s(z),nil))) = eq(merge(cons(s(X1),X2),cons(z,cons(s(z),nil))),cons(z,cons(s(z),cons(s(X1),X2)))),
inference(cp,[status(thm)],[t21137,t744]) ).
cnf(t9632,plain,
prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(z,X3)) = eq(aux(s(X1),X2,z,X3,bfalse),merge(X3,cons(z,cons(s(X1),X2)))),
inference(cp,[status(thm)],[t9627,t178]) ).
cnf(t20916,plain,
eq(aux(s(X1),X2,z,X3,bfalse),merge(X3,cons(z,cons(s(X1),X2)))) = prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(z,X3)),
inference(orient,[status(thm)],[t9632]) ).
cnf(t38,plain,
aux(X1,X2,X3,cons(X4,Y4),bfalse) = aux(X3,cons(X1,X2),X4,Y4,btrue),
inference(cp,[status(thm)],[t37,t33]) ).
cnf(t906,plain,
aux(X1,X2,X3,cons(X4,Y4),bfalse) = aux(X3,cons(X1,X2),X4,Y4,btrue),
inference(orient,[status(thm)],[t38]) ).
cnf(t20936,plain,
prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(z,cons(X3,X4))) = eq(aux(z,cons(s(X1),X2),X3,X4,btrue),merge(cons(X3,X4),cons(z,cons(s(X1),X2)))),
inference(cp,[status(thm)],[t20916,t906]) ).
cnf(t34525,plain,
prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(z,cons(X3,X4))) = prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(X3,X4)),
inference(step,[status(thm)],[t20936,t9428]) ).
cnf(t21055,plain,
prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(z,cons(X3,X4))) = prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(X3,X4)),
inference(orient,[status(thm)],[t34525]) ).
cnf(t34679,plain,
prop_merge_comm(nil,cons(z,cons(s(X1),X2)),cons(s(z),nil)) = eq(merge(cons(s(X1),X2),cons(z,cons(s(z),nil))),cons(z,cons(s(z),cons(s(X1),X2)))),
inference(step,[status(thm)],[t21167,t21055]) ).
cnf(t113,plain,
prop_merge_comm(nil,cons(X1,X2),X3) = impl(eq(merge(nil,cons(X1,X2)),cons(X1,X2)),impl(eq(merge(nil,X3),merge(X3,nil)),eq(merge(cons(X1,X2),X3),merge(X3,cons(X1,X2))))),
inference(cp,[status(thm)],[t108,t32]) ).
cnf(t33978,plain,
prop_merge_comm(nil,cons(X1,X2),X3) = impl(eq(cons(X1,X2),cons(X1,X2)),impl(eq(merge(nil,X3),merge(X3,nil)),eq(merge(cons(X1,X2),X3),merge(X3,cons(X1,X2))))),
inference(step,[status(thm)],[t113,t29]) ).
cnf(t33979,plain,
prop_merge_comm(nil,cons(X1,X2),X3) = impl(eq(X2,X2),impl(eq(merge(nil,X3),merge(X3,nil)),eq(merge(cons(X1,X2),X3),merge(X3,cons(X1,X2))))),
inference(step,[status(thm)],[t33978,t70]) ).
cnf(t33980,plain,
prop_merge_comm(nil,cons(X1,X2),X3) = impl(btrue,impl(eq(merge(nil,X3),merge(X3,nil)),eq(merge(cons(X1,X2),X3),merge(X3,cons(X1,X2))))),
inference(step,[status(thm)],[t33979,t91]) ).
cnf(t33981,plain,
prop_merge_comm(nil,cons(X1,X2),X3) = impl(eq(merge(nil,X3),merge(X3,nil)),eq(merge(cons(X1,X2),X3),merge(X3,cons(X1,X2)))),
inference(step,[status(thm)],[t33980,t30]) ).
cnf(t33982,plain,
prop_merge_comm(nil,cons(X1,X2),X3) = impl(eq(X3,merge(X3,nil)),eq(merge(cons(X1,X2),X3),merge(X3,cons(X1,X2)))),
inference(step,[status(thm)],[t33981,t29]) ).
cnf(t10298,plain,
impl(eq(X1,merge(X1,nil)),eq(merge(cons(X2,X3),X1),merge(X1,cons(X2,X3)))) = prop_merge_comm(nil,cons(X2,X3),X1),
inference(orient,[status(thm)],[t33982]) ).
cnf(t7970,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(eq(cons(z,X1),merge(cons(z,X1),nil)),impl(eq(cons(s(X2),X3),merge(cons(s(X2),X3),nil)),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse)))),
inference(cp,[status(thm)],[t7924,t178]) ).
cnf(t33787,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(eq(cons(z,X1),cons(z,X1)),impl(eq(cons(s(X2),X3),merge(cons(s(X2),X3),nil)),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse)))),
inference(step,[status(thm)],[t7970,t32]) ).
cnf(t33788,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(eq(X1,X1),impl(eq(cons(s(X2),X3),merge(cons(s(X2),X3),nil)),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse)))),
inference(step,[status(thm)],[t33787,t70]) ).
cnf(t33789,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(btrue,impl(eq(cons(s(X2),X3),merge(cons(s(X2),X3),nil)),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse)))),
inference(step,[status(thm)],[t33788,t91]) ).
cnf(t33790,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(eq(cons(s(X2),X3),merge(cons(s(X2),X3),nil)),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse))),
inference(step,[status(thm)],[t33789,t30]) ).
cnf(t33791,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(eq(cons(s(X2),X3),cons(s(X2),X3)),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse))),
inference(step,[status(thm)],[t33790,t32]) ).
cnf(t33792,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(eq(X3,X3),eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse))),
inference(step,[status(thm)],[t33791,t70]) ).
cnf(t33793,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = impl(btrue,eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse))),
inference(step,[status(thm)],[t33792,t91]) ).
cnf(t33794,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = eq(merge(cons(z,X1),cons(s(X2),X3)),aux(s(X2),X3,z,X1,bfalse)),
inference(step,[status(thm)],[t33793,t30]) ).
cnf(t33795,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = eq(aux(z,X1,s(X2),X3,btrue),aux(s(X2),X3,z,X1,bfalse)),
inference(step,[status(thm)],[t33794,t151]) ).
cnf(t354,plain,
eq(merge(X1,cons(X2,X3)),merge(cons(X4,Y4),Y5)) = eq(aux(Y6,X1,X2,X3,btrue),aux(X4,Y4,Y6,Y5,bfalse)),
inference(cp,[status(thm)],[t347,t37]) ).
cnf(t2578,plain,
eq(aux(X1,X2,X3,X4,btrue),aux(Y4,Y5,X1,Y6,bfalse)) = eq(merge(X2,cons(X3,X4)),merge(cons(Y4,Y5),Y6)),
inference(orient,[status(thm)],[t354]) ).
cnf(t33796,plain,
prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)) = eq(merge(X1,cons(s(X2),X3)),merge(cons(s(X2),X3),X1)),
inference(step,[status(thm)],[t33795,t2578]) ).
cnf(t8581,plain,
eq(merge(X1,cons(s(X2),X3)),merge(cons(s(X2),X3),X1)) = prop_merge_comm(nil,cons(z,X1),cons(s(X2),X3)),
inference(orient,[status(thm)],[t33796]) ).
cnf(t10303,plain,
prop_merge_comm(nil,cons(X1,X2),cons(s(X3),X4)) = impl(eq(cons(s(X3),X4),merge(cons(s(X3),X4),nil)),prop_merge_comm(nil,cons(z,cons(X1,X2)),cons(s(X3),X4))),
inference(cp,[status(thm)],[t10298,t8581]) ).
cnf(t33992,plain,
prop_merge_comm(nil,cons(X1,X2),cons(s(X3),X4)) = impl(eq(cons(s(X3),X4),cons(s(X3),X4)),prop_merge_comm(nil,cons(z,cons(X1,X2)),cons(s(X3),X4))),
inference(step,[status(thm)],[t10303,t32]) ).
cnf(t33993,plain,
prop_merge_comm(nil,cons(X1,X2),cons(s(X3),X4)) = impl(eq(X4,X4),prop_merge_comm(nil,cons(z,cons(X1,X2)),cons(s(X3),X4))),
inference(step,[status(thm)],[t33992,t70]) ).
cnf(t33994,plain,
prop_merge_comm(nil,cons(X1,X2),cons(s(X3),X4)) = impl(btrue,prop_merge_comm(nil,cons(z,cons(X1,X2)),cons(s(X3),X4))),
inference(step,[status(thm)],[t33993,t91]) ).
cnf(t33995,plain,
prop_merge_comm(nil,cons(X1,X2),cons(s(X3),X4)) = prop_merge_comm(nil,cons(z,cons(X1,X2)),cons(s(X3),X4)),
inference(step,[status(thm)],[t33994,t30]) ).
cnf(t10476,plain,
prop_merge_comm(nil,cons(z,cons(X1,X2)),cons(s(X3),X4)) = prop_merge_comm(nil,cons(X1,X2),cons(s(X3),X4)),
inference(orient,[status(thm)],[t33995]) ).
cnf(t34680,plain,
prop_merge_comm(nil,cons(s(X1),X2),cons(s(z),nil)) = eq(merge(cons(s(X1),X2),cons(z,cons(s(z),nil))),cons(z,cons(s(z),cons(s(X1),X2)))),
inference(step,[status(thm)],[t34679,t10476]) ).
cnf(t34681,plain,
prop_merge_comm(nil,cons(s(X1),X2),cons(s(z),nil)) = eq(aux(s(X1),X2,z,cons(s(z),nil),bfalse),cons(z,cons(s(z),cons(s(X1),X2)))),
inference(step,[status(thm)],[t34680,t178]) ).
cnf(t34682,plain,
prop_merge_comm(nil,cons(s(X1),X2),cons(s(z),nil)) = eq(aux(z,cons(s(X1),X2),s(z),nil,btrue),cons(z,cons(s(z),cons(s(X1),X2)))),
inference(step,[status(thm)],[t34681,t906]) ).
cnf(t34683,plain,
prop_merge_comm(nil,cons(s(X1),X2),cons(s(z),nil)) = eq(merge(cons(s(X1),X2),cons(s(z),nil)),cons(s(z),cons(s(X1),X2))),
inference(step,[status(thm)],[t34682,t347]) ).
cnf(t33208,plain,
eq(merge(cons(s(X1),X2),cons(s(z),nil)),cons(s(z),cons(s(X1),X2))) = prop_merge_comm(nil,cons(s(X1),X2),cons(s(z),nil)),
inference(orient,[status(thm)],[t34683]) ).
cnf(t33209,plain,
prop_merge_comm(nil,cons(s(z),X1),cons(s(z),nil)) = eq(aux(s(z),X1,s(z),nil,btrue),cons(s(z),cons(s(z),X1))),
inference(cp,[status(thm)],[t33208,t395]) ).
cnf(t34684,plain,
prop_merge_comm(nil,cons(s(z),X1),cons(s(z),nil)) = eq(merge(X1,cons(s(z),nil)),cons(s(z),X1)),
inference(step,[status(thm)],[t33209,t347]) ).
cnf(t33266,plain,
eq(merge(X1,cons(s(z),nil)),cons(s(z),X1)) = prop_merge_comm(nil,cons(s(z),X1),cons(s(z),nil)),
inference(orient,[status(thm)],[t34684]) ).
cnf(t33272,plain,
prop_merge_comm(nil,cons(s(z),cons(z,X1)),cons(s(z),nil)) = eq(aux(z,X1,s(z),nil,btrue),cons(s(z),cons(z,X1))),
inference(cp,[status(thm)],[t33266,t151]) ).
cnf(f19,axiom,
( eq(cons(X,Y),cons(Z,X2)) = bfalse
| eq2(X,Z) != bfalse ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
fof(f19_nnf,plain,
! [X,Z,Y,X2] :
( eq(cons(X,Y),cons(Z,X2)) = bfalse
| eq2(X,Z) != bfalse ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X,Z,Y,X2] :
( eq(cons(X,Y),cons(Z,X2)) = bfalse
| eq2(X,Z) != bfalse ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( eq(cons(X0,X2),cons(X1,X3)) = bfalse
| eq2(X0,X1) != bfalse ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(hi18,axiom,
ifeq(eq2(X0,X1),bfalse,eq(cons(X0,X2),cons(X1,X3)),bfalse) = bfalse,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(f14,axiom,
eq2(z,s(X)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
fof(f14_nnf,plain,
! [X] : eq2(z,s(X)) = bfalse,
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X] : eq2(z,s(X)) = bfalse,
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
eq2(z,s(X0)) = bfalse,
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi13,axiom,
eq2(z,s(X0)) = bfalse,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t20,plain,
eq(cons(z,X1),cons(s(X2),X3)) = bfalse,
inference(hyper_resolution,[status(thm)],[hi18,hi13]) ).
cnf(t52,plain,
eq(cons(z,X1),cons(s(X2),X3)) = bfalse,
inference(orient,[status(thm)],[t20]) ).
cnf(t53,plain,
bfalse = eq(aux(z,X1,X2,X3,btrue),cons(s(X4),Y4)),
inference(cp,[status(thm)],[t52,t33]) ).
cnf(t272,plain,
eq(aux(z,X1,X2,X3,btrue),cons(s(X4),Y4)) = bfalse,
inference(orient,[status(thm)],[t53]) ).
cnf(t34686,plain,
prop_merge_comm(nil,cons(s(z),cons(z,X1)),cons(s(z),nil)) = bfalse,
inference(step,[status(thm)],[t33272,t272]) ).
cnf(t33304,plain,
prop_merge_comm(nil,cons(s(z),cons(z,X1)),cons(s(z),nil)) = bfalse,
inference(orient,[status(thm)],[t34686]) ).
cnf(t33335,plain,
efalse = eqq(eq3(bfalse,bfalse),btrue),
inference(cp,[status(thm)],[t125,t33304]) ).
cnf(f18,axiom,
eq3(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_018) ).
fof(f18_nnf,plain,
! [X] : eq3(X,X) = btrue,
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X] : eq3(X,X) = btrue,
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
eq3(X0,X0) = btrue,
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t2,plain,
eq3(X1,X1) = btrue,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t98,plain,
eq3(X1,X1) = btrue,
inference(orient,[status(thm)],[t2]) ).
cnf(t34687,plain,
efalse = eqq(btrue,btrue),
inference(step,[status(thm)],[t33335,t98]) ).
cnf(t5,plain,
eqq(X1,X1) = etrue,
introduced(definition) ).
cnf(t124,plain,
eqq(X1,X1) = etrue,
inference(orient,[status(thm)],[t5]) ).
cnf(t34688,plain,
efalse = etrue,
inference(step,[status(thm)],[t34687,t124]) ).
cnf(t33336,plain,
efalse = etrue,
inference(orient,[status(thm)],[t34688]) ).
cnf(goal_0,negated_conjecture,
etrue != efalse,
introduced(definition) ).
cnf(g0_0,plain,
etrue != etrue,
inference(rw,[status(thm)],[goal_0,t33336]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.34 % Computer : n011.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Thu Sep 24 23:35:42 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 62.31/8.43 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.31/8.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------