%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX203+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n010.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:04 PM UTC 2026 % Result : Theorem 0.73s 1.53s % Output : Refutation 0.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX203+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.32 % Computer : n010.cluster.edu % 0.15/0.32 % Model : x86_64 x86_64 % 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.32 % Memory : 8042.1875MB % 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.32 % CPULimit : 300 % 0.15/0.32 % WCLimit : 300 % 0.15/0.32 % DateTime : Wed Apr 29 00:47:20 EDT 2026 % 0.15/0.32 % CPUTime : % 0.43/1.01 ============================== Prover9 =============================== % 0.43/1.01 Prover9 (32) version 2009-11A, November 2009. % 0.43/1.01 Process 17442 was started by sandbox on n010.cluster.edu, % 0.43/1.01 Wed Apr 29 00:47:21 2026 % 0.43/1.01 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_17108_n010.cluster.edu". % 0.43/1.01 ============================== end of head =========================== % 0.43/1.01 % 0.43/1.01 ============================== INPUT ================================= % 0.43/1.01 % 0.43/1.01 % Reading from file /tmp/Prover9_17108_n010.cluster.edu % 0.43/1.01 % 0.43/1.01 set(prolog_style_variables). % 0.43/1.01 set(auto2). % 0.43/1.01 % set(auto2) -> set(auto). % 0.43/1.01 % set(auto) -> set(auto_inference). % 0.43/1.01 % set(auto) -> set(auto_setup). % 0.43/1.01 % set(auto_setup) -> set(predicate_elim). % 0.43/1.01 % set(auto_setup) -> assign(eq_defs, unfold). % 0.43/1.01 % set(auto) -> set(auto_limits). % 0.43/1.01 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.43/1.01 % set(auto_limits) -> assign(sos_limit, 20000). % 0.43/1.01 % set(auto) -> set(auto_denials). % 0.43/1.01 % set(auto) -> set(auto_process). % 0.43/1.01 % set(auto2) -> assign(new_constants, 1). % 0.43/1.01 % set(auto2) -> assign(fold_denial_max, 3). % 0.43/1.01 % set(auto2) -> assign(max_weight, "200.000"). % 0.43/1.01 % set(auto2) -> assign(max_hours, 1). % 0.43/1.01 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.43/1.01 % set(auto2) -> assign(max_seconds, 0). % 0.43/1.01 % set(auto2) -> assign(max_minutes, 5). % 0.43/1.01 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.43/1.01 % set(auto2) -> set(sort_initial_sos). % 0.43/1.01 % set(auto2) -> assign(sos_limit, -1). % 0.43/1.01 % set(auto2) -> assign(lrs_ticks, 3000). % 0.43/1.01 % set(auto2) -> assign(max_megs, 400). % 0.43/1.01 % set(auto2) -> assign(stats, some). % 0.43/1.01 % set(auto2) -> clear(echo_input). % 0.43/1.01 % set(auto2) -> set(quiet). % 0.43/1.01 % set(auto2) -> clear(print_initial_clauses). % 0.43/1.01 % set(auto2) -> clear(print_given). % 0.43/1.01 assign(lrs_ticks,-1). % 0.43/1.01 assign(sos_limit,10000). % 0.43/1.01 assign(order,kbo). % 0.43/1.01 set(lex_order_vars). % 0.43/1.01 clear(print_given). % 0.43/1.01 % 0.43/1.01 % formulas(sos). % not echoed (22 formulas) % 0.43/1.01 % 0.43/1.01 ============================== end of input ========================== % 0.43/1.01 % 0.43/1.01 % From the command line: assign(max_seconds, 300). % 0.43/1.01 % 0.43/1.01 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.43/1.01 % 0.43/1.01 % Formulas that are not ordinary clauses: % 0.43/1.01 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 4 (all X proj1S(s(X)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 5 (all X z != s(X)) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 6 (all Y leqNat(z,Y)) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 7 (all Z -leqNat(s(Z),z)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 8 (all Z all M (leqNat(s(Z),s(M)) <-> leqNat(Z,M))) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 9 (all Y sorted(cons(Y,nil))) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 10 (all Y all Y2 all Xs (sorted(cons(Y,cons(Y2,Xs))) <-> leqNat(Y,Y2) & sorted(cons(Y2,Xs)))) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 11 (all Y all Xs lengthNat(cons(Y,Xs)) = s(lengthNat(Xs))) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 12 (all X -elemNat(X,nil)) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 13 (all X all Z all Xs (elemNat(X,cons(Z,Xs)) <-> X = Z | elemNat(X,Xs))) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 14 (all Y all Xs (unique(cons(Y,Xs)) <-> -elemNat(Y,Xs) & unique(Xs))) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 15 (all Y append(nil,Y) = Y) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.01 17 (all Y all Xs rev(cons(Y,Xs)) = append(rev(Xs),cons(Y,nil))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 18 -(exists Xs -(sorted(rev(Xs)) -> (unique(Xs) -> leqNat(lengthNat(Xs),s(s(s(z))))))) # label(goal_022) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.73/1.53 % 0.73/1.53 ============================== end of process non-clausal formulas === % 0.73/1.53 % 0.73/1.53 ============================== PROCESS INITIAL CLAUSES =============== % 0.73/1.53 % 0.73/1.53 ============================== PREDICATE ELIMINATION ================= % 0.73/1.53 % 0.73/1.53 ============================== end predicate elimination ============= % 0.73/1.53 % 0.73/1.53 Auto_denials: (non-Horn, no changes). % 0.73/1.53 % 0.73/1.53 Term ordering decisions: % 0.73/1.53 Function symbol KB weights: nil=1. z=1. cons=1. append=1. s=1. lengthNat=1. rev=1. head=1. proj1S=1. tail=1. % 0.73/1.53 % 0.73/1.53 ============================== end of process initial clauses ======== % 0.73/1.53 % 0.73/1.53 ============================== CLAUSES FOR SEARCH ==================== % 0.73/1.53 % 0.73/1.53 ============================== end of clauses for search ============= % 0.73/1.53 % 0.73/1.53 ============================== SEARCH ================================ % 0.73/1.53 % 0.73/1.53 % Starting search at 0.01 seconds. % 0.73/1.53 % 0.73/1.53 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 239 (0.00 of 0.15 sec). % 0.73/1.53 % 0.73/1.53 ============================== PROOF ================================= % 0.73/1.53 % SZS status Theorem % 0.73/1.53 % SZS output start Refutation % 0.73/1.53 % 0.73/1.53 % Proof 1 at 0.52 (+ 0.02) seconds. % 0.73/1.53 % Length of proof is 100. % 0.73/1.53 % Level of proof is 24. % 0.73/1.53 % Maximum clause weight is 46.000. % 0.73/1.53 % Given clauses 953. % 0.73/1.53 % 0.73/1.53 4 (all X proj1S(s(X)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 5 (all X z != s(X)) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 6 (all Y leqNat(z,Y)) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 7 (all Z -leqNat(s(Z),z)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 8 (all Z all M (leqNat(s(Z),s(M)) <-> leqNat(Z,M))) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 9 (all Y sorted(cons(Y,nil))) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 10 (all Y all Y2 all Xs (sorted(cons(Y,cons(Y2,Xs))) <-> leqNat(Y,Y2) & sorted(cons(Y2,Xs)))) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 11 (all Y all Xs lengthNat(cons(Y,Xs)) = s(lengthNat(Xs))) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 12 (all X -elemNat(X,nil)) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 13 (all X all Z all Xs (elemNat(X,cons(Z,Xs)) <-> X = Z | elemNat(X,Xs))) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 14 (all Y all Xs (unique(cons(Y,Xs)) <-> -elemNat(Y,Xs) & unique(Xs))) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 15 (all Y append(nil,Y) = Y) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 16 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 17 (all Y all Xs rev(cons(Y,Xs)) = append(rev(Xs),cons(Y,nil))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.73/1.53 18 -(exists Xs -(sorted(rev(Xs)) -> (unique(Xs) -> leqNat(lengthNat(Xs),s(s(s(z))))))) # label(goal_022) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.73/1.53 20 unique(nil) # label(axiom_016) # label(axiom). [assumption]. % 0.73/1.53 21 leqNat(z,A) # label(axiom_006) # label(axiom). [clausify(6)]. % 0.73/1.53 22 sorted(cons(A,nil)) # label(axiom_010) # label(axiom). [clausify(9)]. % 0.73/1.53 23 lengthNat(nil) = z # label(axiom_012) # label(axiom). [assumption]. % 0.73/1.53 24 z = lengthNat(nil). [copy(23),flip(a)]. % 0.73/1.53 25 rev(nil) = nil # label(axiom_020) # label(axiom). [assumption]. % 0.73/1.53 26 proj1S(s(A)) = A # label(axiom_004) # label(axiom). [clausify(4)]. % 0.73/1.53 27 append(nil,A) = A # label(axiom_018) # label(axiom). [clausify(15)]. % 0.73/1.53 30 lengthNat(cons(A,B)) = s(lengthNat(B)) # label(axiom_013) # label(axiom). [clausify(11)]. % 0.73/1.53 31 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_019) # label(axiom). [clausify(16)]. % 0.73/1.53 32 rev(cons(A,B)) = append(rev(B),cons(A,nil)) # label(axiom_021) # label(axiom). [clausify(17)]. % 0.73/1.53 33 append(rev(A),cons(B,nil)) = rev(cons(B,A)). [copy(32),flip(a)]. % 0.73/1.53 34 -elemNat(A,nil) # label(axiom_014) # label(axiom). [clausify(12)]. % 0.73/1.53 35 s(A) != z # label(axiom_005) # label(axiom). [clausify(5)]. % 0.73/1.53 36 lengthNat(nil) != s(A). [copy(35),rewrite([24(2)]),flip(a)]. % 0.73/1.53 37 -leqNat(s(A),z) # label(axiom_007) # label(axiom). [clausify(7)]. % 0.73/1.53 38 -leqNat(s(A),lengthNat(nil)). [copy(37),rewrite([24(2)])]. % 0.73/1.53 42 -leqNat(s(A),s(B)) | leqNat(A,B) # label(axiom_008) # label(axiom). [clausify(8)]. % 0.73/1.53 43 leqNat(s(A),s(B)) | -leqNat(A,B) # label(axiom_008) # label(axiom). [clausify(8)]. % 0.73/1.53 46 -sorted(cons(A,cons(B,C))) | leqNat(A,B) # label(axiom_011) # label(axiom). [clausify(10)]. % 0.73/1.53 47 unique(cons(A,B)) | elemNat(A,B) | -unique(B) # label(axiom_017) # label(axiom). [clausify(14)]. % 0.73/1.53 48 -sorted(cons(A,cons(B,C))) | sorted(cons(B,C)) # label(axiom_011) # label(axiom). [clausify(10)]. % 0.73/1.53 49 -elemNat(A,cons(B,C)) | B = A | elemNat(A,C) # label(axiom_015) # label(axiom). [clausify(13)]. % 0.73/1.53 50 -sorted(rev(A)) | -unique(A) | leqNat(lengthNat(A),s(s(s(z)))) # label(goal_022) # label(negated_conjecture). [clausify(18)]. % 0.73/1.53 51 -sorted(rev(A)) | -unique(A) | leqNat(lengthNat(A),s(s(s(lengthNat(nil))))). [copy(50),rewrite([24(5)])]. % 0.73/1.53 52 sorted(cons(A,cons(B,C))) | -leqNat(A,B) | -sorted(cons(B,C)) # label(axiom_011) # label(axiom). [clausify(10)]. % 0.73/1.53 53 leqNat(lengthNat(nil),A). [back_rewrite(21),rewrite([24(1)])]. % 0.73/1.53 54 rev(cons(A,nil)) = cons(A,nil). [para(25(a,1),33(a,1,1)),rewrite([27(4)]),flip(a)]. % 0.73/1.53 55 -leqNat(s(s(A)),s(lengthNat(nil))). [ur(42,b,38,a)]. % 0.73/1.53 61 unique(cons(A,nil)). [resolve(47,c,20,a),unit_del(b,34)]. % 0.73/1.53 66 sorted(cons(lengthNat(nil),cons(A,B))) | -sorted(cons(A,B)). [resolve(53,a,52,b)]. % 0.73/1.53 67 leqNat(s(lengthNat(nil)),s(A)). [resolve(53,a,43,b)]. % 0.73/1.53 68 rev(cons(A,cons(B,nil))) = cons(B,cons(A,nil)). [para(54(a,1),33(a,1,1)),rewrite([31(5),27(4)]),flip(a)]. % 0.73/1.53 70 -leqNat(s(s(s(A))),s(s(lengthNat(nil)))). [ur(42,b,55,a)]. % 0.73/1.53 74 unique(cons(A,cons(B,nil))) | elemNat(A,cons(B,nil)). [resolve(61,a,47,c)]. % 0.73/1.53 77 sorted(cons(s(lengthNat(nil)),cons(s(A),B))) | -sorted(cons(s(A),B)). [resolve(67,a,52,b)]. % 0.73/1.53 78 leqNat(s(s(lengthNat(nil))),s(s(A))). [resolve(67,a,43,b)]. % 0.73/1.53 86 sorted(cons(s(s(lengthNat(nil))),cons(s(s(A)),B))) | -sorted(cons(s(s(A)),B)). [resolve(78,a,52,b)]. % 0.73/1.53 87 leqNat(s(s(s(lengthNat(nil)))),s(s(s(A)))). [resolve(78,a,43,b)]. % 0.73/1.53 91 leqNat(s(s(s(s(lengthNat(nil))))),s(s(s(s(A))))). [resolve(87,a,43,b)]. % 0.73/1.53 93 rev(cons(A,cons(B,cons(C,nil)))) = cons(C,cons(B,cons(A,nil))). [para(68(a,1),33(a,1,1)),rewrite([31(6),31(5),27(4)]),flip(a)]. % 0.73/1.53 95 -leqNat(s(s(s(s(A)))),s(s(s(lengthNat(nil))))). [ur(42,b,70,a)]. % 0.73/1.53 105 unique(cons(A,cons(B,nil))) | B = A. [resolve(74,b,49,a),unit_del(c,34)]. % 0.73/1.53 116 A = B | unique(cons(C,cons(B,cons(A,nil)))) | elemNat(C,cons(B,cons(A,nil))). [resolve(105,a,47,c)]. % 0.73/1.53 120 -leqNat(s(s(s(s(s(A))))),s(s(s(s(lengthNat(nil)))))). [ur(42,b,95,a)]. % 0.73/1.53 128 leqNat(s(s(s(s(s(lengthNat(nil)))))),s(s(s(s(s(A)))))). [resolve(91,a,43,b)]. % 0.73/1.53 130 sorted(cons(s(s(lengthNat(nil))),cons(s(s(A)),nil))). [resolve(86,b,22,a)]. % 0.73/1.53 136 sorted(cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(A)),nil)))). [resolve(130,a,77,b)]. % 0.73/1.53 154 sorted(cons(s(s(s(s(s(lengthNat(nil)))))),cons(s(s(s(s(s(A))))),B))) | -sorted(cons(s(s(s(s(s(A))))),B)). [resolve(128,a,52,b)]. % 0.73/1.53 157 rev(cons(A,cons(B,cons(C,cons(D,nil))))) = cons(D,cons(C,cons(B,cons(A,nil)))). [para(93(a,1),33(a,1,1)),rewrite([31(7),31(6),31(5),27(4)]),flip(a)]. % 0.73/1.53 159 -leqNat(s(s(s(s(s(s(A)))))),s(s(s(s(s(lengthNat(nil))))))). [ur(42,b,120,a)]. % 0.73/1.53 165 sorted(cons(lengthNat(nil),cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(A)),nil))))). [resolve(136,a,66,b)]. % 0.73/1.53 186 -leqNat(s(s(s(s(s(s(s(A))))))),s(s(s(s(s(s(lengthNat(nil)))))))). [ur(42,b,159,a)]. % 0.73/1.53 213 A = B | unique(cons(C,cons(B,cons(A,nil)))) | B = C | elemNat(C,cons(A,nil)). [resolve(116,c,49,a)]. % 0.73/1.53 237 -leqNat(s(s(s(s(s(s(s(s(A)))))))),s(s(s(s(s(s(s(lengthNat(nil))))))))). [ur(42,b,186,a)]. % 0.73/1.53 248 sorted(cons(s(s(s(s(s(lengthNat(nil)))))),cons(s(s(s(s(s(A))))),nil))). [resolve(154,b,22,a)]. % 0.73/1.53 256 sorted(cons(s(s(lengthNat(nil))),cons(s(s(s(s(s(lengthNat(nil)))))),cons(s(s(s(s(s(A))))),nil)))). [resolve(248,a,86,b)]. % 0.73/1.53 276 A = B | unique(cons(C,cons(B,cons(A,nil)))) | B = C | A = C. [resolve(213,d,49,a),unit_del(e,34)]. % 0.73/1.53 286 A = B | B = C | A = C | unique(cons(D,cons(C,cons(B,cons(A,nil))))) | elemNat(D,cons(C,cons(B,cons(A,nil)))). [resolve(276,b,47,c)]. % 0.73/1.53 306 -leqNat(s(s(s(s(s(s(s(s(s(A))))))))),s(s(s(s(s(s(s(s(lengthNat(nil)))))))))). [ur(42,b,237,a)]. % 0.73/1.53 365 -leqNat(s(s(s(s(s(s(s(s(s(s(A)))))))))),s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))). [ur(42,b,306,a)]. % 0.73/1.53 429 -leqNat(s(s(s(s(s(s(s(s(s(s(s(A))))))))))),s(s(s(s(s(s(s(s(s(s(lengthNat(nil)))))))))))). [ur(42,b,365,a)]. % 0.73/1.53 438 sorted(cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(s(s(s(lengthNat(nil)))))),cons(s(s(s(s(s(A))))),nil))))). [resolve(256,a,77,b)]. % 0.73/1.53 506 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))),s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))))). [ur(42,b,429,a)]. % 0.73/1.53 527 A = B | B = C | A = C | unique(cons(D,cons(C,cons(B,cons(A,nil))))) | C = D | elemNat(D,cons(B,cons(A,nil))). [resolve(286,e,49,a)]. % 0.73/1.53 575 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil)))))))))))))). [ur(42,b,506,a)]. % 0.73/1.53 651 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))))))). [ur(42,b,575,a)]. % 0.73/1.53 751 sorted(cons(s(lengthNat(nil)),cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(s(s(s(lengthNat(nil)))))),cons(s(s(s(s(s(A))))),nil)))))). [resolve(438,a,77,b)]. % 0.73/1.53 756 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil)))))))))))))))). [ur(42,b,651,a)]. % 0.73/1.53 837 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))))))))). [ur(42,b,756,a)]. % 0.73/1.53 952 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil)))))))))))))))))). [ur(42,b,837,a)]. % 0.73/1.53 1055 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))))))))))). [ur(42,b,952,a)]. % 0.73/1.53 1095 A = B | B = C | A = C | unique(cons(D,cons(C,cons(B,cons(A,nil))))) | C = D | B = D | elemNat(D,cons(A,nil)). [resolve(527,f,49,a)]. % 0.73/1.53 1159 -leqNat(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil)))))))))))))))))))). [ur(42,b,1055,a)]. % 0.73/1.53 1273 sorted(cons(lengthNat(nil),cons(s(lengthNat(nil)),cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(s(s(s(lengthNat(nil)))))),cons(s(s(s(s(s(A))))),nil))))))). [resolve(751,a,66,b)]. % 0.73/1.53 1281 -sorted(cons(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))),cons(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))))))))))),B))). [ur(46,b,1159,a)]. % 0.73/1.53 1400 A = B | B = C | A = C | unique(cons(D,cons(C,cons(B,cons(A,nil))))) | C = D | B = D | A = D. [resolve(1095,g,49,a),unit_del(h,34)]. % 0.73/1.53 1403 A = B | B = C | A = C | C = D | B = D | A = D | -sorted(cons(A,cons(B,cons(C,cons(D,nil))))). [resolve(1400,d,51,b),rewrite([157(12),30(18),30(17),30(16),30(15)]),unit_del(h,95)]. % 0.73/1.53 1423 s(s(lengthNat(nil))) = s(lengthNat(nil)) | s(s(lengthNat(nil))) = s(s(A)) | s(lengthNat(nil)) = s(s(A)). [resolve(1403,g,165,a),flip(a),flip(b),flip(c),flip(f),unit_del(a(flip),36),unit_del(c(flip),36),unit_del(f(flip),36)]. % 0.73/1.53 1428 s(s(lengthNat(nil))) = s(s(A)) | s(lengthNat(nil)) = s(s(A)). [para(1423(a,1),26(a,1,1)),rewrite([26(17)]),flip(c),unit_del(c(flip),36)]. % 0.73/1.53 2283 -sorted(cons(A,cons(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(B))))))))))))))))))),cons(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(lengthNat(nil))))))))))))))))))),C)))). [ur(48,b,1281,a)]. % 0.73/1.53 2296 s(s(s(A))) = s(lengthNat(nil)). [para(1428(a,2),87(a,2)),flip(a),unit_del(b,70)]. % 0.73/1.53 2297 s(lengthNat(nil)) = s(s(A)). [para(1428(a,1),70(a,1,1,1)),rewrite([2296(9)]),unit_del(b,78)]. % 0.73/1.53 2298 -sorted(cons(A,cons(s(lengthNat(nil)),cons(s(lengthNat(nil)),B)))). [back_rewrite(2283),rewrite([2297(3,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(4,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R),2297(7,R)])]. % 0.73/1.53 2299 $F. [resolve(2298,a,1273,a)]. % 0.73/1.53 % 0.73/1.53 % SZS output end Refutation % 0.73/1.53 ============================== end of proof ========================== % 0.73/1.53 % 0.73/1.53 ============================== STATISTICS ============================ % 0.73/1.53 % 0.73/1.53 Given=953. Generated=24594. Kept=2275. proofs=1. % 0.73/1.53 Usable=953. Sos=1312. Demods=18. Limbo=2, Disabled=36. Hints=0. % 0.73/1.53 Megabytes=3.41. % 0.73/1.53 User_CPU=0.52, System_CPU=0.02, Wall_clock=1. % 0.73/1.53 % 0.73/1.53 ============================== end of statistics ===================== % 0.73/1.53 % 0.73/1.53 ============================== end of search ========================= % 0.73/1.53 % 0.73/1.53 THEOREM PROVED % 0.73/1.53 % SZS status Theorem % 0.73/1.53 % 0.73/1.53 Exiting with 1 proof. % 0.73/1.53 % 0.73/1.53 Process 17442 exit (max_proofs) Wed Apr 29 00:47:22 2026 % 0.73/1.53 Prover9 interrupted %------------------------------------------------------------------------------