%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n006.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 0.76s 1.54s % Output : Refutation 0.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX242-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 : n006.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 03:15:00 EDT 2026 % 0.16/0.35 % CPUTime : % 0.76/1.53 ============================== Prover9 =============================== % 0.76/1.53 Prover9 (32) version 2009-11A, November 2009. % 0.76/1.53 Process 7651 was started by sandbox on n006.cluster.edu, % 0.76/1.53 Wed Apr 29 03:15:01 2026 % 0.76/1.53 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_7498_n006.cluster.edu". % 0.76/1.53 ============================== end of head =========================== % 0.76/1.53 % 0.76/1.53 ============================== INPUT ================================= % 0.76/1.53 % 0.76/1.53 % Reading from file /tmp/Prover9_7498_n006.cluster.edu % 0.76/1.53 % 0.76/1.53 set(prolog_style_variables). % 0.76/1.53 set(auto2). % 0.76/1.53 % set(auto2) -> set(auto). % 0.76/1.53 % set(auto) -> set(auto_inference). % 0.76/1.53 % set(auto) -> set(auto_setup). % 0.76/1.53 % set(auto_setup) -> set(predicate_elim). % 0.76/1.53 % set(auto_setup) -> assign(eq_defs, unfold). % 0.76/1.53 % set(auto) -> set(auto_limits). % 0.76/1.53 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.76/1.53 % set(auto_limits) -> assign(sos_limit, 20000). % 0.76/1.53 % set(auto) -> set(auto_denials). % 0.76/1.53 % set(auto) -> set(auto_process). % 0.76/1.53 % set(auto2) -> assign(new_constants, 1). % 0.76/1.53 % set(auto2) -> assign(fold_denial_max, 3). % 0.76/1.53 % set(auto2) -> assign(max_weight, "200.000"). % 0.76/1.53 % set(auto2) -> assign(max_hours, 1). % 0.76/1.53 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.76/1.53 % set(auto2) -> assign(max_seconds, 0). % 0.76/1.53 % set(auto2) -> assign(max_minutes, 5). % 0.76/1.53 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.76/1.53 % set(auto2) -> set(sort_initial_sos). % 0.76/1.53 % set(auto2) -> assign(sos_limit, -1). % 0.76/1.53 % set(auto2) -> assign(lrs_ticks, 3000). % 0.76/1.53 % set(auto2) -> assign(max_megs, 400). % 0.76/1.53 % set(auto2) -> assign(stats, some). % 0.76/1.53 % set(auto2) -> clear(echo_input). % 0.76/1.53 % set(auto2) -> set(quiet). % 0.76/1.53 % set(auto2) -> clear(print_initial_clauses). % 0.76/1.53 % set(auto2) -> clear(print_given). % 0.76/1.53 assign(lrs_ticks,-1). % 0.76/1.53 assign(sos_limit,10000). % 0.76/1.53 assign(order,kbo). % 0.76/1.53 set(lex_order_vars). % 0.76/1.53 clear(print_given). % 0.76/1.53 % 0.76/1.53 % formulas(sos). % not echoed (73 formulas) % 0.76/1.53 % 0.76/1.53 ============================== end of input ========================== % 0.76/1.53 % 0.76/1.53 % From the command line: assign(max_seconds, 300). % 0.76/1.53 % 0.76/1.53 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.76/1.53 % 0.76/1.53 % Formulas that are not ordinary clauses: % 0.76/1.53 % 0.76/1.53 ============================== end of process non-clausal formulas === % 0.76/1.53 % 0.76/1.53 ============================== PROCESS INITIAL CLAUSES =============== % 0.76/1.53 % 0.76/1.53 ============================== PREDICATE ELIMINATION ================= % 0.76/1.53 % 0.76/1.53 ============================== end predicate elimination ============= % 0.76/1.53 % 0.76/1.53 Auto_denials: % 0.76/1.53 % copying label goal to answer in negative clause % 0.76/1.53 % 0.76/1.53 Term ordering decisions: % 0.76/1.53 Function symbol KB weights: bfalse=1. btrue=1. nil=1. nothing=1. a=1. b=1. c=1. lam3=1. cons=1. app=1. eq2=1. eq3=1. apply1=1. eq=1. subst=1. substList=1. append=1. eq4=1. unify=1. unifyoccurs=1. orb=1. lam=1. unificationOK=1. unify2=1. prop_unify_makes_equal=1. var=1. just=1. isJust2=1. unifyloop=1. sub=1. aux6=1. lam2=1. singleton=1. substSubst=1. fail=1. aux=1. extend=1. unifyvar=1. aux2=1. aux7=1. unifybind=1. aux5=1. aux4=1. aux3=1. % 0.76/1.53 % 0.76/1.53 ============================== end of process initial clauses ======== % 0.76/1.53 % 0.76/1.53 ============================== CLAUSES FOR SEARCH ==================== % 0.76/1.54 % 0.76/1.54 ============================== end of clauses for search ============= % 0.76/1.54 % 0.76/1.54 ============================== SEARCH ================================ % 0.76/1.54 % 0.76/1.54 % Starting search at 0.02 seconds. % 0.76/1.54 % 0.76/1.54 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 1269 (0.00 of 0.33 sec). % 0.76/1.54 % 0.76/1.54 ============================== PROOF ================================= % 0.76/1.54 % SZS status Unsatisfiable % 0.76/1.54 % SZS output start Refutation % 0.76/1.54 % 0.76/1.54 % Proof 1 at 0.51 (+ 0.01) seconds: goal. % 0.76/1.54 % Length of proof is 52. % 0.76/1.54 % Level of proof is 17. % 0.76/1.54 % Maximum clause weight is 35.000. % 0.76/1.54 % Given clauses 659. % 0.76/1.54 % 0.76/1.54 2 substList(A,nil) = nil # label(axiom_020) # label(axiom). [assumption]. % 0.76/1.54 7 append(nil,A) = A # label(axiom_046) # label(axiom). [assumption]. % 0.76/1.54 14 eq4(bfalse,btrue) = bfalse # label(axiom_054) # label(axiom). [assumption]. % 0.76/1.54 16 eq2(A,A) = btrue # label(axiom_056) # label(axiom). [assumption]. % 0.76/1.54 18 eq4(A,A) = btrue # label(axiom_058) # label(axiom). [assumption]. % 0.76/1.54 21 apply1(lam3,A) = var(A) # label(axiom_071) # label(axiom). [assumption]. % 0.76/1.54 24 unifyloop(A,nil,nil) = just(A) # label(axiom_031) # label(axiom). [assumption]. % 0.76/1.54 25 just(A) = unifyloop(A,nil,nil). [copy(24),flip(a)]. % 0.76/1.54 27 eq(cons(A,B),nil) = bfalse # label(axiom_063) # label(axiom). [assumption]. % 0.76/1.54 31 subst(A,var(B)) = apply1(A,B) # label(axiom_019) # label(axiom). [assumption]. % 0.76/1.54 38 prop_unify_makes_equal(A,B) = eq4(unificationOK(A,B),btrue) # label(axiom_043) # label(axiom). [assumption]. % 0.76/1.54 44 unificationOK(A,B) = aux6(A,B,unify2(A,B)) # label(axiom_042) # label(axiom). [assumption]. % 0.76/1.54 47 subst(A,app(B,C)) = app(B,substList(A,C)) # label(axiom_018) # label(axiom). [assumption]. % 0.76/1.54 48 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_047) # label(axiom). [assumption]. % 0.76/1.54 49 aux5(A,B,C,D,E,btrue) = unifyloop(A,C,D) # label(axiom_008) # label(axiom). [assumption]. % 0.76/1.54 52 unify2(A,B) = unifyloop(lam3,cons(A,nil),cons(B,nil)) # label(axiom_041) # label(axiom). [assumption]. % 0.76/1.54 53 aux6(A,B,just(C)) = eq3(subst(C,A),subst(C,B)) # label(axiom_011) # label(axiom). [assumption]. % 0.76/1.54 54 eq3(subst(A,B),subst(A,C)) = aux6(B,C,unifyloop(A,nil,nil)). [copy(53),rewrite([25(1)]),flip(a)]. % 0.76/1.54 55 substList(A,cons(B,C)) = cons(subst(A,B),substList(A,C)) # label(axiom_021) # label(axiom). [assumption]. % 0.76/1.54 56 cons(subst(A,B),substList(A,C)) = substList(A,cons(B,C)). [copy(55),flip(a)]. % 0.76/1.54 71 unifyloop(A,cons(var(B),C),cons(D,E)) = unifyvar(A,B,D,C,E) # label(axiom_037) # label(axiom). [assumption]. % 0.76/1.54 73 unifyvar(A,B,var(C),D,E) = aux5(A,B,D,E,C,eq2(B,C)) # label(axiom_039) # label(axiom). [assumption]. % 0.76/1.54 74 aux5(A,B,C,D,E,eq2(B,E)) = unifyvar(A,B,var(E),C,D). [copy(73),flip(a)]. % 0.76/1.54 75 aux3(A,B,C,D,E,F,V6,btrue) = unifyloop(A,append(D,B),append(V6,E)) # label(axiom_004) # label(axiom). [assumption]. % 0.76/1.54 82 unifyloop(A,cons(app(B,C),D),cons(app(E,F),V6)) = aux3(A,D,B,C,V6,E,F,eq2(B,E)) # label(axiom_034) # label(axiom). [assumption]. % 0.76/1.54 85 eq4(prop_unify_makes_equal(A,B),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 0.76/1.54 86 eq4(eq4(aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))),btrue),bfalse) != btrue # answer(goal). [copy(85),rewrite([38(1),44(1),52(1)])]. % 0.76/1.54 87 eq3(A,B) != bfalse | eq(cons(A,C),cons(B,D)) = bfalse # label(axiom_060) # label(axiom). [assumption]. % 0.76/1.54 90 eq2(A,B) != btrue | eq3(app(A,C),app(B,D)) = eq(C,D) # label(axiom_065) # label(axiom). [assumption]. % 0.76/1.54 112 substList(A,cons(B,nil)) = cons(subst(A,B),nil). [para(2(a,1),56(a,1,2)),flip(a)]. % 0.76/1.54 118 cons(app(A,substList(B,C)),substList(B,D)) = substList(B,cons(app(A,C),D)). [para(47(a,1),56(a,1,1))]. % 0.76/1.54 144 unifyvar(A,B,var(B),C,D) = unifyloop(A,C,D). [para(16(a,1),74(a,1,6)),rewrite([49(2)]),flip(a)]. % 0.76/1.54 155 eq4(eq4(aux6(app(A,B),app(C,D),aux3(lam3,nil,A,B,nil,C,D,eq2(A,C))),btrue),bfalse) != btrue # answer(goal). [para(82(a,1),86(a,1,1,1,3))]. % 0.76/1.54 172 eq3(app(A,B),app(A,C)) = eq(B,C). [hyper(90,a,16,a)]. % 0.76/1.54 180 eq4(eq4(aux6(app(A,B),app(A,C),unifyloop(lam3,append(B,nil),append(C,nil))),btrue),bfalse) != btrue # answer(goal). [para(16(a,1),155(a,1,1,1,3,8)),rewrite([75(7)])]. % 0.76/1.54 183 eq4(eq4(aux6(app(A,cons(B,C)),app(A,D),unifyloop(lam3,cons(B,append(C,nil)),append(D,nil))),btrue),bfalse) != btrue # answer(goal). [para(48(a,1),180(a,1,1,1,3,2))]. % 0.76/1.54 188 eq4(eq4(aux6(app(A,cons(B,nil)),app(A,C),unifyloop(lam3,cons(B,nil),append(C,nil))),btrue),bfalse) != btrue # answer(goal). [para(7(a,1),183(a,1,1,1,3,2,2))]. % 0.76/1.54 191 eq4(eq4(aux6(app(A,cons(B,nil)),app(A,cons(C,D)),unifyloop(lam3,cons(B,nil),cons(C,append(D,nil)))),btrue),bfalse) != btrue # answer(goal). [para(48(a,1),188(a,1,1,1,3,3))]. % 0.76/1.54 212 eq4(eq4(aux6(app(A,cons(app(B,C),nil)),app(A,cons(app(D,E),F)),aux3(lam3,nil,B,C,append(F,nil),D,E,eq2(B,D))),btrue),bfalse) != btrue # answer(goal). [para(82(a,1),191(a,1,1,1,3))]. % 0.76/1.54 267 eq(A,B) != bfalse | eq(cons(app(C,A),D),cons(app(C,B),E)) = bfalse. [para(172(a,1),87(a,1))]. % 0.76/1.54 354 substList(A,cons(app(B,nil),C)) = cons(app(B,nil),substList(A,C)). [para(2(a,1),118(a,1,1,2)),flip(a)]. % 0.76/1.54 649 eq4(eq4(aux6(app(A,cons(app(B,C),nil)),app(A,cons(app(B,D),E)),unifyloop(lam3,append(C,nil),append(D,append(E,nil)))),btrue),bfalse) != btrue # answer(goal). [para(16(a,1),212(a,1,1,1,3,8)),rewrite([75(13)])]. % 0.76/1.54 652 eq4(eq4(aux6(app(A,cons(app(B,C),nil)),app(A,cons(app(B,nil),D)),unifyloop(lam3,append(C,nil),append(D,nil))),btrue),bfalse) != btrue # answer(goal). [para(7(a,1),649(a,1,1,1,3,3))]. % 0.76/1.54 674 eq4(eq4(aux6(app(A,cons(app(B,cons(C,D)),nil)),app(A,cons(app(B,nil),E)),unifyloop(lam3,cons(C,append(D,nil)),append(E,nil))),btrue),bfalse) != btrue # answer(goal). [para(48(a,1),652(a,1,1,1,3,2))]. % 0.76/1.54 684 eq4(eq4(aux6(app(A,cons(app(B,cons(C,nil)),nil)),app(A,cons(app(B,nil),D)),unifyloop(lam3,cons(C,nil),append(D,nil))),btrue),bfalse) != btrue # answer(goal). [para(7(a,1),674(a,1,1,1,3,2,2))]. % 0.76/1.54 687 eq4(eq4(aux6(app(A,cons(app(B,cons(C,nil)),nil)),app(A,cons(app(B,nil),cons(D,E))),unifyloop(lam3,cons(C,nil),cons(D,append(E,nil)))),btrue),bfalse) != btrue # answer(goal). [para(48(a,1),684(a,1,1,1,3,3))]. % 0.76/1.54 1212 eq4(eq4(aux6(app(A,cons(app(B,cons(C,nil)),nil)),app(A,cons(app(B,nil),cons(D,nil))),unifyloop(lam3,cons(C,nil),cons(D,nil))),btrue),bfalse) != btrue # answer(goal). [para(7(a,1),687(a,1,1,1,3,3,2))]. % 0.76/1.54 1218 eq4(eq4(aux6(app(A,cons(app(B,cons(var(C),nil)),nil)),app(A,cons(app(B,nil),cons(D,nil))),unifyvar(lam3,C,D,nil,nil)),btrue),bfalse) != btrue # answer(goal). [para(71(a,1),1212(a,1,1,1,3))]. % 0.76/1.54 1222 eq4(eq4(aux6(app(A,cons(app(B,cons(var(C),nil)),nil)),app(A,cons(app(B,nil),cons(var(C),nil))),unifyloop(lam3,nil,nil)),btrue),bfalse) != btrue # answer(goal). [para(144(a,1),1218(a,1,1,1,3))]. % 0.76/1.54 1239 eq4(eq4(eq(cons(app(A,cons(var(B),nil)),nil),cons(app(A,nil),cons(var(B),nil))),btrue),bfalse) != btrue # answer(goal). [para(54(a,2),1222(a,1,1,1)),rewrite([47(9),112(8),47(6),112(5),31(3),21(2),47(16),354(15),112(14),31(12),21(11),172(15)])]. % 0.76/1.54 1923 eq(cons(app(A,cons(B,C)),D),cons(app(A,nil),E)) = bfalse. [hyper(267,a,27,a)]. % 0.76/1.54 1928 $F # answer(goal). [back_rewrite(1239),rewrite([1923(13),14(3),18(3)]),xx(a)]. % 0.76/1.54 % 0.76/1.54 % SZS output end Refutation % 0.76/1.54 ============================== end of proof ========================== % 0.76/1.54 % 0.76/1.54 ============================== STATISTICS ============================ % 0.76/1.54 % 0.76/1.54 Given=659. Generated=8389. Kept=1910. proofs=1. % 0.76/1.54 Usable=658. Sos=1237. Demods=907. Limbo=5, Disabled=83. Hints=0. % 0.76/1.54 Megabytes=3.67. % 0.76/1.54 User_CPU=0.51, System_CPU=0.01, Wall_clock=1. % 0.76/1.54 % 0.76/1.54 ============================== end of statistics ===================== % 0.76/1.54 % 0.76/1.54 ============================== end of search ========================= % 0.76/1.54 % 0.76/1.54 THEOREM PROVED % 0.76/1.54 % SZS status Unsatisfiable % 0.76/1.54 % 0.76/1.54 Exiting with 1 proof. % 0.76/1.54 % 0.76/1.54 Process 7651 exit (max_proofs) Wed Apr 29 03:15:02 2026 % 0.76/1.54 Prover9 interrupted %------------------------------------------------------------------------------