%------------------------------------------------------------------------------ % 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 : 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:02 PM UTC 2026 % Result : Theorem 2.03s 2.31s % Output : Refutation 2.03s % 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.12/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.34 % Computer : n004.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Apr 28 23:26:31 EDT 2026 % 0.15/0.34 % CPUTime : % 0.76/1.04 ============================== Prover9 =============================== % 0.76/1.04 Prover9 (32) version 2009-11A, November 2009. % 0.76/1.04 Process 30783 was started by sandbox on n004.cluster.edu, % 0.76/1.04 Tue Apr 28 23:26:32 2026 % 0.76/1.04 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_30630_n004.cluster.edu". % 0.76/1.04 ============================== end of head =========================== % 0.76/1.04 % 0.76/1.04 ============================== INPUT ================================= % 0.76/1.04 % 0.76/1.04 % Reading from file /tmp/Prover9_30630_n004.cluster.edu % 0.76/1.04 % 0.76/1.04 set(prolog_style_variables). % 0.76/1.04 set(auto2). % 0.76/1.04 % set(auto2) -> set(auto). % 0.76/1.04 % set(auto) -> set(auto_inference). % 0.76/1.04 % set(auto) -> set(auto_setup). % 0.76/1.04 % set(auto_setup) -> set(predicate_elim). % 0.76/1.04 % set(auto_setup) -> assign(eq_defs, unfold). % 0.76/1.04 % set(auto) -> set(auto_limits). % 0.76/1.04 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.76/1.04 % set(auto_limits) -> assign(sos_limit, 20000). % 0.76/1.04 % set(auto) -> set(auto_denials). % 0.76/1.04 % set(auto) -> set(auto_process). % 0.76/1.04 % set(auto2) -> assign(new_constants, 1). % 0.76/1.04 % set(auto2) -> assign(fold_denial_max, 3). % 0.76/1.04 % set(auto2) -> assign(max_weight, "200.000"). % 0.76/1.04 % set(auto2) -> assign(max_hours, 1). % 0.76/1.04 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.76/1.04 % set(auto2) -> assign(max_seconds, 0). % 0.76/1.04 % set(auto2) -> assign(max_minutes, 5). % 0.76/1.04 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.76/1.04 % set(auto2) -> set(sort_initial_sos). % 0.76/1.04 % set(auto2) -> assign(sos_limit, -1). % 0.76/1.04 % set(auto2) -> assign(lrs_ticks, 3000). % 0.76/1.04 % set(auto2) -> assign(max_megs, 400). % 0.76/1.04 % set(auto2) -> assign(stats, some). % 0.76/1.04 % set(auto2) -> clear(echo_input). % 0.76/1.04 % set(auto2) -> set(quiet). % 0.76/1.04 % set(auto2) -> clear(print_initial_clauses). % 0.76/1.04 % set(auto2) -> clear(print_given). % 0.76/1.04 assign(lrs_ticks,-1). % 0.76/1.04 assign(sos_limit,10000). % 0.76/1.04 assign(order,kbo). % 0.76/1.04 set(lex_order_vars). % 0.76/1.04 clear(print_given). % 0.76/1.04 % 0.76/1.04 % formulas(sos). % not echoed (41 formulas) % 0.76/1.04 % 0.76/1.04 ============================== end of input ========================== % 0.76/1.04 % 0.76/1.04 % From the command line: assign(max_seconds, 300). % 0.76/1.04 % 0.76/1.04 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.76/1.04 % 0.76/1.04 % Formulas that are not ordinary clauses: % 0.76/1.04 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 4 (all X all X2 proj1(z(X,X2)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 5 (all X all X2 proj2(z(X,X2)) = X2) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 6 (all X all X2 proj12(x2(X,X2)) = X) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 7 (all X all X2 proj22(x2(X,X2)) = X2) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 8 (all X all X2 all X3 all X4 z(X,X2) != x2(X3,X4)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 9 (all X all X2 z(X,X2) != eX) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 10 (all X all X2 z(X,X2) != eY) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 11 (all X all X2 x2(X,X2) != eX) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 12 (all X all X2 x2(X,X2) != eY) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 13 (all X (X != z(proj1(X),proj2(X)) -> (X != x2(proj12(X),proj22(X)) -> assoc(X) = X))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 14 (all Y all C (Y != z(proj1(Y),proj2(Y)) -> assoc(z(Y,C)) = z(assoc(Y),assoc(C)))) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 15 (all C all A all B assoc(z(z(A,B),C)) = assoc(z(A,z(B,C)))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 16 (all A2 all B2 assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2))) # label(axiom_032) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 17 (all Y append(nil,Y) = Y) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.04 18 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_034) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 19 (all X (X != x2(proj12(X),proj22(X)) -> linTerm(X) = lin(X))) # label(axiom_035) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 20 (all A all B linTerm(x2(A,B)) = append(cons(c,nil),append(lin(z(A,B)),cons(d,nil)))) # label(axiom_036) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 21 (all A all B lin(z(A,B)) = append(linTerm(A),append(cons(plus,nil),linTerm(B)))) # label(axiom_037) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 22 (all A3 all B2 lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2)))) # label(axiom_038) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 23 -(exists U exists V -(lin(U) = lin(V) -> assoc(U) = assoc(V))) # label(goal_041) # label(negated_conjecture) # label(non_clause). [assumption]. % 2.03/2.31 % 2.03/2.31 ============================== end of process non-clausal formulas === % 2.03/2.31 % 2.03/2.31 ============================== PROCESS INITIAL CLAUSES =============== % 2.03/2.31 % 2.03/2.31 ============================== PREDICATE ELIMINATION ================= % 2.03/2.31 % 2.03/2.31 ============================== end predicate elimination ============= % 2.03/2.31 % 2.03/2.31 Auto_denials: (non-Horn, no changes). % 2.03/2.31 % 2.03/2.31 Term ordering decisions: % 2.03/2.31 Function symbol KB weights: nil=1. c=1. d=1. eX=1. eY=1. mul=1. plus=1. x=1. y=1. z=1. cons=1. append=1. x2=1. assoc=1. lin=1. linTerm=1. proj1=1. proj12=1. proj2=1. proj22=1. head=1. tail=1. % 2.03/2.31 % 2.03/2.31 ============================== end of process initial clauses ======== % 2.03/2.31 % 2.03/2.31 ============================== CLAUSES FOR SEARCH ==================== % 2.03/2.31 % 2.03/2.31 ============================== end of clauses for search ============= % 2.03/2.31 % 2.03/2.31 ============================== SEARCH ================================ % 2.03/2.31 % 2.03/2.31 % Starting search at 0.02 seconds. % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=66.000, iters=3763 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=63.000, iters=3756 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=60.000, iters=3756 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=57.000, iters=3750 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=54.000, iters=3744 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=51.000, iters=3695 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=48.000, iters=3675 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=45.000, iters=3624 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=42.000, iters=3515 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=38.000, iters=3366 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=37.000, iters=3349 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=36.000, iters=3570 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=34.000, iters=3431 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=33.000, iters=3346 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=32.000, iters=3450 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=31.000, iters=3364 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=29.000, iters=3389 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=28.000, iters=3346 % 2.03/2.31 % 2.03/2.31 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 107 (0.00 of 0.76 sec). % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=27.000, iters=3396 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=26.000, iters=3357 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=25.000, iters=3342 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=24.000, iters=3334 % 2.03/2.31 % 2.03/2.31 Low Water (keep): wt=23.000, iters=3336 % 2.03/2.31 % 2.03/2.31 ============================== PROOF ================================= % 2.03/2.31 % SZS status Theorem % 2.03/2.31 % SZS output start Refutation % 2.03/2.31 % 2.03/2.31 % Proof 1 at 1.25 (+ 0.04) seconds. % 2.03/2.31 % Length of proof is 31. % 2.03/2.31 % Level of proof is 7. % 2.03/2.31 % Maximum clause weight is 18.000. % 2.03/2.31 % Given clauses 858. % 2.03/2.31 % 2.03/2.31 6 (all X all X2 proj12(x2(X,X2)) = X) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 9 (all X all X2 z(X,X2) != eX) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 11 (all X all X2 x2(X,X2) != eX) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 13 (all X (X != z(proj1(X),proj2(X)) -> (X != x2(proj12(X),proj22(X)) -> assoc(X) = X))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 16 (all A2 all B2 assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2))) # label(axiom_032) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 17 (all Y append(nil,Y) = Y) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 18 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_034) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 22 (all A3 all B2 lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2)))) # label(axiom_038) # label(axiom) # label(non_clause). [assumption]. % 2.03/2.31 23 -(exists U exists V -(lin(U) = lin(V) -> assoc(U) = assoc(V))) # label(goal_041) # label(negated_conjecture) # label(non_clause). [assumption]. % 2.03/2.31 24 append(nil,A) = A # label(axiom_033) # label(axiom). [clausify(17)]. % 2.03/2.31 29 proj12(x2(A,B)) = A # label(axiom_021) # label(axiom). [clausify(6)]. % 2.03/2.31 31 lin(eX) = cons(x,nil) # label(axiom_039) # label(axiom). [assumption]. % 2.03/2.31 32 cons(x,nil) = lin(eX). [copy(31),flip(a)]. % 2.03/2.31 35 assoc(x2(A,B)) = x2(assoc(A),assoc(B)) # label(axiom_032) # label(axiom). [clausify(16)]. % 2.03/2.31 36 x2(assoc(A),assoc(B)) = assoc(x2(A,B)). [copy(35),flip(a)]. % 2.03/2.31 37 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_034) # label(axiom). [clausify(18)]. % 2.03/2.31 43 lin(x2(A,B)) = append(lin(A),append(cons(mul,nil),lin(B))) # label(axiom_038) # label(axiom). [clausify(22)]. % 2.03/2.31 44 append(lin(A),cons(mul,lin(B))) = lin(x2(A,B)). [copy(43),rewrite([37(8),24(7)]),flip(a)]. % 2.03/2.31 49 z(proj1(A),proj2(A)) = A | x2(proj12(A),proj22(A)) = A | assoc(A) = A # label(axiom_029) # label(axiom). [clausify(13)]. % 2.03/2.31 78 z(A,B) != eX # label(axiom_024) # label(axiom). [clausify(9)]. % 2.03/2.31 80 x2(A,B) != eX # label(axiom_026) # label(axiom). [clausify(11)]. % 2.03/2.31 83 lin(A) != lin(B) | assoc(A) = assoc(B) # label(goal_041) # label(negated_conjecture). [clausify(23)]. % 2.03/2.31 88 proj12(assoc(x2(A,B))) = assoc(A). [para(36(a,1),29(a,1,1))]. % 2.03/2.31 90 append(lin(eX),A) = cons(x,A). [para(32(a,1),37(a,1,1)),rewrite([24(6)])]. % 2.03/2.31 125 assoc(eX) = eX. [resolve(80,a,49,b),unit_del(a,78)]. % 2.03/2.31 150 assoc(x2(eX,A)) = x2(eX,assoc(A)). [para(125(a,1),36(a,1,1)),flip(a)]. % 2.03/2.31 199 cons(x,cons(mul,lin(A))) = lin(x2(eX,A)). [para(90(a,1),44(a,1))]. % 2.03/2.31 673 cons(x,cons(mul,append(lin(A),B))) = append(lin(x2(eX,A)),B). [para(199(a,1),37(a,1,1)),rewrite([37(9)]),flip(a)]. % 2.03/2.31 7222 lin(x2(x2(eX,A),B)) = lin(x2(eX,x2(A,B))). [para(44(a,1),673(a,1,2,2)),rewrite([199(6),44(11)]),flip(a)]. % 2.03/2.31 7256 assoc(x2(x2(eX,A),B)) = x2(eX,assoc(x2(A,B))). [resolve(7222,a,83,a),rewrite([150(8)])]. % 2.03/2.31 7438 $F. [para(7256(a,1),88(a,1,1)),rewrite([29(5),150(4)]),flip(a),unit_del(a,80)]. % 2.03/2.31 % 2.03/2.31 % SZS output end Refutation % 2.03/2.31 ============================== end of proof ========================== % 2.03/2.31 % 2.03/2.31 ============================== STATISTICS ============================ % 2.03/2.31 % 2.03/2.31 Given=858. Generated=54497. Kept=7395. proofs=1. % 2.03/2.31 Usable=828. Sos=6163. Demods=1612. Limbo=3, Disabled=442. Hints=0. % 2.03/2.31 Megabytes=9.67. % 2.03/2.31 User_CPU=1.25, System_CPU=0.04, Wall_clock=1. % 2.03/2.31 % 2.03/2.31 ============================== end of statistics ===================== % 2.03/2.31 % 2.03/2.31 ============================== end of search ========================= % 2.03/2.31 % 2.03/2.31 THEOREM PROVED % 2.03/2.31 % SZS status Theorem % 2.03/2.31 % 2.03/2.31 Exiting with 1 proof. % 2.03/2.31 % 2.03/2.31 Process 30783 exit (max_proofs) Tue Apr 28 23:26:33 2026 % 2.03/2.31 Prover9 interrupted %------------------------------------------------------------------------------