%------------------------------------------------------------------------------ % 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 : n020.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 : Unsatisfiable 7.66s 7.90s % Output : Refutation 7.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.33 % Computer : n020.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 : Wed Apr 29 00:49:19 EDT 2026 % 0.15/0.34 % CPUTime : % 7.66/7.90 ============================== Prover9 =============================== % 7.66/7.90 Prover9 (32) version 2009-11A, November 2009. % 7.66/7.90 Process 4458 was started by sandbox on n020.cluster.edu, % 7.66/7.90 Wed Apr 29 00:49:19 2026 % 7.66/7.90 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_4305_n020.cluster.edu". % 7.66/7.90 ============================== end of head =========================== % 7.66/7.90 % 7.66/7.90 ============================== INPUT ================================= % 7.66/7.90 % 7.66/7.90 % Reading from file /tmp/Prover9_4305_n020.cluster.edu % 7.66/7.90 % 7.66/7.90 set(prolog_style_variables). % 7.66/7.90 set(auto2). % 7.66/7.90 % set(auto2) -> set(auto). % 7.66/7.90 % set(auto) -> set(auto_inference). % 7.66/7.90 % set(auto) -> set(auto_setup). % 7.66/7.90 % set(auto_setup) -> set(predicate_elim). % 7.66/7.90 % set(auto_setup) -> assign(eq_defs, unfold). % 7.66/7.90 % set(auto) -> set(auto_limits). % 7.66/7.90 % set(auto_limits) -> assign(max_weight, "100.000"). % 7.66/7.90 % set(auto_limits) -> assign(sos_limit, 20000). % 7.66/7.90 % set(auto) -> set(auto_denials). % 7.66/7.90 % set(auto) -> set(auto_process). % 7.66/7.90 % set(auto2) -> assign(new_constants, 1). % 7.66/7.90 % set(auto2) -> assign(fold_denial_max, 3). % 7.66/7.90 % set(auto2) -> assign(max_weight, "200.000"). % 7.66/7.90 % set(auto2) -> assign(max_hours, 1). % 7.66/7.90 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 7.66/7.90 % set(auto2) -> assign(max_seconds, 0). % 7.66/7.90 % set(auto2) -> assign(max_minutes, 5). % 7.66/7.90 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 7.66/7.90 % set(auto2) -> set(sort_initial_sos). % 7.66/7.90 % set(auto2) -> assign(sos_limit, -1). % 7.66/7.90 % set(auto2) -> assign(lrs_ticks, 3000). % 7.66/7.90 % set(auto2) -> assign(max_megs, 400). % 7.66/7.90 % set(auto2) -> assign(stats, some). % 7.66/7.90 % set(auto2) -> clear(echo_input). % 7.66/7.90 % set(auto2) -> set(quiet). % 7.66/7.90 % set(auto2) -> clear(print_initial_clauses). % 7.66/7.90 % set(auto2) -> clear(print_given). % 7.66/7.90 assign(lrs_ticks,-1). % 7.66/7.90 assign(sos_limit,10000). % 7.66/7.90 assign(order,kbo). % 7.66/7.90 set(lex_order_vars). % 7.66/7.90 clear(print_given). % 7.66/7.90 % 7.66/7.90 % formulas(sos). % not echoed (33 formulas) % 7.66/7.90 % 7.66/7.90 ============================== end of input ========================== % 7.66/7.90 % 7.66/7.90 % From the command line: assign(max_seconds, 300). % 7.66/7.90 % 7.66/7.90 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 7.66/7.90 % 7.66/7.90 % Formulas that are not ordinary clauses: % 7.66/7.90 % 7.66/7.90 ============================== end of process non-clausal formulas === % 7.66/7.90 % 7.66/7.90 ============================== PROCESS INITIAL CLAUSES =============== % 7.66/7.90 % 7.66/7.90 ============================== PREDICATE ELIMINATION ================= % 7.66/7.90 % 7.66/7.90 ============================== end predicate elimination ============= % 7.66/7.90 % 7.66/7.90 Auto_denials: % 7.66/7.90 % copying label goal to answer in negative clause % 7.66/7.90 % 7.66/7.90 Term ordering decisions: % 7.66/7.90 Function symbol KB weights: btrue=1. bfalse=1. nil=1. z=1. cons=1. eq=1. eq2=1. leqNat=1. append=1. elemNat=1. impl=1. andb=1. orb=1. s=1. sorted=1. lengthNat=1. rev=1. unique=1. psorted_rev=1. aux=1. % 7.66/7.90 % 7.66/7.90 ============================== end of process initial clauses ======== % 7.66/7.90 % 7.66/7.90 ============================== CLAUSES FOR SEARCH ==================== % 7.66/7.90 % 7.66/7.90 ============================== end of clauses for search ============= % 7.66/7.90 % 7.66/7.90 ============================== SEARCH ================================ % 7.66/7.90 % 7.66/7.90 % Starting search at 0.01 seconds. % 7.66/7.90 % 7.66/7.90 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 39 (0.00 of 0.55 sec). % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=64.000, iters=3400 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=62.000, iters=3355 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=61.000, iters=3359 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=60.000, iters=3344 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=59.000, iters=3379 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=58.000, iters=3364 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=57.000, iters=3348 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=56.000, iters=3407 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=54.000, iters=3357 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=53.000, iters=3336 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=52.000, iters=3363 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=51.000, iters=3418 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=50.000, iters=3408 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=49.000, iters=3350 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=48.000, iters=3341 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=47.000, iters=3342 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=46.000, iters=3341 % 7.66/7.90 % 7.66/7.90 Low Water (keep): wt=45.000, iters=3333 % 7.66/7.90 % 7.66/7.90 ============================== PROOF ================================= % 7.66/7.90 % SZS status Unsatisfiable % 7.66/7.90 % SZS output start Refutation % 7.66/7.90 % 7.66/7.90 % Proof 1 at 6.74 (+ 0.09) seconds: goal. % 7.66/7.90 % Length of proof is 77. % 7.66/7.90 % Level of proof is 10. % 7.66/7.90 % Maximum clause weight is 34.000. % 7.66/7.90 % Given clauses 2200. % 7.66/7.90 % 7.66/7.90 1 lengthNat(nil) = z # label(axiom_007) # label(axiom). [assumption]. % 7.66/7.90 2 unique(nil) = btrue # label(axiom_013) # label(axiom). [assumption]. % 7.66/7.90 3 btrue = unique(nil). [copy(2),flip(a)]. % 7.66/7.90 4 rev(nil) = nil # label(axiom_017) # label(axiom). [assumption]. % 7.66/7.90 5 sorted(nil) = btrue # label(axiom_021) # label(axiom). [assumption]. % 7.66/7.90 6 unique(nil) = sorted(nil). [copy(5),rewrite([3(3)]),flip(a)]. % 7.66/7.90 9 orb(bfalse,A) = A # label(axiom_003) # label(axiom). [assumption]. % 7.66/7.90 10 leqNat(z,A) = btrue # label(axiom_004) # label(axiom). [assumption]. % 7.66/7.90 11 leqNat(z,A) = sorted(nil). [copy(10),rewrite([3(3),6(4)])]. % 7.66/7.90 12 impl(btrue,A) = A # label(axiom_009) # label(axiom). [assumption]. % 7.66/7.90 13 impl(sorted(nil),A) = A. [copy(12),rewrite([3(1),6(2)])]. % 7.66/7.90 16 elemNat(A,nil) = bfalse # label(axiom_011) # label(axiom). [assumption]. % 7.66/7.90 17 append(nil,A) = A # label(axiom_015) # label(axiom). [assumption]. % 7.66/7.90 18 andb(btrue,A) = A # label(axiom_019) # label(axiom). [assumption]. % 7.66/7.90 19 andb(sorted(nil),A) = A. [copy(18),rewrite([3(1),6(2)])]. % 7.66/7.90 21 eq2(bfalse,btrue) = bfalse # label(axiom_025) # label(axiom). [assumption]. % 7.66/7.90 22 eq2(bfalse,sorted(nil)) = bfalse. [copy(21),rewrite([3(2),6(3)])]. % 7.66/7.90 27 eq2(A,A) = btrue # label(axiom_031) # label(axiom). [assumption]. % 7.66/7.90 28 eq2(A,A) = sorted(nil). [copy(27),rewrite([3(2),6(3)])]. % 7.66/7.90 31 leqNat(s(A),z) = bfalse # label(axiom_005) # label(axiom). [assumption]. % 7.66/7.90 32 sorted(cons(A,nil)) = btrue # label(axiom_022) # label(axiom). [assumption]. % 7.66/7.90 33 sorted(cons(A,nil)) = sorted(nil). [copy(32),rewrite([3(4),6(5)])]. % 7.66/7.90 35 eq(s(A),z) = bfalse # label(axiom_029) # label(axiom). [assumption]. % 7.66/7.90 36 aux(A,B,bfalse) = unique(B) # label(axiom_001) # label(axiom). [assumption]. % 7.66/7.90 37 lengthNat(cons(A,B)) = s(lengthNat(B)) # label(axiom_008) # label(axiom). [assumption]. % 7.66/7.90 38 leqNat(s(A),s(B)) = leqNat(A,B) # label(axiom_006) # label(axiom). [assumption]. % 7.66/7.90 39 eq(s(A),s(B)) = eq(A,B) # label(axiom_027) # label(axiom). [assumption]. % 7.66/7.90 40 unique(cons(A,B)) = aux(A,B,elemNat(A,B)) # label(axiom_014) # label(axiom). [assumption]. % 7.66/7.90 41 aux(A,B,elemNat(A,B)) = unique(cons(A,B)). [copy(40),flip(a)]. % 7.66/7.90 42 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_016) # label(axiom). [assumption]. % 7.66/7.90 43 rev(cons(A,B)) = append(rev(B),cons(A,nil)) # label(axiom_018) # label(axiom). [assumption]. % 7.66/7.90 44 append(rev(A),cons(B,nil)) = rev(cons(B,A)). [copy(43),flip(a)]. % 7.66/7.90 45 elemNat(A,cons(B,C)) = orb(eq(A,B),elemNat(A,C)) # label(axiom_012) # label(axiom). [assumption]. % 7.66/7.90 46 orb(eq(A,B),elemNat(A,C)) = elemNat(A,cons(B,C)). [copy(45),flip(a)]. % 7.66/7.90 47 sorted(cons(A,cons(B,C))) = andb(leqNat(A,B),sorted(cons(B,C))) # label(axiom_023) # label(axiom). [assumption]. % 7.66/7.90 48 andb(leqNat(A,B),sorted(cons(B,C))) = sorted(cons(A,cons(B,C))). [copy(47),flip(a)]. % 7.66/7.90 49 psorted_rev(A) = impl(eq2(sorted(rev(A)),btrue),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))) # label(axiom_024) # label(axiom). [assumption]. % 7.66/7.90 50 psorted_rev(A) = impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),sorted(nil)))). [copy(49),rewrite([3(4),6(5),3(8),6(9),3(17),6(18)])]. % 7.66/7.90 51 eq2(psorted_rev(A),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 7.66/7.90 52 eq2(impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil) # answer(goal). [copy(51),rewrite([50(1),3(23),6(24)])]. % 7.66/7.90 54 unique(cons(A,nil)) = sorted(nil). [para(16(a,1),41(a,1,3)),rewrite([36(3),6(2)]),flip(a)]. % 7.66/7.90 55 rev(cons(A,nil)) = cons(A,nil). [para(4(a,1),44(a,1,1)),rewrite([17(4)]),flip(a)]. % 7.66/7.90 56 orb(eq(A,B),bfalse) = elemNat(A,cons(B,nil)). [para(16(a,1),46(a,1,2))]. % 7.66/7.90 59 elemNat(s(A),cons(z,B)) = elemNat(s(A),B). [para(35(a,1),46(a,1,1)),rewrite([9(4)]),flip(a)]. % 7.66/7.90 60 orb(eq(A,B),elemNat(s(A),C)) = elemNat(s(A),cons(s(B),C)). [para(39(a,1),46(a,1,1))]. % 7.66/7.90 63 sorted(cons(A,cons(B,nil))) = andb(leqNat(A,B),sorted(nil)). [para(33(a,1),48(a,1,2)),flip(a)]. % 7.66/7.90 64 andb(leqNat(A,B),sorted(cons(s(B),C))) = sorted(cons(s(A),cons(s(B),C))). [para(38(a,1),48(a,1,1))]. % 7.66/7.90 70 rev(cons(A,cons(B,nil))) = cons(B,cons(A,nil)). [para(55(a,1),44(a,1,1)),rewrite([42(5),17(4)]),flip(a)]. % 7.66/7.90 76 elemNat(s(A),cons(s(B),nil)) = elemNat(A,cons(B,nil)). [para(39(a,1),56(a,1,1)),rewrite([56(3)]),flip(a)]. % 7.66/7.90 82 aux(s(A),cons(z,B),elemNat(s(A),B)) = unique(cons(s(A),cons(z,B))). [para(59(a,1),41(a,1,3))]. % 7.66/7.90 83 elemNat(s(A),cons(B,cons(z,C))) = elemNat(s(A),cons(B,C)). [para(59(a,1),46(a,1,2)),rewrite([46(5)]),flip(a)]. % 7.66/7.90 85 rev(cons(A,cons(B,cons(C,nil)))) = cons(C,cons(B,cons(A,nil))). [para(70(a,1),44(a,1,1)),rewrite([42(6),42(5),17(4)]),flip(a)]. % 7.66/7.90 87 elemNat(s(s(A)),cons(s(z),B)) = elemNat(s(s(A)),B). [para(35(a,1),60(a,1,1)),rewrite([9(5)]),flip(a)]. % 7.66/7.90 93 andb(leqNat(A,B),andb(leqNat(B,C),sorted(nil))) = sorted(cons(A,cons(B,cons(C,nil)))). [para(63(a,1),48(a,1,2))]. % 7.66/7.90 102 sorted(cons(s(z),cons(s(A),B))) = sorted(cons(s(A),B)). [para(11(a,1),64(a,1,1)),rewrite([19(6)]),flip(a)]. % 7.66/7.90 104 sorted(cons(s(s(A)),cons(s(s(B)),C))) = andb(leqNat(A,B),sorted(cons(s(s(B)),C))). [para(38(a,1),64(a,1,1)),flip(a)]. % 7.66/7.90 105 andb(leqNat(A,B),andb(leqNat(s(B),C),sorted(nil))) = sorted(cons(s(A),cons(s(B),cons(C,nil)))). [para(63(a,1),64(a,1,2))]. % 7.66/7.90 114 elemNat(s(s(A)),cons(B,cons(s(z),C))) = elemNat(s(s(A)),cons(B,C)). [para(87(a,1),46(a,1,2)),rewrite([46(7)]),flip(a)]. % 7.66/7.90 115 sorted(cons(A,cons(s(z),cons(s(B),C)))) = andb(leqNat(A,s(z)),sorted(cons(s(B),C))). [para(102(a,1),48(a,1,2)),flip(a)]. % 7.66/7.90 123 aux(s(A),cons(B,cons(z,C)),elemNat(s(A),cons(B,C))) = unique(cons(s(A),cons(B,cons(z,C)))). [para(83(a,1),41(a,1,3))]. % 7.66/7.90 128 rev(cons(A,cons(B,cons(C,cons(D,nil))))) = cons(D,cons(C,cons(B,cons(A,nil)))). [para(85(a,1),44(a,1,1)),rewrite([42(7),42(6),42(5),17(4)]),flip(a)]. % 7.66/7.90 134 unique(cons(s(A),cons(z,nil))) = sorted(nil). [para(16(a,1),82(a,1,3)),rewrite([36(6),54(4)]),flip(a)]. % 7.66/7.90 161 aux(s(s(A)),cons(B,cons(s(z),C)),elemNat(s(s(A)),cons(B,C))) = unique(cons(s(s(A)),cons(B,cons(s(z),C)))). [para(114(a,1),41(a,1,3))]. % 7.66/7.90 184 andb(leqNat(A,s(B)),andb(leqNat(B,C),sorted(nil))) = sorted(cons(A,cons(s(B),cons(s(C),nil)))). [para(38(a,1),93(a,1,2,1))]. % 7.66/7.90 250 sorted(cons(s(s(z)),cons(s(s(A)),B))) = sorted(cons(s(s(A)),B)). [para(11(a,1),104(a,2,1)),rewrite([19(15)])]. % 7.66/7.90 263 sorted(cons(A,cons(s(s(z)),cons(s(s(B)),C)))) = andb(leqNat(A,s(s(z))),sorted(cons(s(s(B)),C))). [para(250(a,1),48(a,1,2)),flip(a)]. % 7.66/7.90 287 sorted(cons(s(A),cons(s(B),cons(s(C),nil)))) = sorted(cons(A,cons(B,cons(C,nil)))). [para(38(a,1),105(a,1,2,1)),rewrite([93(6)]),flip(a)]. % 7.66/7.90 291 sorted(cons(A,cons(s(B),cons(s(C),cons(s(D),nil))))) = andb(leqNat(A,s(B)),sorted(cons(B,cons(C,cons(D,nil))))). [para(287(a,1),48(a,1,2)),flip(a)]. % 7.66/7.90 292 sorted(cons(s(A),cons(s(B),cons(s(C),cons(s(D),nil))))) = sorted(cons(A,cons(B,cons(C,cons(D,nil))))). [para(287(a,1),64(a,1,2)),rewrite([48(7)]),flip(a)]. % 7.66/7.90 391 aux(s(A),cons(s(B),cons(z,nil)),elemNat(A,cons(B,nil))) = unique(cons(s(A),cons(s(B),cons(z,nil)))). [para(76(a,1),123(a,1,3))]. % 7.66/7.90 983 unique(cons(s(s(A)),cons(s(z),cons(z,nil)))) = sorted(nil). [para(59(a,1),391(a,1,3)),rewrite([16(11),36(10),134(7)]),flip(a)]. % 7.66/7.90 997 aux(s(s(A)),cons(B,cons(s(z),cons(z,C))),elemNat(s(s(A)),cons(B,C))) = unique(cons(s(s(A)),cons(B,cons(s(z),cons(z,C))))). [para(83(a,1),161(a,1,3))]. % 7.66/7.90 1638 sorted(cons(A,cons(s(B),cons(s(s(s(z))),cons(s(s(s(C))),nil))))) = sorted(cons(A,cons(s(B),cons(s(s(s(z))),nil)))). [para(263(a,1),291(a,2,2)),rewrite([33(25),184(24)])]. % 7.66/7.90 4763 sorted(cons(A,cons(B,cons(s(s(z)),cons(s(s(C)),nil))))) = sorted(cons(A,cons(B,cons(s(s(z)),nil)))). [para(1638(a,1),292(a,1)),rewrite([287(11)]),flip(a)]. % 7.66/7.90 7675 aux(s(s(A)),cons(s(B),cons(s(z),cons(z,nil))),elemNat(s(A),cons(B,nil))) = unique(cons(s(s(A)),cons(s(B),cons(s(z),cons(z,nil))))). [para(76(a,1),997(a,1,3))]. % 7.66/7.90 9999 unique(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = sorted(nil). [para(87(a,1),7675(a,1,3)),rewrite([16(17),36(15),983(11)]),flip(a)]. % 7.66/7.90 10025 $F # answer(goal). [para(9999(a,1),52(a,1,1,2,1,1)),rewrite([128(15),4763(15),115(11),11(4),33(8),19(5),28(5),28(7),37(19),37(15),37(11),37(8),1(6),38(14),38(12),38(10),31(8),22(8),13(6),13(4),28(3)]),xx(a)]. % 7.66/7.90 % 7.66/7.90 % SZS output end Refutation % 7.66/7.90 ============================== end of proof ========================== % 7.66/7.90 % 7.66/7.90 ============================== STATISTICS ============================ % 7.66/7.90 % 7.66/7.90 Given=2200. Generated=145669. Kept=10005. proofs=1. % 7.66/7.90 Usable=2140. Sos=7031. Demods=3842. Limbo=0, Disabled=867. Hints=0. % 7.66/7.90 Megabytes=17.96. % 7.66/7.90 User_CPU=6.75, System_CPU=0.09, Wall_clock=7. % 7.66/7.90 % 7.66/7.90 ============================== end of statistics ===================== % 7.66/7.90 % 7.66/7.90 ============================== end of search ========================= % 7.66/7.90 % 7.66/7.90 THEOREM PROVED % 7.66/7.90 % SZS status Unsatisfiable % 7.66/7.90 % 7.66/7.90 Exiting with 1 proof. % 7.66/7.90 % 7.66/7.90 Process 4458 exit (max_proofs) Wed Apr 29 00:49:26 2026 % 7.66/7.91 Prover9 interrupted %------------------------------------------------------------------------------