%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Sun Sep 27 09:16:18 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.44s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 57 ( 53 unt; 0 def)
% Number of atoms : 61 ( 60 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 22 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-5 aty)
% Number of variables : 132 ( 10 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : aux(VAR_0,VAR_1,VAR_2,VAR_3,btrue) = cons(VAR_0,merge(VAR_1,cons(VAR_2,VAR_3))),
file('theBenchmark.p',axiom) ).
cnf(c_1,plain,
aux(A,B,C,D,btrue) = cons(A,merge(B,cons(C,D))),
inference(clausify,[status(thm)],[axiom]) ).
fof(axiom_002,axiom,
! [VAR_0] : leqNat(z,VAR_0) = btrue,
file('theBenchmark.p',axiom_002) ).
cnf(c_3,plain,
leqNat(z,A) = btrue,
inference(clausify,[status(thm)],[axiom_002]) ).
fof(axiom_004,axiom,
! [VAR_0,VAR_1] : leqNat(s(VAR_0),s(VAR_1)) = leqNat(VAR_0,VAR_1),
file('theBenchmark.p',axiom_004) ).
cnf(c_5,plain,
leqNat(s(A),s(B)) = leqNat(A,B),
inference(clausify,[status(thm)],[axiom_004]) ).
fof(axiom_005,axiom,
! [VAR_0] : merge(nil,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
merge(nil,A) = A,
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_006,axiom,
! [VAR_0,VAR_1] : merge(cons(VAR_0,VAR_1),nil) = cons(VAR_0,VAR_1),
file('theBenchmark.p',axiom_006) ).
cnf(c_7,plain,
merge(cons(A,B),nil) = cons(A,B),
inference(clausify,[status(thm)],[axiom_006]) ).
fof(axiom_007,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : merge(cons(VAR_0,VAR_1),cons(VAR_2,VAR_3)) = aux(VAR_0,VAR_1,VAR_2,VAR_3,leqNat(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_007) ).
cnf(c_8,plain,
merge(cons(A,B),cons(C,D)) = aux(A,B,C,D,leqNat(A,C)),
inference(clausify,[status(thm)],[axiom_007]) ).
cnf(c_9,plain,
aux(A,B,C,D,leqNat(A,C)) = merge(cons(A,B),cons(C,D)),
inference(copy,[status(thm)],[c_8]) ).
fof(axiom_008,axiom,
! [VAR_0] : impl(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_008) ).
cnf(c_10,plain,
impl(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_008]) ).
fof(axiom_010,axiom,
! [VAR_0,VAR_1,VAR_2] : prop_merge_comm(VAR_0,VAR_1,VAR_2) = impl(eq(merge(VAR_0,VAR_1),merge(VAR_1,VAR_0)),impl(eq(merge(VAR_0,VAR_2),merge(VAR_2,VAR_0)),eq(merge(VAR_1,VAR_2),merge(VAR_2,VAR_1)))),
file('theBenchmark.p',axiom_010) ).
cnf(c_12,plain,
prop_merge_comm(A,B,C) = impl(eq(merge(A,B),merge(B,A)),impl(eq(merge(A,C),merge(C,A)),eq(merge(B,C),merge(C,B)))),
inference(clausify,[status(thm)],[axiom_010]) ).
fof(axiom_015,axiom,
! [VAR_0] : eq2(s(VAR_0),z) = bfalse,
file('theBenchmark.p',axiom_015) ).
cnf(c_17,plain,
eq2(s(A),z) = bfalse,
inference(clausify,[status(thm)],[axiom_015]) ).
fof(axiom_016,axiom,
! [VAR_0] : eq(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_016) ).
cnf(c_18,plain,
eq(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_016]) ).
fof(axiom_017,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_017) ).
cnf(c_19,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_017]) ).
fof(axiom_018,axiom,
! [VAR_0] : eq3(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_018) ).
cnf(c_20,plain,
eq3(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_018]) ).
fof(axiom_019,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq(cons(VAR_0,VAR_2),cons(VAR_1,VAR_3)) = bfalse
| eq2(VAR_0,VAR_1) != bfalse ),
file('theBenchmark.p',axiom_019) ).
cnf(c_21,plain,
( eq(cons(A,C),cons(B,D)) = bfalse
| eq2(A,B) != bfalse ),
inference(clausify,[status(thm)],[axiom_019]) ).
fof(axiom_020,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq(cons(VAR_0,VAR_2),cons(VAR_1,VAR_3)) = eq(VAR_2,VAR_3)
| eq2(VAR_0,VAR_1) != btrue ),
file('theBenchmark.p',axiom_020) ).
cnf(c_22,plain,
( eq(cons(A,C),cons(B,D)) = eq(C,D)
| eq2(A,B) != btrue ),
inference(clausify,[status(thm)],[axiom_020]) ).
fof(goal,axiom,
! [VAR_0,VAR_1,VAR_2] : eq3(prop_merge_comm(VAR_0,VAR_1,VAR_2),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_25,plain,
eq3(prop_merge_comm(A,B,C),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_26,plain,
eq3(impl(eq(merge(A,B),merge(B,A)),impl(eq(merge(A,C),merge(C,A)),eq(merge(B,C),merge(C,B)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_12,c_25]) ).
cnf(c_184,plain,
aux(z,A,B,C,btrue) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_3,c_9]) ).
cnf(c_185,plain,
cons(z,merge(A,cons(B,C))) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_1,c_184]) ).
cnf(c_27,plain,
merge(cons(z,A),cons(B,C)) = cons(z,merge(A,cons(B,C))),
inference(copy,[status(thm)],[c_185]) ).
cnf(c_29,plain,
aux(s(A),B,s(C),D,leqNat(A,C)) = merge(cons(s(A),B),cons(s(C),D)),
inference(paramod,[status(thm)],[c_5,c_9]) ).
cnf(c_30,plain,
eq(cons(s(A),B),cons(z,C)) = bfalse,
inference(resolve,[status(thm)],[c_21,c_17]) ).
cnf(c_34,plain,
eq(cons(A,B),cons(A,C)) = eq(B,C),
inference(resolve,[status(thm)],[c_22,c_19]) ).
cnf(c_186,plain,
eq3(impl(eq(A,merge(A,nil)),impl(eq(merge(nil,B),merge(B,nil)),eq(merge(A,B),merge(B,A)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_6,c_26]) ).
cnf(c_37,plain,
eq3(impl(eq(A,merge(A,nil)),impl(eq(B,merge(B,nil)),eq(merge(A,B),merge(B,A)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_6,c_186]) ).
cnf(c_187,plain,
aux(s(z),A,s(B),C,btrue) = merge(cons(s(z),A),cons(s(B),C)),
inference(paramod,[status(thm)],[c_3,c_29]) ).
cnf(c_188,plain,
cons(s(z),merge(A,cons(s(B),C))) = merge(cons(s(z),A),cons(s(B),C)),
inference(paramod,[status(thm)],[c_1,c_187]) ).
cnf(c_61,plain,
merge(cons(s(z),A),cons(s(B),C)) = cons(s(z),merge(A,cons(s(B),C))),
inference(copy,[status(thm)],[c_188]) ).
cnf(c_189,plain,
eq3(impl(eq(cons(s(z),A),merge(cons(s(z),A),nil)),impl(eq(cons(s(B),C),merge(cons(s(B),C),nil)),eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_37]) ).
cnf(c_190,plain,
eq3(impl(eq(cons(s(z),A),cons(s(z),A)),impl(eq(cons(s(B),C),merge(cons(s(B),C),nil)),eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_7,c_189]) ).
cnf(c_191,plain,
eq3(impl(btrue,impl(eq(cons(s(B),C),merge(cons(s(B),C),nil)),eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_18,c_190]) ).
cnf(c_192,plain,
eq3(impl(btrue,impl(eq(cons(s(B),C),cons(s(B),C)),eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_7,c_191]) ).
cnf(c_193,plain,
eq3(impl(btrue,impl(btrue,eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_18,c_192]) ).
cnf(c_194,plain,
eq3(impl(btrue,eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_10,c_193]) ).
cnf(c_91,plain,
eq3(eq(cons(s(z),merge(A,cons(s(B),C))),merge(cons(s(B),C),cons(s(z),A))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_10,c_194]) ).
cnf(c_195,plain,
eq3(eq(cons(s(z),merge(A,cons(s(z),B))),cons(s(z),merge(B,cons(s(z),A)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_91]) ).
cnf(c_174,plain,
eq3(eq(merge(A,cons(s(z),B)),merge(B,cons(s(z),A))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_34,c_195]) ).
cnf(c_176,plain,
eq3(eq(cons(s(z),A),merge(A,cons(s(z),nil))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_6,c_174]) ).
cnf(c_196,plain,
eq3(eq(cons(s(z),cons(z,A)),cons(z,merge(A,cons(s(z),nil)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_27,c_176]) ).
cnf(c_197,plain,
eq3(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_30,c_196]) ).
cnf(c_198,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_20,c_197]) ).
cnf(c_183,plain,
$false,
inference(copy,[status(thm)],[c_198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 16:54:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1779134 was started by sandbox on n019,
% 0.10/0.37 % Sat Sep 26 16:54:20 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 0.10/0.44
% 0.10/0.44 % SZS status Unsatisfiable for theBenchmark
% 0.10/0.44
% 0.10/0.44 % Proof 1 at 0.04 (+ 0.02) seconds.
% 0.10/0.44 % Length of proof is 27.
% 0.10/0.44 % Level of proof is 7.
% 0.10/0.44 % Maximum clause weight is 62.000.
% 0.10/0.44 % Given clauses 100.
% 0.10/0.44
% 0.10/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------