%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX200-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:19 AM UTC 2026
% Result : Unsatisfiable 0.16s 0.49s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of formulae : 42 ( 42 unt; 0 def)
% Number of atoms : 42 ( 41 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 11 ( 11 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-4 aty)
% Number of variables : 54 ( 12 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_003,axiom,
! [VAR_0,VAR_1,VAR_2] : aux2(VAR_0,VAR_1,VAR_2,bfalse) = bfalse,
file('theBenchmark.p',axiom_003) ).
cnf(c_4,plain,
aux2(A,B,C,bfalse) = bfalse,
inference(clausify,[status(thm)],[axiom_003]) ).
fof(axiom_005,axiom,
! [VAR_0] : leqNat(s(VAR_0),z) = bfalse,
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
leqNat(s(A),z) = bfalse,
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_007,axiom,
! [VAR_0] : merge(nil,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_007) ).
cnf(c_8,plain,
merge(nil,A) = A,
inference(clausify,[status(thm)],[axiom_007]) ).
fof(axiom_010,axiom,
ord(nil) = btrue,
file('theBenchmark.p',axiom_010) ).
cnf(c_12,plain,
ord(nil) = btrue,
inference(clausify,[status(thm)],[axiom_010]) ).
cnf(c_13,plain,
btrue = ord(nil),
inference(copy,[status(thm)],[c_12]) ).
fof(axiom_012,axiom,
! [VAR_0,VAR_1,VAR_2] : ord(cons(VAR_0,cons(VAR_1,VAR_2))) = aux2(VAR_0,VAR_1,VAR_2,leqNat(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_012) ).
cnf(c_16,plain,
ord(cons(A,cons(B,C))) = aux2(A,B,C,leqNat(A,B)),
inference(clausify,[status(thm)],[axiom_012]) ).
cnf(c_17,plain,
aux2(A,B,C,leqNat(A,B)) = ord(cons(A,cons(B,C))),
inference(copy,[status(thm)],[c_16]) ).
fof(axiom_013,axiom,
! [VAR_0] : impl(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_013) ).
cnf(c_18,plain,
impl(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_013]) ).
cnf(c_19,plain,
impl(ord(nil),A) = A,
inference(paramod,[status(thm)],[c_13,c_18]) ).
fof(axiom_015,axiom,
! [VAR_0,VAR_1] : prop_merge_ord_not3(VAR_0,VAR_1) = impl(eq2(ord(VAR_0),btrue),impl(eq2(ord(VAR_1),bfalse),eq2(ord(merge(VAR_0,VAR_1)),btrue))),
file('theBenchmark.p',axiom_015) ).
cnf(c_22,plain,
prop_merge_ord_not3(A,B) = impl(eq2(ord(A),btrue),impl(eq2(ord(B),bfalse),eq2(ord(merge(A,B)),btrue))),
inference(clausify,[status(thm)],[axiom_015]) ).
cnf(c_138,plain,
prop_merge_ord_not3(A,B) = impl(eq2(ord(A),ord(nil)),impl(eq2(ord(B),bfalse),eq2(ord(merge(A,B)),btrue))),
inference(paramod,[status(thm)],[c_13,c_22]) ).
cnf(c_23,plain,
prop_merge_ord_not3(A,B) = impl(eq2(ord(A),ord(nil)),impl(eq2(ord(B),bfalse),eq2(ord(merge(A,B)),ord(nil)))),
inference(paramod,[status(thm)],[c_13,c_138]) ).
fof(axiom_016,axiom,
eq2(bfalse,btrue) = bfalse,
file('theBenchmark.p',axiom_016) ).
cnf(c_24,plain,
eq2(bfalse,btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_016]) ).
cnf(c_25,plain,
eq2(bfalse,ord(nil)) = bfalse,
inference(paramod,[status(thm)],[c_13,c_24]) ).
fof(axiom_022,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_022) ).
cnf(c_33,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_022]) ).
cnf(c_34,plain,
eq2(A,A) = ord(nil),
inference(paramod,[status(thm)],[c_13,c_33]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : eq2(prop_merge_ord_not3(VAR_0,VAR_1),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_35,plain,
eq2(prop_merge_ord_not3(A,B),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_139,plain,
eq2(impl(eq2(ord(A),ord(nil)),impl(eq2(ord(B),bfalse),eq2(ord(merge(A,B)),ord(nil)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_23,c_35]) ).
cnf(c_36,plain,
eq2(impl(eq2(ord(A),ord(nil)),impl(eq2(ord(B),bfalse),eq2(ord(merge(A,B)),ord(nil)))),bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_13,c_139]) ).
cnf(c_140,plain,
aux2(s(A),z,B,bfalse) = ord(cons(s(A),cons(z,B))),
inference(paramod,[status(thm)],[c_6,c_17]) ).
cnf(c_141,plain,
bfalse = ord(cons(s(A),cons(z,B))),
inference(paramod,[status(thm)],[c_4,c_140]) ).
cnf(c_42,plain,
ord(cons(s(A),cons(z,B))) = bfalse,
inference(copy,[status(thm)],[c_141]) ).
cnf(c_61,plain,
impl(eq2(A,A),B) = B,
inference(paramod,[status(thm)],[c_34,c_19]) ).
cnf(c_142,plain,
eq2(impl(eq2(ord(nil),ord(nil)),impl(eq2(ord(A),bfalse),eq2(ord(A),ord(nil)))),bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_8,c_36]) ).
cnf(c_73,plain,
eq2(impl(eq2(ord(A),bfalse),eq2(ord(A),ord(nil))),bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_61,c_142]) ).
cnf(c_143,plain,
eq2(impl(eq2(bfalse,bfalse),eq2(ord(cons(s(A),cons(z,B))),ord(nil))),bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_42,c_73]) ).
cnf(c_144,plain,
eq2(impl(eq2(bfalse,bfalse),eq2(bfalse,ord(nil))),bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_42,c_143]) ).
cnf(c_145,plain,
eq2(impl(eq2(bfalse,bfalse),bfalse),bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_25,c_144]) ).
cnf(c_146,plain,
eq2(bfalse,bfalse) != ord(nil),
inference(paramod,[status(thm)],[c_61,c_145]) ).
cnf(c_136,plain,
ord(nil) != eq2(bfalse,bfalse),
inference(copy,[status(thm)],[c_146]) ).
cnf(c_147,plain,
ord(nil) = eq2(A,A),
inference(copy,[status(thm)],[c_34]) ).
cnf(c_137,plain,
$false,
inference(resolve,[status(thm)],[c_136,c_147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX200-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.45 % Computer : n003.cluster.edu
% 0.16/0.45 % Model : x86_64 x86_64
% 0.16/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.45 % Memory : 8046.5625MB
% 0.16/0.45 % OS : Linux 6.8.0-71-generic
% 0.16/0.45 % CPULimit : 300
% 0.16/0.45 % WCLimit : 300
% 0.16/0.45 % DateTime : Sat Sep 26 16:56:26 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.45 % Process 3349076 was started by sandbox2 on n003,
% 0.16/0.45 % Sat Sep 26 16:56:26 2026
% 0.16/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.46
% 0.16/0.46 % From the command line: assign(max_seconds, 300).
% 0.16/0.49
% 0.16/0.49 % SZS status Unsatisfiable for theBenchmark
% 0.16/0.49
% 0.16/0.49 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.16/0.49 % Length of proof is 22.
% 0.16/0.49 % Level of proof is 6.
% 0.16/0.49 % Maximum clause weight is 23.000.
% 0.16/0.49 % Given clauses 43.
% 0.16/0.49
% 0.16/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------