%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX228-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n021.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:08 PM UTC 2026 % Result : Unsatisfiable 0.79s 1.08s % Output : Refutation 0.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX228-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.34 % Computer : n021.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Wed Apr 29 02:36:35 EDT 2026 % 0.16/0.34 % CPUTime : % 0.79/1.08 ============================== Prover9 =============================== % 0.79/1.08 Prover9 (32) version 2009-11A, November 2009. % 0.79/1.08 Process 10815 was started by sandbox on n021.cluster.edu, % 0.79/1.08 Wed Apr 29 02:36:36 2026 % 0.79/1.08 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_10662_n021.cluster.edu". % 0.79/1.08 ============================== end of head =========================== % 0.79/1.08 % 0.79/1.08 ============================== INPUT ================================= % 0.79/1.08 % 0.79/1.08 % Reading from file /tmp/Prover9_10662_n021.cluster.edu % 0.79/1.08 % 0.79/1.08 set(prolog_style_variables). % 0.79/1.08 set(auto2). % 0.79/1.08 % set(auto2) -> set(auto). % 0.79/1.08 % set(auto) -> set(auto_inference). % 0.79/1.08 % set(auto) -> set(auto_setup). % 0.79/1.08 % set(auto_setup) -> set(predicate_elim). % 0.79/1.08 % set(auto_setup) -> assign(eq_defs, unfold). % 0.79/1.08 % set(auto) -> set(auto_limits). % 0.79/1.08 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.79/1.08 % set(auto_limits) -> assign(sos_limit, 20000). % 0.79/1.08 % set(auto) -> set(auto_denials). % 0.79/1.08 % set(auto) -> set(auto_process). % 0.79/1.08 % set(auto2) -> assign(new_constants, 1). % 0.79/1.08 % set(auto2) -> assign(fold_denial_max, 3). % 0.79/1.08 % set(auto2) -> assign(max_weight, "200.000"). % 0.79/1.08 % set(auto2) -> assign(max_hours, 1). % 0.79/1.08 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.79/1.08 % set(auto2) -> assign(max_seconds, 0). % 0.79/1.08 % set(auto2) -> assign(max_minutes, 5). % 0.79/1.08 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.79/1.08 % set(auto2) -> set(sort_initial_sos). % 0.79/1.08 % set(auto2) -> assign(sos_limit, -1). % 0.79/1.08 % set(auto2) -> assign(lrs_ticks, 3000). % 0.79/1.08 % set(auto2) -> assign(max_megs, 400). % 0.79/1.08 % set(auto2) -> assign(stats, some). % 0.79/1.08 % set(auto2) -> clear(echo_input). % 0.79/1.08 % set(auto2) -> set(quiet). % 0.79/1.08 % set(auto2) -> clear(print_initial_clauses). % 0.79/1.08 % set(auto2) -> clear(print_given). % 0.79/1.08 assign(lrs_ticks,-1). % 0.79/1.08 assign(sos_limit,10000). % 0.79/1.08 assign(order,kbo). % 0.79/1.08 set(lex_order_vars). % 0.79/1.08 clear(print_given). % 0.79/1.08 % 0.79/1.08 % formulas(sos). % not echoed (26 formulas) % 0.79/1.08 % 0.79/1.08 ============================== end of input ========================== % 0.79/1.08 % 0.79/1.08 % From the command line: assign(max_seconds, 300). % 0.79/1.08 % 0.79/1.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.79/1.08 % 0.79/1.08 % Formulas that are not ordinary clauses: % 0.79/1.08 % 0.79/1.08 ============================== end of process non-clausal formulas === % 0.79/1.08 % 0.79/1.08 ============================== PROCESS INITIAL CLAUSES =============== % 0.79/1.08 % 0.79/1.08 ============================== PREDICATE ELIMINATION ================= % 0.79/1.08 % 0.79/1.08 ============================== end predicate elimination ============= % 0.79/1.08 % 0.79/1.08 Auto_denials: % 0.79/1.08 % copying label goal to answer in negative clause % 0.79/1.08 % 0.79/1.08 Term ordering decisions: % 0.79/1.08 % 0.79/1.08 % Assigning unary symbol s kb_weight 0 and highest precedence (16). % 0.79/1.08 Function symbol KB weights: bfalse=1. btrue=1. z=1. nil=1. cons=1. eq=1. eq2=1. eqNat=1. union=1. elem=1. barbar=1. eq3=1. prop_union_comm=1. aux=1. s=0. % 0.79/1.08 % 0.79/1.08 ============================== end of process initial clauses ======== % 0.79/1.08 % 0.79/1.08 ============================== CLAUSES FOR SEARCH ==================== % 0.79/1.08 % 0.79/1.08 ============================== end of clauses for search ============= % 0.79/1.08 % 0.79/1.08 ============================== SEARCH ================================ % 0.79/1.08 % 0.79/1.08 % Starting search at 0.01 seconds. % 0.79/1.08 % 0.79/1.08 ============================== PROOF ================================= % 0.79/1.08 % SZS status Unsatisfiable % 0.79/1.08 % SZS output start Refutation % 0.79/1.08 % 0.79/1.08 % Proof 1 at 0.02 (+ 0.00) seconds: goal. % 0.79/1.08 % Length of proof is 39. % 0.79/1.08 % Level of proof is 12. % 0.79/1.08 % Maximum clause weight is 18.000. % 0.79/1.08 % Given clauses 49. % 0.79/1.08 % 0.79/1.08 1 barbar(btrue,A) = btrue # label(axiom_002) # label(axiom). [assumption]. % 0.79/1.08 3 eqNat(z,z) = btrue # label(axiom_007) # label(axiom). [assumption]. % 0.79/1.08 4 btrue = eqNat(z,z). [copy(3),flip(a)]. % 0.79/1.08 6 union(nil,A) = A # label(axiom_010) # label(axiom). [assumption]. % 0.79/1.08 11 eq(A,A) = btrue # label(axiom_018) # label(axiom). [assumption]. % 0.79/1.08 12 eq(A,A) = eqNat(z,z). [copy(11),rewrite([4(2)])]. % 0.79/1.08 13 eq2(A,A) = btrue # label(axiom_019) # label(axiom). [assumption]. % 0.79/1.08 14 eq2(A,A) = eqNat(z,z). [copy(13),rewrite([4(2)])]. % 0.79/1.08 15 eq3(A,A) = btrue # label(axiom_020) # label(axiom). [assumption]. % 0.79/1.08 16 eq3(A,A) = eqNat(z,z). [copy(15),rewrite([4(2)])]. % 0.79/1.08 22 eq(cons(A,B),nil) = bfalse # label(axiom_024) # label(axiom). [assumption]. % 0.79/1.08 23 aux(A,B,C,btrue) = union(C,A) # label(axiom) # label(axiom). [assumption]. % 0.79/1.08 24 aux(A,B,C,eqNat(z,z)) = union(C,A). [copy(23),rewrite([4(1)])]. % 0.79/1.08 28 prop_union_comm(A,B) = eq(union(A,B),union(B,A)) # label(axiom_012) # label(axiom). [assumption]. % 0.79/1.08 29 elem(A,cons(B,C)) = barbar(eqNat(A,B),elem(A,C)) # label(axiom_009) # label(axiom). [assumption]. % 0.79/1.08 30 barbar(eqNat(A,B),elem(A,C)) = elem(A,cons(B,C)). [copy(29),flip(a)]. % 0.79/1.08 31 union(cons(A,B),C) = aux(C,A,B,elem(A,C)) # label(axiom_011) # label(axiom). [assumption]. % 0.79/1.08 32 aux(A,B,C,elem(B,A)) = union(cons(B,C),A). [copy(31),flip(a)]. % 0.79/1.08 33 eq3(prop_union_comm(A,B),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 0.79/1.08 34 eq3(eq(union(A,B),union(B,A)),bfalse) != eqNat(z,z) # answer(goal). [copy(33),rewrite([28(1),4(6)])]. % 0.79/1.08 36 eq2(A,B) != btrue | eq(cons(A,C),cons(B,D)) = eq(C,D) # label(axiom_022) # label(axiom). [assumption]. % 0.79/1.08 37 eq2(A,B) != eqNat(z,z) | eq(cons(A,C),cons(B,D)) = eq(C,D). [copy(36),rewrite([4(2)])]. % 0.79/1.08 38 barbar(eqNat(z,z),A) = eqNat(z,z). [back_rewrite(1),rewrite([4(1),4(5)])]. % 0.79/1.08 41 eq(A,A) = eq(B,B). [para(12(a,2),12(a,2))]. % 0.79/1.08 42 eq(A,A) = c_0. [new_symbol(41)]. % 0.79/1.08 45 eqNat(z,z) = c_0. [back_rewrite(12),rewrite([42(1)]),flip(a)]. % 0.79/1.08 46 barbar(c_0,A) = c_0. [back_rewrite(38),rewrite([45(3),45(5)])]. % 0.79/1.08 47 eq2(A,B) != c_0 | eq(cons(A,C),cons(B,D)) = eq(C,D). [back_rewrite(37),rewrite([45(4)])]. % 0.79/1.08 48 eq3(eq(union(A,B),union(B,A)),bfalse) != c_0 # answer(goal). [back_rewrite(34),rewrite([45(8)])]. % 0.79/1.08 49 aux(A,B,C,c_0) = union(C,A). [back_rewrite(24),rewrite([45(3)])]. % 0.79/1.08 50 eq3(A,A) = c_0. [back_rewrite(16),rewrite([45(4)])]. % 0.79/1.08 51 eq2(A,A) = c_0. [back_rewrite(14),rewrite([45(4)])]. % 0.79/1.08 64 elem(z,cons(z,A)) = c_0. [para(45(a,1),30(a,1,1)),rewrite([46(4)]),flip(a)]. % 0.79/1.08 66 union(cons(z,A),cons(z,B)) = union(A,cons(z,B)). [para(64(a,1),32(a,1,4)),rewrite([49(5)]),flip(a)]. % 0.79/1.08 67 eq(cons(A,B),cons(A,C)) = eq(B,C). [hyper(47,a,51,a)]. % 0.79/1.08 76 eq3(eq(union(A,cons(z,B)),union(B,cons(z,A))),bfalse) != c_0 # answer(goal). [para(66(a,1),48(a,1,1,1)),rewrite([66(8)])]. % 0.79/1.08 81 eq3(eq(cons(z,A),union(A,cons(z,nil))),bfalse) != c_0 # answer(goal). [para(6(a,1),76(a,1,1,1))]. % 0.79/1.08 85 eq3(eq(cons(z,cons(z,A)),union(A,cons(z,nil))),bfalse) != c_0 # answer(goal). [para(66(a,1),81(a,1,1,2))]. % 0.79/1.08 87 $F # answer(goal). [para(6(a,1),85(a,1,1,2)),rewrite([67(9),22(5),50(3)]),xx(a)]. % 0.79/1.08 % 0.79/1.08 % SZS output end Refutation % 0.79/1.08 ============================== end of proof ========================== % 0.79/1.08 % 0.79/1.08 ============================== STATISTICS ============================ % 0.79/1.08 % 0.79/1.08 Given=49. Generated=199. Kept=75. proofs=1. % 0.79/1.08 Usable=45. Sos=16. Demods=45. Limbo=0, Disabled=40. Hints=0. % 0.79/1.08 Megabytes=0.12. % 0.79/1.08 User_CPU=0.02, System_CPU=0.00, Wall_clock=0. % 0.79/1.08 % 0.79/1.08 ============================== end of statistics ===================== % 0.79/1.08 % 0.79/1.08 ============================== end of search ========================= % 0.79/1.08 % 0.79/1.08 THEOREM PROVED % 0.79/1.08 % SZS status Unsatisfiable % 0.79/1.08 % 0.79/1.08 Exiting with 1 proof. % 0.79/1.08 % 0.79/1.08 Process 10815 exit (max_proofs) Wed Apr 29 02:36:36 2026 % 0.79/1.08 Prover9 interrupted %------------------------------------------------------------------------------