%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Tue Sep 29 01:45:33 PM UTC 2026
% Result : Unsatisfiable 5.54s 1.00s
% Output : Proof 5.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX199-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.15 % Computer : n002.cluster.edu
% 0.10/0.15 % Model : x86_64 x86_64
% 0.10/0.15 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.15 % Memory : 8046.5625MB
% 0.10/0.15 % OS : Linux 6.8.0-71-generic
% 0.10/0.15 % CPULimit : 300
% 0.10/0.15 % WCLimit : 300
% 0.10/0.15 % DateTime : Mon Sep 28 15:10:36 UTC 2026
% 0.10/0.15 % CPUTime :
% 0.10/0.15 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.54/1.00 Command-line arguments: --flatten-regeneralise
% 5.54/1.00
% 5.54/1.00 % SZS status Unsatisfiable
% 5.54/1.00
% 5.54/1.02 % SZS output start Proof
% 5.54/1.02 Axiom 1 (axiom_008): impl(btrue, X) = X.
% 5.54/1.02 Axiom 2 (axiom_018): eq3(X, X) = btrue.
% 5.54/1.02 Axiom 3 (axiom_002): leqNat(z, X) = btrue.
% 5.54/1.02 Axiom 4 (axiom_003): leqNat(s(X), z) = bfalse.
% 5.54/1.02 Axiom 5 (axiom_004): leqNat(s(X), s(Y)) = leqNat(X, Y).
% 5.54/1.02 Axiom 6 (axiom_017): eq2(X, X) = btrue.
% 5.54/1.02 Axiom 7 (axiom_015): eq2(s(X), z) = bfalse.
% 5.54/1.02 Axiom 8 (axiom_016): eq(X, X) = btrue.
% 5.54/1.02 Axiom 9 (axiom_005): merge(nil, X) = X.
% 5.54/1.02 Axiom 10 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 5.54/1.02 Axiom 11 (axiom_006): merge(cons(X, Y), nil) = cons(X, Y).
% 5.54/1.02 Axiom 12 (axiom): aux(X, Y, Z, W, btrue) = cons(X, merge(Y, cons(Z, W))).
% 5.54/1.02 Axiom 13 (axiom_001): aux(X, Y, Z, W, bfalse) = cons(Z, merge(cons(X, Y), W)).
% 5.54/1.02 Axiom 14 (axiom_007): merge(cons(X, Y), cons(Z, W)) = aux(X, Y, Z, W, leqNat(X, Z)).
% 5.54/1.02 Axiom 15 (axiom_019): ifeq(eq2(X, Y), bfalse, eq(cons(X, Z), cons(Y, W)), bfalse) = bfalse.
% 5.54/1.02 Axiom 16 (axiom_020): ifeq(eq2(X, Y), btrue, eq(cons(X, Z), cons(Y, W)), eq(Z, W)) = eq(Z, W).
% 5.54/1.02 Axiom 17 (axiom_010): 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)))).
% 5.54/1.02
% 5.54/1.02 Lemma 18: merge(cons(z, X), cons(Y, Z)) = aux(z, X, Y, Z, btrue).
% 5.54/1.02 Proof:
% 5.54/1.02 merge(cons(z, X), cons(Y, Z))
% 5.54/1.02 = { by axiom 14 (axiom_007) }
% 5.54/1.02 aux(z, X, Y, Z, leqNat(z, Y))
% 5.54/1.02 = { by axiom 3 (axiom_002) }
% 5.54/1.02 aux(z, X, Y, Z, btrue)
% 5.54/1.02
% 5.54/1.02 Lemma 19: eq(cons(X, Y), cons(X, Z)) = eq(Y, Z).
% 5.54/1.02 Proof:
% 5.54/1.02 eq(cons(X, Y), cons(X, Z))
% 5.54/1.02 = { by axiom 10 (ifeq_axiom) R->L }
% 5.54/1.02 ifeq(btrue, btrue, eq(cons(X, Y), cons(X, Z)), eq(Y, Z))
% 5.54/1.02 = { by axiom 6 (axiom_017) R->L }
% 5.54/1.02 ifeq(eq2(X, X), btrue, eq(cons(X, Y), cons(X, Z)), eq(Y, Z))
% 5.54/1.02 = { by axiom 16 (axiom_020) }
% 5.54/1.02 eq(Y, Z)
% 5.54/1.02
% 5.54/1.02 Lemma 20: merge(cons(s(X), Y), cons(z, Z)) = aux(s(X), Y, z, Z, bfalse).
% 5.54/1.02 Proof:
% 5.54/1.02 merge(cons(s(X), Y), cons(z, Z))
% 5.54/1.02 = { by axiom 14 (axiom_007) }
% 5.54/1.02 aux(s(X), Y, z, Z, leqNat(s(X), z))
% 5.54/1.02 = { by axiom 4 (axiom_003) }
% 5.54/1.02 aux(s(X), Y, z, Z, bfalse)
% 5.54/1.02
% 5.54/1.02 Lemma 21: merge(cons(s(z), X), cons(s(Y), Z)) = aux(s(z), X, s(Y), Z, btrue).
% 5.54/1.02 Proof:
% 5.54/1.02 merge(cons(s(z), X), cons(s(Y), Z))
% 5.54/1.02 = { by axiom 14 (axiom_007) }
% 5.54/1.02 aux(s(z), X, s(Y), Z, leqNat(s(z), s(Y)))
% 5.54/1.02 = { by axiom 5 (axiom_004) }
% 5.54/1.02 aux(s(z), X, s(Y), Z, leqNat(z, Y))
% 5.54/1.02 = { by axiom 3 (axiom_002) }
% 5.54/1.02 aux(s(z), X, s(Y), Z, btrue)
% 5.54/1.02
% 5.54/1.02 Lemma 22: impl(eq(X, merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z)))) = prop_merge_comm(nil, cons(Y, Z), X).
% 5.54/1.02 Proof:
% 5.54/1.02 impl(eq(X, merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z))))
% 5.54/1.02 = { by axiom 9 (axiom_005) R->L }
% 5.54/1.02 impl(eq(merge(nil, X), merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z))))
% 5.54/1.02 = { by axiom 1 (axiom_008) R->L }
% 5.54/1.02 impl(btrue, impl(eq(merge(nil, X), merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z)))))
% 5.54/1.02 = { by axiom 8 (axiom_016) R->L }
% 5.54/1.02 impl(eq(Z, Z), impl(eq(merge(nil, X), merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z)))))
% 5.54/1.02 = { by lemma 19 R->L }
% 5.54/1.02 impl(eq(cons(Y, Z), cons(Y, Z)), impl(eq(merge(nil, X), merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z)))))
% 5.54/1.02 = { by axiom 9 (axiom_005) R->L }
% 5.54/1.02 impl(eq(merge(nil, cons(Y, Z)), cons(Y, Z)), impl(eq(merge(nil, X), merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z)))))
% 5.54/1.02 = { by axiom 11 (axiom_006) R->L }
% 5.54/1.02 impl(eq(merge(nil, cons(Y, Z)), merge(cons(Y, Z), nil)), impl(eq(merge(nil, X), merge(X, nil)), eq(merge(cons(Y, Z), X), merge(X, cons(Y, Z)))))
% 5.54/1.02 = { by axiom 17 (axiom_010) R->L }
% 5.54/1.02 prop_merge_comm(nil, cons(Y, Z), X)
% 5.54/1.02
% 5.54/1.02 Goal 1 (goal): eq3(prop_merge_comm(X, Y, Z), bfalse) = btrue.
% 5.54/1.02 The goal is true when:
% 5.54/1.02 X = nil
% 5.54/1.02 Y = cons(s(z), nil)
% 5.54/1.02 Z = cons(s(z), cons(z, X))
% 5.54/1.02
% 5.54/1.03 Proof:
% 5.54/1.03 eq3(prop_merge_comm(nil, cons(s(z), nil), cons(s(z), cons(z, X))), bfalse)
% 5.54/1.03 = { by lemma 22 R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(merge(cons(s(z), nil), cons(s(z), cons(z, X))), merge(cons(s(z), cons(z, X)), cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by lemma 19 R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(cons(z, merge(cons(s(z), nil), cons(s(z), cons(z, X)))), cons(z, merge(cons(s(z), cons(z, X)), cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by axiom 12 (axiom) R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), cons(z, merge(cons(s(z), cons(z, X)), cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by axiom 13 (axiom_001) R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse))), bfalse)
% 5.54/1.03 = { by lemma 18 R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse))), bfalse)
% 5.54/1.03 = { by axiom 1 (axiom_008) R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), impl(btrue, eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse)))), bfalse)
% 5.54/1.03 = { by axiom 8 (axiom_016) R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), impl(eq(cons(z, X), cons(z, X)), eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse)))), bfalse)
% 5.54/1.03 = { by lemma 19 R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), impl(eq(cons(s(z), cons(z, X)), cons(s(z), cons(z, X))), eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse)))), bfalse)
% 5.54/1.03 = { by axiom 11 (axiom_006) R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse)))), bfalse)
% 5.54/1.03 = { by lemma 20 R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil)))))), bfalse)
% 5.54/1.03 = { by lemma 22 }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), prop_merge_comm(nil, cons(z, cons(s(z), nil)), cons(s(z), cons(z, X)))), bfalse)
% 5.54/1.03 = { by axiom 11 (axiom_006) }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), cons(s(z), cons(z, X))), prop_merge_comm(nil, cons(z, cons(s(z), nil)), cons(s(z), cons(z, X)))), bfalse)
% 5.54/1.03 = { by lemma 19 }
% 5.54/1.03 eq3(impl(eq(cons(z, X), cons(z, X)), prop_merge_comm(nil, cons(z, cons(s(z), nil)), cons(s(z), cons(z, X)))), bfalse)
% 5.54/1.03 = { by axiom 8 (axiom_016) }
% 5.54/1.03 eq3(impl(btrue, prop_merge_comm(nil, cons(z, cons(s(z), nil)), cons(s(z), cons(z, X)))), bfalse)
% 5.54/1.03 = { by axiom 1 (axiom_008) }
% 5.54/1.03 eq3(prop_merge_comm(nil, cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), bfalse)
% 5.54/1.03 = { by lemma 22 R->L }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(merge(cons(z, cons(s(z), nil)), cons(s(z), cons(z, X))), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by lemma 18 }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), merge(cons(s(z), cons(z, X)), nil)), eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by axiom 11 (axiom_006) }
% 5.54/1.03 eq3(impl(eq(cons(s(z), cons(z, X)), cons(s(z), cons(z, X))), eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by lemma 19 }
% 5.54/1.03 eq3(impl(eq(cons(z, X), cons(z, X)), eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by axiom 8 (axiom_016) }
% 5.54/1.03 eq3(impl(btrue, eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil))))), bfalse)
% 5.54/1.03 = { by axiom 1 (axiom_008) }
% 5.54/1.03 eq3(eq(aux(z, cons(s(z), nil), s(z), cons(z, X), btrue), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by axiom 12 (axiom) }
% 5.54/1.03 eq3(eq(cons(z, merge(cons(s(z), nil), cons(s(z), cons(z, X)))), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by lemma 21 }
% 5.54/1.03 eq3(eq(cons(z, aux(s(z), nil, s(z), cons(z, X), btrue)), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by axiom 12 (axiom) }
% 5.54/1.03 eq3(eq(cons(z, cons(s(z), merge(nil, cons(s(z), cons(z, X))))), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by axiom 9 (axiom_005) }
% 5.54/1.03 eq3(eq(cons(z, cons(s(z), cons(s(z), cons(z, X)))), merge(cons(s(z), cons(z, X)), cons(z, cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by lemma 20 }
% 5.54/1.03 eq3(eq(cons(z, cons(s(z), cons(s(z), cons(z, X)))), aux(s(z), cons(z, X), z, cons(s(z), nil), bfalse)), bfalse)
% 5.54/1.03 = { by axiom 13 (axiom_001) }
% 5.54/1.03 eq3(eq(cons(z, cons(s(z), cons(s(z), cons(z, X)))), cons(z, merge(cons(s(z), cons(z, X)), cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by lemma 19 }
% 5.54/1.03 eq3(eq(cons(s(z), cons(s(z), cons(z, X))), merge(cons(s(z), cons(z, X)), cons(s(z), nil))), bfalse)
% 5.54/1.03 = { by lemma 21 }
% 5.54/1.03 eq3(eq(cons(s(z), cons(s(z), cons(z, X))), aux(s(z), cons(z, X), s(z), nil, btrue)), bfalse)
% 5.54/1.03 = { by axiom 12 (axiom) }
% 5.54/1.03 eq3(eq(cons(s(z), cons(s(z), cons(z, X))), cons(s(z), merge(cons(z, X), cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by lemma 19 }
% 5.54/1.03 eq3(eq(cons(s(z), cons(z, X)), merge(cons(z, X), cons(s(z), nil))), bfalse)
% 5.54/1.03 = { by lemma 18 }
% 5.54/1.03 eq3(eq(cons(s(z), cons(z, X)), aux(z, X, s(z), nil, btrue)), bfalse)
% 5.54/1.03 = { by axiom 12 (axiom) }
% 5.54/1.03 eq3(eq(cons(s(z), cons(z, X)), cons(z, merge(X, cons(s(z), nil)))), bfalse)
% 5.54/1.03 = { by axiom 10 (ifeq_axiom) R->L }
% 5.54/1.03 eq3(ifeq(bfalse, bfalse, eq(cons(s(z), cons(z, X)), cons(z, merge(X, cons(s(z), nil)))), bfalse), bfalse)
% 5.54/1.03 = { by axiom 7 (axiom_015) R->L }
% 5.54/1.03 eq3(ifeq(eq2(s(z), z), bfalse, eq(cons(s(z), cons(z, X)), cons(z, merge(X, cons(s(z), nil)))), bfalse), bfalse)
% 5.54/1.03 = { by axiom 15 (axiom_019) }
% 5.54/1.03 eq3(bfalse, bfalse)
% 5.54/1.04 = { by axiom 2 (axiom_018) }
% 5.54/1.04 btrue
% 5.54/1.04 % SZS output end Proof
% 5.54/1.04
% 5.54/1.04 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------