%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX185-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n018.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:02 PM UTC 2026 % Result : Unsatisfiable 2.12s 2.47s % Output : Refutation 2.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX185-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.33 % Computer : n018.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue Apr 28 23:29:46 EDT 2026 % 0.16/0.33 % CPUTime : % 2.12/2.47 ============================== Prover9 =============================== % 2.12/2.47 Prover9 (32) version 2009-11A, November 2009. % 2.12/2.47 Process 1614 was started by sandbox2 on n018.cluster.edu, % 2.12/2.47 Tue Apr 28 23:29:47 2026 % 2.12/2.47 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_1459_n018.cluster.edu". % 2.12/2.47 ============================== end of head =========================== % 2.12/2.47 % 2.12/2.47 ============================== INPUT ================================= % 2.12/2.47 % 2.12/2.47 % Reading from file /tmp/Prover9_1459_n018.cluster.edu % 2.12/2.47 % 2.12/2.47 set(prolog_style_variables). % 2.12/2.47 set(auto2). % 2.12/2.47 % set(auto2) -> set(auto). % 2.12/2.47 % set(auto) -> set(auto_inference). % 2.12/2.47 % set(auto) -> set(auto_setup). % 2.12/2.47 % set(auto_setup) -> set(predicate_elim). % 2.12/2.47 % set(auto_setup) -> assign(eq_defs, unfold). % 2.12/2.47 % set(auto) -> set(auto_limits). % 2.12/2.47 % set(auto_limits) -> assign(max_weight, "100.000"). % 2.12/2.47 % set(auto_limits) -> assign(sos_limit, 20000). % 2.12/2.47 % set(auto) -> set(auto_denials). % 2.12/2.47 % set(auto) -> set(auto_process). % 2.12/2.47 % set(auto2) -> assign(new_constants, 1). % 2.12/2.47 % set(auto2) -> assign(fold_denial_max, 3). % 2.12/2.47 % set(auto2) -> assign(max_weight, "200.000"). % 2.12/2.47 % set(auto2) -> assign(max_hours, 1). % 2.12/2.47 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 2.12/2.47 % set(auto2) -> assign(max_seconds, 0). % 2.12/2.47 % set(auto2) -> assign(max_minutes, 5). % 2.12/2.47 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 2.12/2.47 % set(auto2) -> set(sort_initial_sos). % 2.12/2.47 % set(auto2) -> assign(sos_limit, -1). % 2.12/2.47 % set(auto2) -> assign(lrs_ticks, 3000). % 2.12/2.47 % set(auto2) -> assign(max_megs, 400). % 2.12/2.47 % set(auto2) -> assign(stats, some). % 2.12/2.47 % set(auto2) -> clear(echo_input). % 2.12/2.47 % set(auto2) -> set(quiet). % 2.12/2.47 % set(auto2) -> clear(print_initial_clauses). % 2.12/2.47 % set(auto2) -> clear(print_given). % 2.12/2.47 assign(lrs_ticks,-1). % 2.12/2.47 assign(sos_limit,10000). % 2.12/2.47 assign(order,kbo). % 2.12/2.47 set(lex_order_vars). % 2.12/2.47 clear(print_given). % 2.12/2.47 % 2.12/2.47 % formulas(sos). % not echoed (77 formulas) % 2.12/2.47 % 2.12/2.47 ============================== end of input ========================== % 2.12/2.47 % 2.12/2.47 % From the command line: assign(max_seconds, 300). % 2.12/2.47 % 2.12/2.47 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 2.12/2.47 % 2.12/2.47 % Formulas that are not ordinary clauses: % 2.12/2.47 % 2.12/2.47 ============================== end of process non-clausal formulas === % 2.12/2.47 % 2.12/2.47 ============================== PROCESS INITIAL CLAUSES =============== % 2.12/2.47 % 2.12/2.47 ============================== PREDICATE ELIMINATION ================= % 2.12/2.47 % 2.12/2.47 ============================== end predicate elimination ============= % 2.12/2.47 % 2.12/2.47 Auto_denials: % 2.12/2.47 % copying label goal to answer in negative clause % 2.12/2.47 % 2.12/2.47 Term ordering decisions: % 2.12/2.47 Function symbol KB weights: bfalse=1. eX=1. eY=1. btrue=1. c=1. d=1. mul=1. plus=1. x=1. y=1. nil=1. eq2=1. eq3=1. z=1. x2=1. cons=1. append=1. eq=1. eq4=1. impl=1. prop_unambig=1. assoc=1. lin=1. linTerm=1. % 2.12/2.47 % 2.12/2.47 ============================== end of process initial clauses ======== % 2.12/2.47 % 2.12/2.47 ============================== CLAUSES FOR SEARCH ==================== % 2.12/2.47 % 2.12/2.47 ============================== end of clauses for search ============= % 2.12/2.47 % 2.12/2.47 ============================== SEARCH ================================ % 2.12/2.47 % 2.12/2.47 % Starting search at 0.01 seconds. % 2.12/2.47 % 2.12/2.47 Low Water (keep): wt=33.000, iters=3394 % 2.12/2.47 % 2.12/2.47 Low Water (keep): wt=32.000, iters=3362 % 2.12/2.47 % 2.12/2.47 Low Water (keep): wt=31.000, iters=3333 % 2.12/2.47 % 2.12/2.47 Low Water (keep): wt=29.000, iters=3415 % 2.12/2.47 % 2.12/2.47 Low Water (keep): wt=26.000, iters=3363 % 2.12/2.47 % 2.12/2.47 ============================== PROOF ================================= % 2.12/2.47 % SZS status Unsatisfiable % 2.12/2.47 % SZS output start Refutation % 2.12/2.47 % 2.12/2.47 % Proof 1 at 1.45 (+ 0.03) seconds: goal. % 2.12/2.47 % Length of proof is 38. % 2.12/2.47 % Level of proof is 8. % 2.12/2.47 % Maximum clause weight is 21.000. % 2.12/2.47 % Given clauses 1240. % 2.12/2.47 % 2.12/2.47 1 assoc(eX) = eX # label(axiom_007) # label(axiom). [assumption]. % 2.12/2.47 3 impl(btrue,A) = A # label(axiom) # label(axiom). [assumption]. % 2.12/2.47 5 append(nil,A) = A # label(axiom_009) # label(axiom). [assumption]. % 2.12/2.47 8 eq2(c,d) = bfalse # label(axiom_020) # label(axiom). [assumption]. % 2.12/2.47 9 bfalse = eq2(c,d). [copy(8),flip(a)]. % 2.12/2.47 76 eq(A,A) = btrue # label(axiom_068) # label(axiom). [assumption]. % 2.12/2.47 77 eq2(A,A) = btrue # label(axiom_069) # label(axiom). [assumption]. % 2.12/2.47 79 eq4(A,A) = btrue # label(axiom_071) # label(axiom). [assumption]. % 2.12/2.47 80 lin(eX) = cons(x,nil) # label(axiom_017) # label(axiom). [assumption]. % 2.12/2.47 81 cons(x,nil) = lin(eX). [copy(80),flip(a)]. % 2.12/2.47 88 eq3(x2(A,B),eX) = bfalse # label(axiom_062) # label(axiom). [assumption]. % 2.12/2.47 89 eq3(x2(A,B),eX) = eq2(c,d). [copy(88),rewrite([9(4)])]. % 2.12/2.47 113 assoc(x2(A,B)) = x2(assoc(A),assoc(B)) # label(axiom_006) # label(axiom). [assumption]. % 2.12/2.47 114 x2(assoc(A),assoc(B)) = assoc(x2(A,B)). [copy(113),flip(a)]. % 2.12/2.47 115 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_010) # label(axiom). [assumption]. % 2.12/2.47 121 lin(x2(A,B)) = append(lin(A),append(cons(mul,nil),lin(B))) # label(axiom_016) # label(axiom). [assumption]. % 2.12/2.47 122 append(lin(A),cons(mul,lin(B))) = lin(x2(A,B)). [copy(121),rewrite([115(8),5(7)]),flip(a)]. % 2.12/2.47 123 prop_unambig(A,B) = impl(eq(lin(A),lin(B)),eq3(assoc(A),assoc(B))) # label(axiom_019) # label(axiom). [assumption]. % 2.12/2.47 126 eq4(prop_unambig(A,B),bfalse) != btrue # label(goal) # label(negated_conjecture) # answer(goal). [assumption]. % 2.12/2.47 127 eq4(impl(eq(lin(A),lin(B)),eq3(assoc(A),assoc(B))),eq2(c,d)) != btrue # answer(goal). [copy(126),rewrite([123(1),9(8)])]. % 2.12/2.47 130 eq3(A,B) != bfalse | eq3(x2(A,C),x2(B,D)) = bfalse # label(axiom_056) # label(axiom). [assumption]. % 2.12/2.47 131 eq2(c,d) != eq3(A,B) | eq3(x2(A,C),x2(B,D)) = eq2(c,d). [copy(130),rewrite([9(2),9(9)]),flip(a)]. % 2.12/2.47 136 eq2(A,B) != btrue | eq(cons(A,C),cons(B,D)) = eq(C,D) # label(axiom_073) # label(axiom). [assumption]. % 2.12/2.47 142 assoc(x2(eX,A)) = x2(eX,assoc(A)). [para(1(a,1),114(a,1,1)),flip(a)]. % 2.12/2.47 146 eq3(assoc(x2(A,B)),eX) = eq2(c,d). [para(114(a,1),89(a,1,1))]. % 2.12/2.47 156 append(lin(eX),A) = cons(x,A). [para(81(a,1),115(a,1,1)),rewrite([5(6)])]. % 2.12/2.47 251 eq(cons(A,B),cons(A,C)) = eq(B,C). [hyper(136,a,77,a)]. % 2.12/2.47 260 cons(x,cons(mul,lin(A))) = lin(x2(eX,A)). [para(156(a,1),122(a,1))]. % 2.12/2.47 266 eq4(impl(eq(lin(A),lin(x2(eX,B))),eq3(assoc(A),x2(eX,assoc(B)))),eq2(c,d)) != btrue # answer(goal). [para(142(a,1),127(a,1,1,2,2))]. % 2.12/2.47 308 eq3(x2(assoc(x2(A,B)),C),x2(eX,D)) = eq2(c,d). [hyper(131,a,146,a(flip))]. % 2.12/2.47 828 cons(x,cons(mul,append(lin(A),B))) = append(lin(x2(eX,A)),B). [para(260(a,1),115(a,1,1)),rewrite([115(9)]),flip(a)]. % 2.12/2.47 841 eq(lin(x2(eX,A)),cons(x,B)) = eq(cons(mul,lin(A)),B). [para(260(a,1),251(a,1,1))]. % 2.12/2.47 4232 eq3(assoc(x2(x2(A,B),C)),x2(eX,D)) = eq2(c,d). [para(114(a,1),308(a,1,1))]. % 2.12/2.47 8109 lin(x2(x2(eX,A),B)) = lin(x2(eX,x2(A,B))). [para(122(a,1),828(a,1,2,2)),rewrite([260(6),122(11)]),flip(a)]. % 2.12/2.47 8189 eq4(impl(eq(lin(x2(eX,x2(A,B))),lin(x2(eX,C))),eq2(c,d)),eq2(c,d)) != btrue # answer(goal). [para(8109(a,1),266(a,1,1,1,1)),rewrite([4232(16)])]. % 2.12/2.47 8834 eq(lin(x2(eX,A)),lin(x2(eX,B))) = eq(lin(A),lin(B)). [para(260(a,1),841(a,1,2)),rewrite([251(14)])]. % 2.12/2.47 8840 eq4(impl(eq(lin(x2(A,B)),lin(C)),eq2(c,d)),eq2(c,d)) != btrue # answer(goal). [back_rewrite(8189),rewrite([8834(8)])]. % 2.12/2.47 8856 $F # answer(goal). [para(76(a,1),8840(a,1,1,1)),rewrite([3(5),79(7)]),xx(a)]. % 2.12/2.47 % 2.12/2.47 % SZS output end Refutation % 2.12/2.47 ============================== end of proof ========================== % 2.12/2.47 % 2.12/2.47 ============================== STATISTICS ============================ % 2.12/2.47 % 2.12/2.47 Given=1240. Generated=58963. Kept=8796. proofs=1. % 2.12/2.47 Usable=895. Sos=5685. Demods=4355. Limbo=0, Disabled=2293. Hints=0. % 2.12/2.47 Megabytes=11.87. % 2.12/2.47 User_CPU=1.45, System_CPU=0.03, Wall_clock=1. % 2.12/2.47 % 2.12/2.47 ============================== end of statistics ===================== % 2.12/2.47 % 2.12/2.47 ============================== end of search ========================= % 2.12/2.47 % 2.12/2.47 THEOREM PROVED % 2.12/2.47 % SZS status Unsatisfiable % 2.12/2.47 % 2.12/2.47 Exiting with 1 proof. % 2.12/2.47 % 2.12/2.47 Process 1614 exit (max_proofs) Tue Apr 28 23:29:48 2026 % 2.12/2.47 Prover9 interrupted %------------------------------------------------------------------------------