%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n004.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:10 PM UTC 2026 % Result : Unsatisfiable 1.75s 2.11s % Output : Refutation 1.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.14/0.34 % Computer : n004.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 29 03:03:31 EDT 2026 % 0.14/0.34 % CPUTime : % 1.75/2.11 ============================== Prover9 =============================== % 1.75/2.11 Prover9 (32) version 2009-11A, November 2009. % 1.75/2.11 Process 14763 was started by sandbox on n004.cluster.edu, % 1.75/2.11 Wed Apr 29 03:03:32 2026 % 1.75/2.11 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_14609_n004.cluster.edu". % 1.75/2.11 ============================== end of head =========================== % 1.75/2.11 % 1.75/2.11 ============================== INPUT ================================= % 1.75/2.11 % 1.75/2.11 % Reading from file /tmp/Prover9_14609_n004.cluster.edu % 1.75/2.11 % 1.75/2.11 set(prolog_style_variables). % 1.75/2.11 set(auto2). % 1.75/2.11 % set(auto2) -> set(auto). % 1.75/2.11 % set(auto) -> set(auto_inference). % 1.75/2.11 % set(auto) -> set(auto_setup). % 1.75/2.11 % set(auto_setup) -> set(predicate_elim). % 1.75/2.11 % set(auto_setup) -> assign(eq_defs, unfold). % 1.75/2.11 % set(auto) -> set(auto_limits). % 1.75/2.11 % set(auto_limits) -> assign(max_weight, "100.000"). % 1.75/2.11 % set(auto_limits) -> assign(sos_limit, 20000). % 1.75/2.11 % set(auto) -> set(auto_denials). % 1.75/2.11 % set(auto) -> set(auto_process). % 1.75/2.11 % set(auto2) -> assign(new_constants, 1). % 1.75/2.11 % set(auto2) -> assign(fold_denial_max, 3). % 1.75/2.11 % set(auto2) -> assign(max_weight, "200.000"). % 1.75/2.11 % set(auto2) -> assign(max_hours, 1). % 1.75/2.11 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 1.75/2.11 % set(auto2) -> assign(max_seconds, 0). % 1.75/2.11 % set(auto2) -> assign(max_minutes, 5). % 1.75/2.11 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 1.75/2.11 % set(auto2) -> set(sort_initial_sos). % 1.75/2.11 % set(auto2) -> assign(sos_limit, -1). % 1.75/2.11 % set(auto2) -> assign(lrs_ticks, 3000). % 1.75/2.11 % set(auto2) -> assign(max_megs, 400). % 1.75/2.11 % set(auto2) -> assign(stats, some). % 1.75/2.11 % set(auto2) -> clear(echo_input). % 1.75/2.11 % set(auto2) -> set(quiet). % 1.75/2.11 % set(auto2) -> clear(print_initial_clauses). % 1.75/2.11 % set(auto2) -> clear(print_given). % 1.75/2.11 assign(lrs_ticks,-1). % 1.75/2.11 assign(sos_limit,10000). % 1.75/2.11 assign(order,kbo). % 1.75/2.11 set(lex_order_vars). % 1.75/2.11 clear(print_given). % 1.75/2.11 % 1.75/2.11 % formulas(sos). % not echoed (113 formulas) % 1.75/2.11 % 1.75/2.11 ============================== end of input ========================== % 1.75/2.11 % 1.75/2.11 % From the command line: assign(max_seconds, 300). % 1.75/2.11 % 1.75/2.11 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 1.75/2.11 % 1.75/2.11 % Formulas that are not ordinary clauses: % 1.75/2.11 % 1.75/2.11 ============================== end of process non-clausal formulas === % 1.75/2.11 % 1.75/2.11 ============================== PROCESS INITIAL CLAUSES =============== % 1.75/2.11 % 1.75/2.11 ============================== PREDICATE ELIMINATION ================= % 1.75/2.11 % 1.75/2.11 ============================== end predicate elimination ============= % 1.75/2.11 % 1.75/2.11 Auto_denials: % 1.75/2.11 % copying label goal to answer in negative clause % 1.75/2.11 % 1.75/2.11 Term ordering decisions: % 1.75/2.11 Function symbol KB weights: eps=1. bfalse=1. nil4=1. btrue=1. nil2=1. a=1. b=1. c=1. nil=1. nil3=1. x=1. y=1. x2=1. z=1. reck2=1. step=1. cons2=1. eq=1. rec=1. cons=1. orb=1. pair2=1. andb=1. eq2=1. splits=1. cons3=1. prop_same=1. star=1. atom=1. eps2=1. or2=1. splits2=1. notb=1. reck=1. aux=1. aux2=1. aux3=1. % 1.75/2.11 % 1.75/2.11 ============================== end of process initial clauses ======== % 1.75/2.11 % 1.75/2.11 ============================== CLAUSES FOR SEARCH ==================== % 1.75/2.11 % 1.75/2.11 ============================== end of clauses for search ============= % 1.75/2.11 % 1.75/2.11 ============================== SEARCH ================================ % 1.75/2.11 % 1.75/2.11 % Starting search at 0.02 seconds. % 1.75/2.11 % 1.75/2.11 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 414 (0.00 of 0.32 sec). % 1.75/2.11 % 1.75/2.11 Low Water (keep): wt=31.000, iters=3396 % 1.75/2.11 % 1.75/2.11 Low Water (keep): wt=23.000, iters=3358 % 1.75/2.11 % 1.75/2.11 Low Water (keep): wt=22.000, iters=3369 % 1.75/2.11 % 1.75/2.11 Low Water (keep): wt=21.000, iters=3454 % 1.75/2.11 % 1.75/2.11 Low Water (keep): wt=20.000, iters=3333 % 1.75/2.11 % 1.75/2.11 Low Water (keep): wt=19.000, iters=3334 % 1.75/2.11 % 1.75/2.11 ============================== PROOF ================================= % 1.75/2.11 % SZS status Unsatisfiable % 1.75/2.11 % SZS output start Refutation % 1.75/2.11 % 1.75/2.11 % Proof 1 at 1.09 (+ 0.02) seconds: goal. % 1.75/2.11 % Length of proof is 38. % 1.75/2.11 % Level of proof is 7. % 1.75/2.11 % Maximum clause weight is 15.000. % 1.75/2.11 % Given clauses 1238. % 1.75/2.11 % 1.75/2.11 1 aux(A,B,btrue) = eps # label(axiom) # label(axiom). [assumption]. % 1.75/2.11 9 aux3(A,B,C,bfalse) = bfalse # label(axiom_005) # label(axiom). [assumption]. % 1.75/2.11 78 notb(btrue) = bfalse # label(axiom_071) # label(axiom). [assumption]. % 1.75/2.11 80 andb(btrue,A) = A # label(axiom_073) # label(axiom). [assumption]. % 1.75/2.11 82 eps2(eps) = btrue # label(axiom_075) # label(axiom). [assumption]. % 1.75/2.11 85 eps2(y(A,B)) = andb(eps2(A),eps2(B)) # label(axiom_077) # label(axiom). [assumption]. % 1.75/2.11 86 andb(eps2(A),eps2(B)) = eps2(y(A,B)). [copy(85),flip(a)]. % 1.75/2.11 87 eps2(star(A)) = btrue # label(axiom_078) # label(axiom). [assumption]. % 1.75/2.11 90 step(atom(A),B) = aux(B,A,eq(A,B)) # label(axiom_081) # label(axiom). [assumption]. % 1.75/2.11 91 aux(A,B,eq(B,A)) = step(atom(B),A). [copy(90),flip(a)]. % 1.75/2.11 96 step(star(A),B) = y(step(A,B),star(A)) # label(axiom_084) # label(axiom). [assumption]. % 1.75/2.11 97 y(step(A,B),star(A)) = step(star(A),B). [copy(96),flip(a)]. % 1.75/2.11 100 rec(A,nil2) = eps2(A) # label(axiom_087) # label(axiom). [assumption]. % 1.75/2.11 101 eps2(A) = rec(A,nil2). [copy(100),flip(a)]. % 1.75/2.11 102 rec(A,cons2(B,C)) = rec(step(A,B),C) # label(axiom_088) # label(axiom). [assumption]. % 1.75/2.11 103 rec(step(A,B),C) = rec(A,cons2(B,C)). [copy(102),flip(a)]. % 1.75/2.11 111 reck2(atom(A),cons2(B,nil2)) = eq(A,B) # label(axiom_095) # label(axiom). [assumption]. % 1.75/2.11 112 eq(A,B) = reck2(atom(A),cons2(B,nil2)). [copy(111),flip(a)]. % 1.75/2.11 119 reck2(star(A),cons2(B,C)) = aux3(A,B,C,notb(eps2(A))) # label(axiom_100) # label(axiom). [assumption]. % 1.75/2.11 120 aux3(A,B,C,notb(rec(A,nil2))) = reck2(star(A),cons2(B,C)). [copy(119),rewrite([101(4)]),flip(a)]. % 1.75/2.11 121 prop_same(A,B) = eq2(rec(A,B),reck2(A,B)) # label(axiom_101) # label(axiom). [assumption]. % 1.75/2.11 135 eq2(btrue,bfalse) = bfalse # label(axiom_109) # label(axiom). [assumption]. % 1.75/2.11 136 eq(A,A) = btrue # label(axiom_110) # label(axiom). [assumption]. % 1.75/2.11 137 reck2(atom(A),cons2(A,nil2)) = btrue. [copy(136),rewrite([112(1)])]. % 1.75/2.11 138 eq2(A,A) = btrue # label(axiom_111) # label(axiom). [assumption]. % 1.75/2.11 139 eq2(prop_same(A,B),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 1.75/2.11 140 eq2(eq2(rec(A,B),reck2(A,B)),bfalse) != btrue # answer(goal). [copy(139),rewrite([121(1)])]. % 1.75/2.11 144 rec(star(A),nil2) = btrue. [back_rewrite(87),rewrite([101(2)])]. % 1.75/2.11 145 andb(rec(A,nil2),rec(B,nil2)) = rec(y(A,B),nil2). [back_rewrite(86),rewrite([101(1),101(3),101(7)])]. % 1.75/2.11 147 rec(eps,nil2) = btrue. [back_rewrite(82),rewrite([101(2)])]. % 1.75/2.11 148 aux(A,B,reck2(atom(B),cons2(A,nil2))) = step(atom(B),A). [back_rewrite(91),rewrite([112(1)])]. % 1.75/2.11 321 reck2(star(star(A)),cons2(B,C)) = bfalse. [para(144(a,1),120(a,1,4,1)),rewrite([78(3),9(3)]),flip(a)]. % 1.75/2.11 323 andb(rec(A,cons2(B,nil2)),btrue) = rec(star(A),cons2(B,nil2)). [para(97(a,1),145(a,2,1)),rewrite([103(3),144(6),103(9)])]. % 1.75/2.11 362 step(atom(A),A) = eps. [para(137(a,1),148(a,1,3)),rewrite([1(2)]),flip(a)]. % 1.75/2.11 410 y(eps,star(atom(A))) = step(star(atom(A)),A). [para(362(a,1),97(a,1,1))]. % 1.75/2.11 1296 rec(star(atom(A)),cons2(A,nil2)) = btrue. [para(410(a,1),145(a,2,1)),rewrite([147(3),144(5),80(3),103(6)]),flip(a)]. % 1.75/2.11 7850 rec(star(star(atom(A))),cons2(A,nil2)) = btrue. [para(1296(a,1),323(a,1,1)),rewrite([80(3)]),flip(a)]. % 1.75/2.11 7890 $F # answer(goal). [para(7850(a,1),140(a,1,1,1)),rewrite([321(7),135(3),138(3)]),xx(a)]. % 1.75/2.11 % 1.75/2.11 % SZS output end Refutation % 1.75/2.11 ============================== end of proof ========================== % 1.75/2.11 % 1.75/2.11 ============================== STATISTICS ============================ % 1.75/2.11 % 1.75/2.11 Given=1238. Generated=33716. Kept=7862. proofs=1. % 1.75/2.11 Usable=947. Sos=5234. Demods=2279. Limbo=0, Disabled=1794. Hints=0. % 1.75/2.11 Megabytes=8.17. % 1.75/2.11 User_CPU=1.09, System_CPU=0.02, Wall_clock=1. % 1.75/2.11 % 1.75/2.11 ============================== end of statistics ===================== % 1.75/2.11 % 1.75/2.11 ============================== end of search ========================= % 1.75/2.11 % 1.75/2.11 THEOREM PROVED % 1.75/2.11 % SZS status Unsatisfiable % 1.75/2.11 % 1.75/2.11 Exiting with 1 proof. % 1.75/2.11 % 1.75/2.11 Process 14763 exit (max_proofs) Wed Apr 29 03:03:33 2026 % 1.75/2.11 Prover9 interrupted %------------------------------------------------------------------------------