%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX199-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n029.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 0.74s 1.08s % Output : Refutation 0.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX199-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.14/0.33 % Computer : n029.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Wed Apr 29 00:33:29 EDT 2026 % 0.14/0.33 % CPUTime : % 0.74/1.08 ============================== Prover9 =============================== % 0.74/1.08 Prover9 (32) version 2009-11A, November 2009. % 0.74/1.08 Process 15262 was started by sandbox on n029.cluster.edu, % 0.74/1.08 Wed Apr 29 00:33:29 2026 % 0.74/1.08 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_15109_n029.cluster.edu". % 0.74/1.08 ============================== end of head =========================== % 0.74/1.08 % 0.74/1.08 ============================== INPUT ================================= % 0.74/1.08 % 0.74/1.08 % Reading from file /tmp/Prover9_15109_n029.cluster.edu % 0.74/1.08 % 0.74/1.08 set(prolog_style_variables). % 0.74/1.08 set(auto2). % 0.74/1.08 % set(auto2) -> set(auto). % 0.74/1.08 % set(auto) -> set(auto_inference). % 0.74/1.08 % set(auto) -> set(auto_setup). % 0.74/1.08 % set(auto_setup) -> set(predicate_elim). % 0.74/1.08 % set(auto_setup) -> assign(eq_defs, unfold). % 0.74/1.08 % set(auto) -> set(auto_limits). % 0.74/1.08 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.74/1.08 % set(auto_limits) -> assign(sos_limit, 20000). % 0.74/1.08 % set(auto) -> set(auto_denials). % 0.74/1.08 % set(auto) -> set(auto_process). % 0.74/1.08 % set(auto2) -> assign(new_constants, 1). % 0.74/1.08 % set(auto2) -> assign(fold_denial_max, 3). % 0.74/1.08 % set(auto2) -> assign(max_weight, "200.000"). % 0.74/1.08 % set(auto2) -> assign(max_hours, 1). % 0.74/1.08 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.74/1.08 % set(auto2) -> assign(max_seconds, 0). % 0.74/1.08 % set(auto2) -> assign(max_minutes, 5). % 0.74/1.08 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.74/1.08 % set(auto2) -> set(sort_initial_sos). % 0.74/1.08 % set(auto2) -> assign(sos_limit, -1). % 0.74/1.08 % set(auto2) -> assign(lrs_ticks, 3000). % 0.74/1.08 % set(auto2) -> assign(max_megs, 400). % 0.74/1.08 % set(auto2) -> assign(stats, some). % 0.74/1.08 % set(auto2) -> clear(echo_input). % 0.74/1.08 % set(auto2) -> set(quiet). % 0.74/1.08 % set(auto2) -> clear(print_initial_clauses). % 0.74/1.08 % set(auto2) -> clear(print_given). % 0.74/1.08 assign(lrs_ticks,-1). % 0.74/1.08 assign(sos_limit,10000). % 0.74/1.08 assign(order,kbo). % 0.74/1.08 set(lex_order_vars). % 0.74/1.08 clear(print_given). % 0.74/1.08 % 0.74/1.08 % formulas(sos). % not echoed (24 formulas) % 0.74/1.08 % 0.74/1.08 ============================== end of input ========================== % 0.74/1.08 % 0.74/1.08 % From the command line: assign(max_seconds, 300). % 0.74/1.08 % 0.74/1.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.74/1.08 % 0.74/1.08 % Formulas that are not ordinary clauses: % 0.74/1.08 % 0.74/1.08 ============================== end of process non-clausal formulas === % 0.74/1.08 % 0.74/1.08 ============================== PROCESS INITIAL CLAUSES =============== % 0.74/1.08 % 0.74/1.08 ============================== PREDICATE ELIMINATION ================= % 0.74/1.08 % 0.74/1.08 ============================== end predicate elimination ============= % 0.74/1.08 % 0.74/1.08 Auto_denials: % 0.74/1.08 % copying label goal to answer in negative clause % 0.74/1.08 % 0.74/1.08 Term ordering decisions: % 0.74/1.08 % 0.74/1.08 % Assigning unary symbol s kb_weight 0 and highest precedence (15). % 0.74/1.08 Function symbol KB weights: bfalse=1. btrue=1. nil=1. z=1. cons=1. merge=1. eq=1. eq2=1. leqNat=1. impl=1. eq3=1. prop_merge_comm=1. aux=1. s=0. % 0.74/1.08 % 0.74/1.08 ============================== end of process initial clauses ======== % 0.74/1.08 % 0.74/1.08 ============================== CLAUSES FOR SEARCH ==================== % 0.74/1.08 % 0.74/1.08 ============================== end of clauses for search ============= % 0.74/1.08 % 0.74/1.08 ============================== SEARCH ================================ % 0.74/1.08 % 0.74/1.08 % Starting search at 0.01 seconds. % 0.74/1.08 % 0.74/1.08 ============================== PROOF ================================= % 0.74/1.08 % SZS status Unsatisfiable % 0.74/1.08 % SZS output start Refutation % 0.74/1.08 % 0.74/1.08 % Proof 1 at 0.12 (+ 0.01) seconds: goal. % 0.74/1.08 % Length of proof is 31. % 0.74/1.08 % Level of proof is 7. % 0.74/1.08 % Maximum clause weight is 28.000. % 0.74/1.08 % Given clauses 208. % 0.74/1.08 % 0.74/1.08 1 leqNat(z,A) = btrue # label(axiom_002) # label(axiom). [assumption]. % 0.74/1.08 2 merge(nil,A) = A # label(axiom_005) # label(axiom). [assumption]. % 0.74/1.08 3 impl(btrue,A) = A # label(axiom_008) # label(axiom). [assumption]. % 0.74/1.08 7 eq(A,A) = btrue # label(axiom_016) # label(axiom). [assumption]. % 0.74/1.08 8 eq2(A,A) = btrue # label(axiom_017) # label(axiom). [assumption]. % 0.74/1.08 9 eq3(A,A) = btrue # label(axiom_018) # label(axiom). [assumption]. % 0.74/1.08 12 eq2(s(A),z) = bfalse # label(axiom_015) # label(axiom). [assumption]. % 0.74/1.08 15 leqNat(s(A),s(B)) = leqNat(A,B) # label(axiom_004) # label(axiom). [assumption]. % 0.74/1.08 16 merge(cons(A,B),nil) = cons(A,B) # label(axiom_006) # label(axiom). [assumption]. % 0.74/1.08 18 aux(A,B,C,D,btrue) = cons(A,merge(B,cons(C,D))) # label(axiom) # label(axiom). [assumption]. % 0.74/1.08 19 cons(A,merge(B,cons(C,D))) = aux(A,B,C,D,btrue). [copy(18),flip(a)]. % 0.74/1.08 22 merge(cons(A,B),cons(C,D)) = aux(A,B,C,D,leqNat(A,C)) # label(axiom_007) # label(axiom). [assumption]. % 0.74/1.08 23 aux(A,B,C,D,leqNat(A,C)) = merge(cons(A,B),cons(C,D)). [copy(22),flip(a)]. % 0.74/1.08 24 prop_merge_comm(A,B,C) = impl(eq(merge(A,B),merge(B,A)),impl(eq(merge(A,C),merge(C,A)),eq(merge(B,C),merge(C,B)))) # label(axiom_010) # label(axiom). [assumption]. % 0.74/1.08 25 eq3(prop_merge_comm(A,B,C),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 0.74/1.08 26 eq3(impl(eq(merge(A,B),merge(B,A)),impl(eq(merge(A,C),merge(C,A)),eq(merge(B,C),merge(C,B)))),bfalse) != btrue # answer(goal). [copy(25),rewrite([24(1)])]. % 0.74/1.08 27 eq2(A,B) != bfalse | eq(cons(A,C),cons(B,D)) = bfalse # label(axiom_019) # label(axiom). [assumption]. % 0.74/1.08 28 eq2(A,B) != btrue | eq(cons(A,C),cons(B,D)) = eq(C,D) # label(axiom_020) # label(axiom). [assumption]. % 0.74/1.08 42 merge(cons(z,A),cons(B,C)) = aux(z,A,B,C,btrue). [para(1(a,1),23(a,1,5)),flip(a)]. % 0.74/1.08 44 aux(s(A),B,s(C),D,leqNat(A,C)) = merge(cons(s(A),B),cons(s(C),D)). [para(15(a,1),23(a,1,5))]. % 0.74/1.08 52 eq3(impl(eq(A,merge(A,nil)),eq(merge(cons(B,C),A),merge(A,cons(B,C)))),bfalse) != btrue # answer(goal). [para(16(a,1),26(a,1,1,1,2)),rewrite([2(3),7(3),2(3),3(11)])]. % 0.74/1.08 57 eq(cons(s(A),B),cons(z,C)) = bfalse. [hyper(27,a,12,a)]. % 0.74/1.08 61 eq(cons(A,B),cons(A,C)) = eq(B,C). [hyper(28,a,8,a)]. % 0.74/1.08 78 eq(cons(s(A),B),aux(z,C,D,E,btrue)) = bfalse. [para(19(a,1),57(a,1,2))]. % 0.74/1.08 85 eq(aux(A,B,C,D,btrue),cons(A,E)) = eq(merge(B,cons(C,D)),E). [para(19(a,1),61(a,1,1))]. % 0.74/1.08 222 merge(cons(s(z),A),cons(s(B),C)) = aux(s(z),A,s(B),C,btrue). [para(1(a,1),44(a,1,5)),flip(a)]. % 0.74/1.08 275 eq(aux(A,B,C,D,btrue),aux(A,E,F,V6,btrue)) = eq(merge(B,cons(C,D)),merge(E,cons(F,V6))). [para(19(a,1),85(a,1,2))]. % 0.74/1.08 396 eq3(eq(aux(s(z),A,s(B),C,btrue),merge(cons(s(B),C),cons(s(z),A))),bfalse) != btrue # answer(goal). [para(222(a,1),52(a,1,1,2,1)),rewrite([16(6),7(5),3(14)])]. % 0.74/1.08 484 eq3(eq(merge(A,cons(s(z),B)),merge(B,cons(s(z),A))),bfalse) != btrue # answer(goal). [para(222(a,1),396(a,1,1,2)),rewrite([275(13)])]. % 0.74/1.08 485 eq3(eq(cons(s(z),A),merge(A,cons(s(z),nil))),bfalse) != btrue # answer(goal). [para(2(a,1),484(a,1,1,1))]. % 0.74/1.08 499 $F # answer(goal). [para(42(a,1),485(a,1,1,2)),rewrite([78(12),9(3)]),xx(a)]. % 0.74/1.08 % 0.74/1.08 % SZS output end Refutation % 0.74/1.08 ============================== end of proof ========================== % 0.74/1.08 % 0.74/1.08 ============================== STATISTICS ============================ % 0.74/1.08 % 0.74/1.08 Given=208. Generated=2542. Kept=494. proofs=1. % 0.74/1.08 Usable=200. Sos=242. Demods=148. Limbo=2, Disabled=74. Hints=0. % 0.74/1.08 Megabytes=0.92. % 0.74/1.08 User_CPU=0.12, System_CPU=0.01, Wall_clock=1. % 0.74/1.08 % 0.74/1.08 ============================== end of statistics ===================== % 0.74/1.08 % 0.74/1.08 ============================== end of search ========================= % 0.74/1.08 % 0.74/1.08 THEOREM PROVED % 0.74/1.08 % SZS status Unsatisfiable % 0.74/1.08 % 0.74/1.08 Exiting with 1 proof. % 0.74/1.08 % 0.74/1.08 Process 15262 exit (max_proofs) Wed Apr 29 00:33:30 2026 % 0.74/1.08 Prover9 interrupted %------------------------------------------------------------------------------