%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX187+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 29 02:38:02 PM UTC 2026 % Result : Theorem 0.87s 1.18s % Output : Refutation 0.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX187+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.33 % Computer : n014.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue Apr 28 23:33:50 EDT 2026 % 0.15/0.33 % CPUTime : % 0.43/0.99 ============================== Prover9 =============================== % 0.43/0.99 Prover9 (32) version 2009-11A, November 2009. % 0.43/0.99 Process 5275 was started by sandbox2 on n014.cluster.edu, % 0.43/0.99 Tue Apr 28 23:33:51 2026 % 0.43/0.99 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_5121_n014.cluster.edu". % 0.43/0.99 ============================== end of head =========================== % 0.43/0.99 % 0.43/0.99 ============================== INPUT ================================= % 0.43/0.99 % 0.43/0.99 % Reading from file /tmp/Prover9_5121_n014.cluster.edu % 0.43/0.99 % 0.43/0.99 set(prolog_style_variables). % 0.43/0.99 set(auto2). % 0.43/0.99 % set(auto2) -> set(auto). % 0.43/0.99 % set(auto) -> set(auto_inference). % 0.43/0.99 % set(auto) -> set(auto_setup). % 0.43/0.99 % set(auto_setup) -> set(predicate_elim). % 0.43/0.99 % set(auto_setup) -> assign(eq_defs, unfold). % 0.43/0.99 % set(auto) -> set(auto_limits). % 0.43/0.99 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.43/0.99 % set(auto_limits) -> assign(sos_limit, 20000). % 0.43/0.99 % set(auto) -> set(auto_denials). % 0.43/0.99 % set(auto) -> set(auto_process). % 0.43/0.99 % set(auto2) -> assign(new_constants, 1). % 0.43/0.99 % set(auto2) -> assign(fold_denial_max, 3). % 0.43/0.99 % set(auto2) -> assign(max_weight, "200.000"). % 0.43/0.99 % set(auto2) -> assign(max_hours, 1). % 0.43/0.99 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.43/0.99 % set(auto2) -> assign(max_seconds, 0). % 0.43/0.99 % set(auto2) -> assign(max_minutes, 5). % 0.43/0.99 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.43/0.99 % set(auto2) -> set(sort_initial_sos). % 0.43/0.99 % set(auto2) -> assign(sos_limit, -1). % 0.43/0.99 % set(auto2) -> assign(lrs_ticks, 3000). % 0.43/0.99 % set(auto2) -> assign(max_megs, 400). % 0.43/0.99 % set(auto2) -> assign(stats, some). % 0.43/0.99 % set(auto2) -> clear(echo_input). % 0.43/0.99 % set(auto2) -> set(quiet). % 0.43/0.99 % set(auto2) -> clear(print_initial_clauses). % 0.43/0.99 % set(auto2) -> clear(print_given). % 0.43/0.99 assign(lrs_ticks,-1). % 0.43/0.99 assign(sos_limit,10000). % 0.43/0.99 assign(order,kbo). % 0.43/0.99 set(lex_order_vars). % 0.43/0.99 clear(print_given). % 0.43/0.99 % 0.43/0.99 % formulas(sos). % not echoed (17 formulas) % 0.43/0.99 % 0.43/0.99 ============================== end of input ========================== % 0.43/0.99 % 0.43/0.99 % From the command line: assign(max_seconds, 300). % 0.43/0.99 % 0.43/0.99 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.43/0.99 % 0.43/0.99 % Formulas that are not ordinary clauses: % 0.43/0.99 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 4 (all X proj1S(s(X)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 5 (all X s(X) != z) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 6 (all Y all Xs length(cons(Y,Xs)) = s(length(Xs))) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 7 (all Z all Y2 (x2(s(Z),s(Y2)) <-> x2(Z,Y2))) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 8 (all Z -x2(s(Z),z)) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 9 (all X2 x2(z,s(X2))) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 10 (all Y x(nil,Y) = Y) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 11 (all Y all Z all Xs x(cons(Z,Xs),Y) = cons(Z,x(Xs,Y))) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 12 (all Z rotate(s(Z),nil) = nil) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 13 (all Z all X2 all X3 rotate(s(Z),cons(X2,X3)) = rotate(Z,x(X3,cons(X2,nil)))) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 14 (all Y rotate(z,Y) = Y) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.43/0.99 15 -(exists N exists M exists Ys exists Xs -(x2(N,length(Xs)) -> (x2(M,length(Ys)) -> (Xs = Ys -> (rotate(s(z),Xs) != Xs -> (rotate(N,Xs) = rotate(M,Ys) -> N = M)))))) # label(goal_017) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.43/0.99 % 0.43/0.99 ============================== end of process non-clausal formulas === % 0.43/0.99 % 0.43/0.99 ============================== PROCESS INITIAL CLAUSES =============== % 0.43/0.99 % 0.43/0.99 ============================== PREDICATE ELIMINATION ================= % 0.87/1.18 % 0.87/1.18 ============================== end predicate elimination ============= % 0.87/1.18 % 0.87/1.18 Auto_denials: (non-Horn, no changes). % 0.87/1.18 % 0.87/1.18 Term ordering decisions: % 0.87/1.18 Function symbol KB weights: nil=1. z=1. cons=1. rotate=1. x=1. s=1. length=1. head=1. proj1S=1. tail=1. % 0.87/1.18 % 0.87/1.18 ============================== end of process initial clauses ======== % 0.87/1.18 % 0.87/1.18 ============================== CLAUSES FOR SEARCH ==================== % 0.87/1.18 % 0.87/1.18 ============================== end of clauses for search ============= % 0.87/1.18 % 0.87/1.18 ============================== SEARCH ================================ % 0.87/1.18 % 0.87/1.18 % Starting search at 0.01 seconds. % 0.87/1.18 % 0.87/1.18 ============================== PROOF ================================= % 0.87/1.18 % SZS status Theorem % 0.87/1.18 % SZS output start Refutation % 0.87/1.18 % 0.87/1.18 % Proof 1 at 0.20 (+ 0.00) seconds. % 0.87/1.18 % Length of proof is 46. % 0.87/1.18 % Level of proof is 15. % 0.87/1.18 % Maximum clause weight is 44.000. % 0.87/1.18 % Given clauses 232. % 0.87/1.18 % 0.87/1.18 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 5 (all X s(X) != z) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 6 (all Y all Xs length(cons(Y,Xs)) = s(length(Xs))) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 7 (all Z all Y2 (x2(s(Z),s(Y2)) <-> x2(Z,Y2))) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 9 (all X2 x2(z,s(X2))) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 10 (all Y x(nil,Y) = Y) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 11 (all Y all Z all Xs x(cons(Z,Xs),Y) = cons(Z,x(Xs,Y))) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 13 (all Z all X2 all X3 rotate(s(Z),cons(X2,X3)) = rotate(Z,x(X3,cons(X2,nil)))) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 14 (all Y rotate(z,Y) = Y) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.87/1.18 15 -(exists N exists M exists Ys exists Xs -(x2(N,length(Xs)) -> (x2(M,length(Ys)) -> (Xs = Ys -> (rotate(s(z),Xs) != Xs -> (rotate(N,Xs) = rotate(M,Ys) -> N = M)))))) # label(goal_017) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.87/1.18 16 length(nil) = z # label(axiom_006) # label(axiom). [assumption]. % 0.87/1.18 17 z = length(nil). [copy(16),flip(a)]. % 0.87/1.18 18 x2(z,s(A)) # label(axiom_010) # label(axiom). [clausify(9)]. % 0.87/1.18 19 x2(length(nil),s(A)). [copy(18),rewrite([17(1)])]. % 0.87/1.18 21 x(nil,A) = A # label(axiom_012) # label(axiom). [clausify(10)]. % 0.87/1.18 22 rotate(z,A) = A # label(axiom_016) # label(axiom). [clausify(14)]. % 0.87/1.18 23 rotate(length(nil),A) = A. [copy(22),rewrite([17(1)])]. % 0.87/1.18 24 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.87/1.18 27 length(cons(A,B)) = s(length(B)) # label(axiom_007) # label(axiom). [clausify(6)]. % 0.87/1.18 28 x(cons(A,B),C) = cons(A,x(B,C)) # label(axiom_013) # label(axiom). [clausify(11)]. % 0.87/1.18 29 rotate(s(A),cons(B,C)) = rotate(A,x(C,cons(B,nil))) # label(axiom_015) # label(axiom). [clausify(13)]. % 0.87/1.18 30 rotate(A,x(B,cons(C,nil))) = rotate(s(A),cons(C,B)). [copy(29),flip(a)]. % 0.87/1.18 33 s(A) != z # label(axiom_005) # label(axiom). [clausify(5)]. % 0.87/1.18 34 length(nil) != s(A). [copy(33),rewrite([17(2)]),flip(a)]. % 0.87/1.18 37 cons(A,B) != nil # label(axiom_003) # label(axiom). [clausify(3)]. % 0.87/1.18 39 x2(s(A),s(B)) | -x2(A,B) # label(axiom_008) # label(axiom). [clausify(7)]. % 0.87/1.18 40 -x2(A,length(B)) | -x2(C,length(D)) | D != B | rotate(s(z),B) = B | rotate(C,D) != rotate(A,B) | C = A # label(goal_017) # label(negated_conjecture). [clausify(15)]. % 0.87/1.18 41 -x2(A,length(B)) | -x2(C,length(D)) | D != B | rotate(s(length(nil)),B) = B | rotate(C,D) != rotate(A,B) | C = A. [copy(40),rewrite([17(6)])]. % 0.87/1.18 44 rotate(s(length(nil)),cons(A,B)) = x(B,cons(A,nil)). [para(30(a,1),23(a,1))]. % 0.87/1.18 45 rotate(A,cons(B,x(C,cons(D,nil)))) = rotate(s(A),cons(D,cons(B,C))). [para(28(a,1),30(a,1,2))]. % 0.87/1.18 48 x2(s(length(nil)),s(s(A))). [resolve(39,b,19,a)]. % 0.87/1.18 49 -x2(A,s(length(B))) | -x2(C,length(D)) | cons(E,B) != D | x(B,cons(E,nil)) = cons(E,B) | rotate(A,cons(E,B)) != rotate(C,D) | C = A. [para(27(a,1),41(a,2)),rewrite([44(12)]),flip(c),flip(e)]. % 0.87/1.18 58 x2(s(s(length(nil))),s(s(s(A)))). [resolve(48,a,39,b)]. % 0.87/1.18 64 rotate(s(s(length(nil))),cons(A,cons(B,C))) = x(x(C,cons(A,nil)),cons(B,nil)). [para(45(a,1),44(a,1))]. % 0.87/1.18 74 -x2(A,length(B)) | cons(C,D) != B | x(D,cons(C,nil)) = cons(C,D) | rotate(A,B) != cons(C,D) | length(nil) = A. [resolve(49,a,19,a),rewrite([23(13)]),flip(d),flip(e)]. % 0.87/1.18 133 -x2(A,s(length(B))) | cons(C,D) != cons(E,B) | x(D,cons(C,nil)) = cons(C,D) | rotate(A,cons(E,B)) != cons(C,D) | length(nil) = A. [para(27(a,1),74(a,2))]. % 0.87/1.18 175 -x2(A,s(s(length(B)))) | cons(C,cons(D,B)) != cons(E,F) | x(F,cons(E,nil)) = cons(E,F) | rotate(A,cons(C,cons(D,B))) != cons(E,F) | length(nil) = A. [para(27(a,1),133(a,2,1)),flip(b)]. % 0.87/1.18 240 -x2(A,s(s(s(length(B))))) | cons(C,cons(D,cons(E,B))) != cons(F,V6) | x(V6,cons(F,nil)) = cons(F,V6) | rotate(A,cons(C,cons(D,cons(E,B)))) != cons(F,V6) | length(nil) = A. [para(27(a,1),175(a,2,1,1))]. % 0.87/1.18 428 cons(A,cons(B,cons(C,D))) != cons(E,F) | x(F,cons(E,nil)) = cons(E,F) | cons(C,x(x(D,cons(A,nil)),cons(B,nil))) != cons(E,F). [resolve(240,a,58,a),rewrite([64(18),28(14),28(17)]),flip(d),unit_del(d(flip),34)]. % 0.87/1.18 431 cons(A,cons(B,cons(C,cons(D,E)))) != cons(F,V6) | x(V6,cons(F,nil)) = cons(F,V6) | cons(C,cons(D,x(x(E,cons(A,nil)),cons(B,nil)))) != cons(F,V6). [para(28(a,1),428(c,1,2,1)),rewrite([28(18)])]. % 0.87/1.18 437 cons(A,cons(B,cons(C,cons(D,nil)))) != cons(E,F) | x(F,cons(E,nil)) = cons(E,F) | cons(C,cons(D,cons(A,cons(B,nil)))) != cons(E,F). [para(21(a,1),431(c,1,2,2,1)),rewrite([28(17),21(16)])]. % 0.87/1.18 443 cons(A,cons(B,cons(A,cons(B,nil)))) != cons(C,D) | x(D,cons(C,nil)) = cons(C,D). [factor(437,a,c)]. % 0.87/1.18 444 cons(A,cons(B,cons(A,cons(B,nil)))) = cons(B,cons(A,cons(B,cons(A,nil)))). [xx_res(443,a),rewrite([28(7),28(6),28(5),21(4)])]. % 0.87/1.18 449 A = B. [para(444(a,1),24(a,1,1)),rewrite([24(6)])]. % 0.87/1.18 450 $F. [resolve(449,a,37,a)]. % 0.87/1.18 % 0.87/1.18 % SZS output end Refutation % 0.87/1.18 ============================== end of proof ========================== % 0.87/1.18 % 0.87/1.18 ============================== STATISTICS ============================ % 0.87/1.18 % 0.87/1.18 Given=232. Generated=1397. Kept=426. proofs=1. % 0.87/1.18 Usable=231. Sos=170. Demods=78. Limbo=0, Disabled=42. Hints=0. % 0.87/1.18 Megabytes=1.41. % 0.87/1.18 User_CPU=0.20, System_CPU=0.00, Wall_clock=0. % 0.87/1.18 % 0.87/1.18 ============================== end of statistics ===================== % 0.87/1.18 % 0.87/1.18 ============================== end of search ========================= % 0.87/1.18 % 0.87/1.18 THEOREM PROVED % 0.87/1.18 % SZS status Theorem % 0.87/1.18 % 0.87/1.18 Exiting with 1 proof. % 0.87/1.18 % 0.87/1.18 Process 5275 exit (max_proofs) Tue Apr 28 23:33:51 2026 % 0.87/1.18 Prover9 interrupted %------------------------------------------------------------------------------