%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX055+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:07 AM UTC 2026
% Result : Theorem 238.07s 32.44s
% Output : CNFRefutation 238.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX055+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n009.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:45:14 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 632035 was started by sandbox2 on n009,
% 0.10/0.37 % Sat Sep 26 16:45:14 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.44
% 0.10/0.44 % From the command line: assign(max_seconds, 300).
% 0.10/0.44
% 0.10/0.44 % SInE: 217 to sos, 83 to usable, of 300 axioms (tolerance 2.00, depth 0 fixpoint).
% 238.07/32.44
% 238.07/32.44 % given #500 (T,wt=16): 1983 list_succeeds(f41(c6)) | c6 = nil. [resolve(754,a,1014,a),flip(b)].
% 238.07/32.44
% 238.07/32.44 % given #1000 (W,wt=16): 3530 append_terminates(f59(c7,c7),A,B). [resolve(3422,a,519,a)].
% 238.07/32.44
% 238.07/32.44 % given #1500 (A,wt=30): 1100 -times_succeeds(A,B,C) | s(f42(A,B,C)) = A | lh(nil) = C. [back_rewrite(761),rewrite([925(5)])].
% 238.07/32.44
% 238.07/32.44 % given #2000 (W,wt=21): 4166 list_succeeds(**(c6,cons(A,nil))). [resolve(3488,a,899,a)].
% 238.07/32.44
% 238.07/32.44 % given #2500 (A,wt=27): 1732 sub(c6,A) | member_succeeds(f130(**(c6,B),A),**(c6,B)). [resolve(1379,a,545,a)].
% 238.07/32.44
% 238.07/32.44 % given #3000 (T,wt=22): 7459 delete_terminates(A,B,f41(cons(C,c6))). [resolve(2320,a,539,a)].
% 238.07/32.44
% 238.07/32.44 % given #3500 (A,wt=23): 2128 nat_succeeds(A) | s(occ(B,c6)) != A. [resolve(810,c,1417,a)].
% 238.07/32.44
% 238.07/32.44 % given #4000 (A,wt=33): 2348 delete_succeeds(f22(cons(A,c7),cons(A,c7)),cons(A,c7),f24(cons(A,c7),cons(A,c7))). [resolve(2237,a,715,a),flip(b),unit_del(b,554)].
% 238.07/32.44
% 238.07/32.44 % given #4500 (T,wt=23): 6444 @*(lh(nil),lh(c7)) = lh(nil). [resolve(1077,a,1338,a)].
% 238.07/32.44
% 238.07/32.44 % given #5000 (W,wt=23): 14213 occ(A,c7) = occ(A,c6) | append_terminates(**(c4,c4),B,C). [resolve(6296,b,519,a)].
% 238.07/32.44
% 238.07/32.44 % SZS status Theorem for theBenchmark
% 238.07/32.44
% 238.07/32.44 % Proof 1 at 5.59 (+ 1.58) seconds.
% 238.07/32.44 % Length of proof is 48.
% 238.07/32.44 % Level of proof is 13.
% 238.07/32.44 % Maximum clause weight is 321.000.
% 238.07/32.44 % Given clauses 5228.
% 238.07/32.44
% 238.07/32.44 % SZS output start CNFRefutation for theBenchmark
% 238.07/32.44 fof(id16, axiom, ! [Xx28,Xx29,Xx30] : ~ ((occ_succeeds(Xx28,Xx29,Xx30) & occ_fails(Xx28,Xx29,Xx30))), file('theBenchmark.p',id16)).
% 238.07/32.44 fof(id47, axiom, ! [Xx1,Xx2,Xx3] : (member2_fails(Xx1,Xx2,Xx3) <=> (member_fails(Xx1,Xx3) & member_fails(Xx1,Xx2))), file('theBenchmark.p',id47)).
% 238.07/32.44 fof(id53, axiom, ! [Xx1,Xx2] : (not_same_occ_fails(Xx1,Xx2) <=> ! [Xx3,Xx4,Xx5] : (member2_fails(Xx3,Xx1,Xx2) | occ_fails(Xx3,Xx1,Xx4) | occ_fails(Xx3,Xx2,Xx5) | Xx4 = Xx5)), file('theBenchmark.p',id53)).
% 238.07/32.44 fof(id55, axiom, ! [Xx1,Xx2] : (same_occ_succeeds(Xx1,Xx2) <=> not_same_occ_fails(Xx1,Xx2)), file('theBenchmark.p',id55)).
% 238.07/32.44 fof(occ/2, axiom, ! [Xx,Xl,Xm] : (list_succeeds(Xl) => (occ(Xx,Xl) = Xm <=> occ_succeeds(Xx,Xl,Xm))), file('theBenchmark.p',occ/2)).
% 238.07/32.44 fof('lemma-(occ:existence)', axiom, ! [Xx,Xl] : (list_succeeds(Xl) => ? [Xn] : occ_succeeds(Xx,Xl,Xn)), file('theBenchmark.p','lemma-(occ:existence)')).
% 238.07/32.44 fof('lemma-(occ:member)', axiom, ! [Xx,Xl] : ((list_succeeds(Xl) & member_fails(Xx,Xl)) => occ(Xx,Xl) ='0'), file('theBenchmark.p','lemma-(occ:member)')).
% 238.07/32.44 fof('lemma-(same_occ:success)', conjecture, ! [Xl1,Xl2] : ((list_succeeds(Xl1) & list_succeeds(Xl2) & same_occ_succeeds(Xl1,Xl2)) => ! [Xx] : occ(Xx,Xl1) = occ(Xx,Xl2)), file('theBenchmark.p','lemma-(same_occ:success)')).
% 238.07/32.44 fof('lemma-(same_occ:success)_neg', negated_conjecture, ~(! [Xl1,Xl2] : ((list_succeeds(Xl1) & list_succeeds(Xl2) & same_occ_succeeds(Xl1,Xl2)) => ! [Xx] : occ(Xx,Xl1) = occ(Xx,Xl2))), inference(assume_negation, [status(cth)], ['lemma-(same_occ:success)'])).
% 238.07/32.44 cnf(c_568, plain, ~occ_succeeds(A,B,C) | ~occ_fails(A,B,C), inference(clausify, [status(thm)], [id16])).
% 238.07/32.44 cnf(c_579, plain, ~member2_fails(A,B,C) | member_fails(A,C), inference(clausify, [status(thm)], [id47])).
% 238.07/32.44 cnf(c_580, plain, ~member2_fails(A,B,C) | member_fails(A,B), inference(clausify, [status(thm)], [id47])).
% 238.07/32.44 cnf(c_686, plain, ~not_same_occ_fails(A,B) | member2_fails(C,A,B) | occ_fails(C,A,D) | occ_fails(C,B,E) | E = D, inference(clausify, [status(thm)], [id53])).
% 238.07/32.44 cnf(c_700, plain, ~same_occ_succeeds(A,B) | not_same_occ_fails(A,B), inference(clausify, [status(thm)], [id55])).
% 238.07/32.44 fof('axiom-(lh:nil)', axiom, (lh(nil) ='0'), file('theBenchmark.p','axiom-(lh:nil)')).
% 238.07/32.44 cnf(c_924, plain, lh(nil) ='0', inference(clausify, [status(thm)], ['axiom-(lh:nil)'])).
% 238.07/32.44 cnf(c_925, plain, '0' = lh(nil),
% 238.07/32.44 inference(copy, [status(thm)], [c_924])).
% 238.07/32.44 cnf(c_974, plain, ~list_succeeds(A) | occ(B,A) != C | occ_succeeds(B,A,C), inference(clausify, [status(thm)], [occ/2])).
% 238.07/32.44 cnf(c_975, plain, ~list_succeeds(A) | occ(B,A) = C | ~occ_succeeds(B,A,C), inference(clausify, [status(thm)], [occ/2])).
% 238.07/32.44 fof(nnf_197, plain, ! [Xx,Xl] : (~ (list_succeeds(Xl)) | ? [Xn] : occ_succeeds(Xx,Xl,Xn)), inference(fof_nnf, [status(thm)], ['lemma-(occ:existence)'])).
% 238.07/32.44 fof('sk_lemma-(occ:existence)', plain, ! [Xx,Xl] : (~ (list_succeeds(Xl)) | occ_succeeds(Xx,Xl,sK0(Xx,Xl))), inference(skolemize, [status(esa), new_symbols(skolem, [sK0]), skolemize(Xn,sK0(Xx,Xl))], [nnf_197])).
% 238.07/32.44 cnf(c_986, plain, ~list_succeeds(A) | occ_succeeds(B,A,sK0(B,A)), inference(split_conjunct, [status(thm)], ['sk_lemma-(occ:existence)'])).
% 238.07/32.44 cnf(c_1005, plain, ~list_succeeds(A) | ~member_fails(B,A) | occ(B,A) ='0', inference(clausify, [status(thm)], ['lemma-(occ:member)'])).
% 238.07/32.44 cnf(c_1006, plain, ~list_succeeds(A) | ~member_fails(B,A) | occ(B,A) = lh(nil),
% 238.07/32.44 inference(paramod, [status(thm)], [c_925, c_1005])).
% 238.07/32.44 fof(nnf_297, plain, ? [Xl1,Xl2] : (list_succeeds(Xl1) & list_succeeds(Xl2) & same_occ_succeeds(Xl1,Xl2) & ? [Xx] : ~ (occ(Xx,Xl2) = occ(Xx,Xl1))), inference(fof_nnf, [status(thm)], ['lemma-(same_occ:success)_neg'])).
% 238.07/32.44 fof('sk_lemma-(same_occ:success)_neg', plain, (list_succeeds(sK1) & list_succeeds(sK2) & same_occ_succeeds(sK1,sK2) & ~ (occ(sK3,sK2) = occ(sK3,sK1))), inference(skolemize, [status(esa), new_symbols(skolem, [sK1,sK2,sK3]), skolemize(Xl1,sK1), skolemize(Xl2,sK2), skolemize(Xx,sK3)], [nnf_297])).
% 238.07/32.44 cnf(c_1014, negated_conjecture, list_succeeds(sK1), inference(split_conjunct, [status(thm)], ['sk_lemma-(same_occ:success)_neg'])).
% 238.07/32.44 cnf(c_1015, negated_conjecture, list_succeeds(sK2), inference(split_conjunct, [status(thm)], ['sk_lemma-(same_occ:success)_neg'])).
% 238.07/32.44 cnf(c_1016, negated_conjecture, same_occ_succeeds(sK1,sK2), inference(split_conjunct, [status(thm)], ['sk_lemma-(same_occ:success)_neg'])).
% 238.07/32.44 cnf(c_1017, negated_conjecture, occ(sK3,sK2) != occ(sK3,sK1), inference(split_conjunct, [status(thm)], ['sk_lemma-(same_occ:success)_neg'])).
% 238.07/32.44 cnf(c_1238, plain, not_same_occ_fails(sK1,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_700, c_1016])).
% 238.07/32.44 cnf(c_1628, plain, member2_fails(A,sK1,sK2) | occ_fails(A,sK1,B) | occ_fails(A,sK2,C) | C = B,
% 238.07/32.44 inference(resolve, [status(thm)], [c_686, c_1238])).
% 238.07/32.44 cnf(c_4971, plain, occ(A,sK1) != B | occ_succeeds(A,sK1,B),
% 238.07/32.44 inference(resolve, [status(thm)], [c_974, c_1014])).
% 238.07/32.44 cnf(c_5288, plain, occ_succeeds(A,sK2,sK0(A,sK2)),
% 238.07/32.44 inference(resolve, [status(thm)], [c_986, c_1015])).
% 238.07/32.44 cnf(c_5289, plain, occ_succeeds(A,sK1,sK0(A,sK1)),
% 238.07/32.44 inference(resolve, [status(thm)], [c_986, c_1014])).
% 238.07/32.44 cnf(c_25347, plain, ~list_succeeds(sK2) | occ(A,sK2) = sK0(A,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_5288, c_975])).
% 238.07/32.44 cnf(c_25348, plain, ~list_succeeds(sK2) | sK0(A,sK2) = occ(A,sK2),
% 238.07/32.44 inference(copy, [status(thm)], [c_25347])).
% 238.07/32.44 cnf(c_5379, negated_conjecture, sK0(A,sK2) = occ(A,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_1015, c_25348])).
% 238.07/32.44 cnf(c_5392, plain, occ_succeeds(A,sK2,occ(A,sK2)),
% 238.07/32.44 inference(paramod, [status(thm)], [c_5379, c_5288])).
% 238.07/32.44 cnf(c_25349, plain, ~list_succeeds(sK1) | occ(A,sK1) = sK0(A,sK1),
% 238.07/32.44 inference(resolve, [status(thm)], [c_5289, c_975])).
% 238.07/32.44 cnf(c_25350, plain, ~list_succeeds(sK1) | sK0(A,sK1) = occ(A,sK1),
% 238.07/32.44 inference(copy, [status(thm)], [c_25349])).
% 238.07/32.44 cnf(c_5396, negated_conjecture, sK0(A,sK1) = occ(A,sK1),
% 238.07/32.44 inference(resolve, [status(thm)], [c_1014, c_25350])).
% 238.07/32.44 cnf(c_5409, plain, occ_succeeds(A,sK1,occ(A,sK1)),
% 238.07/32.44 inference(paramod, [status(thm)], [c_5396, c_5289])).
% 238.07/32.44 cnf(c_6466, plain, occ_fails(A,sK1,B) | occ_fails(A,sK2,C) | C = B | member_fails(A,sK1),
% 238.07/32.44 inference(resolve, [status(thm)], [c_1628, c_580])).
% 238.07/32.44 cnf(c_6467, plain, occ_fails(A,sK1,B) | occ_fails(A,sK2,C) | C = B | member_fails(A,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_1628, c_579])).
% 238.07/32.44 cnf(c_6473, plain, occ_fails(A,sK2,B) | B = C | member_fails(A,sK1) | ~occ_succeeds(A,sK1,C),
% 238.07/32.44 inference(resolve, [status(thm)], [c_6466, c_568])).
% 238.07/32.44 cnf(c_6495, plain, occ_fails(A,sK1,B) | C = B | member_fails(A,sK2) | ~occ_succeeds(A,sK2,C),
% 238.07/32.44 inference(resolve, [status(thm)], [c_6467, c_568])).
% 238.07/32.44 cnf(c_25351, plain, occ_fails(A,sK2,B) | B = occ(A,sK1) | member_fails(A,sK1),
% 238.07/32.44 inference(resolve, [status(thm)], [c_6473, c_5409])).
% 238.07/32.44 cnf(c_6500, plain, occ_fails(A,sK2,B) | occ(A,sK1) = B | member_fails(A,sK1),
% 238.07/32.44 inference(copy, [status(thm)], [c_25351])).
% 238.07/32.44 cnf(c_6503, plain, occ_fails(A,sK1,B) | occ(A,sK2) = B | member_fails(A,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_6495, c_5392])).
% 238.07/32.44 cnf(c_18962, plain, occ(A,sK1) = B | member_fails(A,sK1) | ~occ_succeeds(A,sK2,B),
% 238.07/32.44 inference(resolve, [status(thm)], [c_6500, c_568])).
% 238.07/32.44 cnf(c_18968, plain, occ(A,sK2) = B | member_fails(A,sK2) | ~occ_succeeds(A,sK1,B),
% 238.07/32.44 inference(resolve, [status(thm)], [c_6503, c_568])).
% 238.07/32.44 cnf(c_25352, plain, occ(A,sK1) = occ(A,sK2) | member_fails(A,sK1),
% 238.07/32.44 inference(resolve, [status(thm)], [c_18962, c_5392])).
% 238.07/32.44 cnf(c_21420, plain, occ(A,sK2) = occ(A,sK1) | member_fails(A,sK1),
% 238.07/32.44 inference(copy, [status(thm)], [c_25352])).
% 238.07/32.44 cnf(c_25353, plain, occ(A,sK2) = occ(A,sK1) | ~list_succeeds(sK1) | occ(A,sK1) = lh(nil),
% 238.07/32.44 inference(resolve, [status(thm)], [c_21420, c_1006])).
% 238.07/32.44 cnf(c_21430, negated_conjecture, occ(A,sK2) = occ(A,sK1) | occ(A,sK1) = lh(nil),
% 238.07/32.44 inference(resolve, [status(thm)], [c_1014, c_25353])).
% 238.07/32.44 cnf(c_25318, plain, occ(sK3,sK1) = lh(nil),
% 238.07/32.44 inference(resolve, [status(thm)], [c_21430, c_1017])).
% 238.07/32.44 cnf(c_25325, negated_conjecture, occ(sK3,sK2) != lh(nil),
% 238.07/32.44 inference(paramod, [status(thm)], [c_25318, c_1017])).
% 238.07/32.44 cnf(c_25326, plain, occ_succeeds(sK3,sK1,lh(nil)),
% 238.07/32.44 inference(resolve, [status(thm)], [c_25318, c_4971])).
% 238.07/32.44 cnf(c_25354, plain, occ(sK3,sK2) = lh(nil) | member_fails(sK3,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_25326, c_18968])).
% 238.07/32.44 cnf(c_25327, negated_conjecture, member_fails(sK3,sK2),
% 238.07/32.44 inference(resolve, [status(thm)], [c_25325, c_25354])).
% 238.07/32.44 cnf(c_25355, plain, ~list_succeeds(sK2) | occ(sK3,sK2) = lh(nil),
% 238.07/32.44 inference(resolve, [status(thm)], [c_25327, c_1006])).
% 238.07/32.44 cnf(c_25356, negated_conjecture, occ(sK3,sK2) = lh(nil),
% 238.07/32.44 inference(resolve, [status(thm)], [c_1015, c_25355])).
% 238.07/32.44 cnf(c_25346, negated_conjecture, $false,
% 238.07/32.44 inference(resolve, [status(thm)], [c_25325, c_25356])).
% 238.07/32.44 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------