%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX218+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n008.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:07 PM UTC 2026 % Result : Unknown 169.43s 169.70s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX218+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.34 % Computer : n008.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Wed Apr 29 01:49:28 EDT 2026 % 0.17/0.34 % CPUTime : % 0.76/1.07 ============================== Prover9 =============================== % 0.76/1.07 Prover9 (32) version 2009-11A, November 2009. % 0.76/1.07 Process 10884 was started by sandbox on n008.cluster.edu, % 0.76/1.07 Wed Apr 29 01:49:28 2026 % 0.76/1.07 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_10729_n008.cluster.edu". % 0.76/1.07 ============================== end of head =========================== % 0.76/1.07 % 0.76/1.07 ============================== INPUT ================================= % 0.76/1.07 % 0.76/1.07 % Reading from file /tmp/Prover9_10729_n008.cluster.edu % 0.76/1.07 % 0.76/1.07 set(prolog_style_variables). % 0.76/1.07 set(auto2). % 0.76/1.07 % set(auto2) -> set(auto). % 0.76/1.07 % set(auto) -> set(auto_inference). % 0.76/1.07 % set(auto) -> set(auto_setup). % 0.76/1.07 % set(auto_setup) -> set(predicate_elim). % 0.76/1.07 % set(auto_setup) -> assign(eq_defs, unfold). % 0.76/1.07 % set(auto) -> set(auto_limits). % 0.76/1.07 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.76/1.07 % set(auto_limits) -> assign(sos_limit, 20000). % 0.76/1.07 % set(auto) -> set(auto_denials). % 0.76/1.07 % set(auto) -> set(auto_process). % 0.76/1.07 % set(auto2) -> assign(new_constants, 1). % 0.76/1.07 % set(auto2) -> assign(fold_denial_max, 3). % 0.76/1.07 % set(auto2) -> assign(max_weight, "200.000"). % 0.76/1.07 % set(auto2) -> assign(max_hours, 1). % 0.76/1.07 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.76/1.07 % set(auto2) -> assign(max_seconds, 0). % 0.76/1.07 % set(auto2) -> assign(max_minutes, 5). % 0.76/1.07 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.76/1.07 % set(auto2) -> set(sort_initial_sos). % 0.76/1.07 % set(auto2) -> assign(sos_limit, -1). % 0.76/1.07 % set(auto2) -> assign(lrs_ticks, 3000). % 0.76/1.07 % set(auto2) -> assign(max_megs, 400). % 0.76/1.07 % set(auto2) -> assign(stats, some). % 0.76/1.07 % set(auto2) -> clear(echo_input). % 0.76/1.07 % set(auto2) -> set(quiet). % 0.76/1.07 % set(auto2) -> clear(print_initial_clauses). % 0.76/1.07 % set(auto2) -> clear(print_given). % 0.76/1.07 assign(lrs_ticks,-1). % 0.76/1.07 assign(sos_limit,10000). % 0.76/1.07 assign(order,kbo). % 0.76/1.07 set(lex_order_vars). % 0.76/1.07 clear(print_given). % 0.76/1.07 % 0.76/1.07 % formulas(sos). % not echoed (65 formulas) % 0.76/1.07 % 0.76/1.07 ============================== end of input ========================== % 0.76/1.07 % 0.76/1.07 % From the command line: assign(max_seconds, 300). % 0.76/1.07 % 0.76/1.07 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.76/1.07 % 0.76/1.07 % Formulas that are not ordinary clauses: % 0.76/1.07 1 (all X all X2 all X3 proj1tuple(tuple2(X,X2,X3)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 2 (all X all X2 all X3 proj2tuple(tuple2(X,X2,X3)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 3 (all X all X2 all X3 proj3tuple(tuple2(X,X2,X3)) = X3) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 4 (all X all X2 proj1pair(pair22(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 5 (all X all X2 proj2pair(pair22(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 6 (all X all X2 proj1pair2(pair23(X,X2)) = X) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 7 (all X all X2 proj2pair2(pair23(X,X2)) = X2) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 8 (all X all X2 proj1pair3(pair24(X,X2)) = X) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 9 (all X all X2 proj2pair3(pair24(X,X2)) = X2) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 10 (all X all X2 proj1pair4(pair25(X,X2)) = X) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 11 (all X all X2 proj2pair4(pair25(X,X2)) = X2) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 12 (all X all X2 head(cons(X,X2)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 13 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 14 (all X all X2 nil != cons(X,X2)) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 15 (all X all X2 head2(cons2(X,X2)) = X) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 16 (all X all X2 tail2(cons2(X,X2)) = X2) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 17 (all X all X2 nil2 != cons2(X,X2)) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 18 (all X proj1Succ(succ(X)) = X) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 19 (all X zero != succ(X)) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 20 (all X proj1Left(left(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 21 (all X proj1Right(right(X)) = X) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 22 (all X all X2 left(X) != right(X2)) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 23 (all X proj1Lft(lft(X)) = X) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 24 (all X proj1Rgt(rgt(X)) = X) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 25 (all X all X2 lft(X) != rgt(X2)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 26 (all X lft(X) != stp) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 27 (all X rgt(X) != stp) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 28 (all Y all Xs split(cons2(Y,Xs)) = pair24(Y,Xs)) # label(axiom_032) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 29 (all Y rev(nil2,Y) = Y) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 30 (all Y all Z all Xs (Z != o -> rev(cons2(Z,Xs),Y) = rev(Xs,cons2(Z,Y)))) # label(axiom_034) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 31 (all Y all Xs rev(cons2(o,Xs),Y) = Y) # label(axiom_035) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 32 (all Y apply(nil,Y) = pair25(o,stp)) # label(axiom_038) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 33 (all Y all Q all Sa all Rhs (Sa = Y -> apply(cons(pair22(Sa,Rhs),Q),Y) = Rhs)) # label(axiom_039) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 34 (all Y all Q all Sa all Rhs (Sa != Y -> apply(cons(pair22(Sa,Rhs),Q),Y) = apply(Q,Y))) # label(axiom_040) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 35 (all Y all Z all X2 all S all Y1 all Lft1 (split(Y) = pair24(Y1,Lft1) -> act(lft(S),Y,Z,X2) = right(tuple2(S,Lft1,cons2(Y1,cons2(Z,X2)))))) # label(axiom_041) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 36 (all Y all Z all X2 all T act(rgt(T),Y,Z,X2) = right(tuple2(T,cons2(Z,Y),X2))) # label(axiom_042) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 37 (all Y all Z all X2 act(stp,Y,Z,X2) = left(rev(Y,cons2(Z,X2)))) # label(axiom_043) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 38 (all X all S all Lft all Rgt all X1 all Rgt2 all X12 all What1 (split(Rgt) = pair24(X1,Rgt2) -> (apply(X,pair23(S,X1)) = pair25(X12,What1) -> step(X,tuple2(S,Lft,Rgt)) = act(What1,Lft,X12,Rgt2)))) # label(axiom_044) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 39 (all X all Y all Tape (step(X,Y) = left(Tape) -> steps(X,Y) = Tape)) # label(axiom_045) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 40 (all X all Y all St (step(X,Y) = right(St) -> steps(X,Y) = steps(X,St))) # label(axiom_046) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 41 (all X all Y runt(X,Y) = steps(X,tuple2(zero,nil2,Y))) # label(axiom_047) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 42 (all X (runt(X,cons2(a2,nil2)) = nil2 -> -prog0(X))) # label(axiom_048) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 43 (all X all Y all Z (runt(X,cons2(a2,nil2)) = cons2(Y,Z) -> (Y != a2 -> -prog0(X)))) # label(axiom_049) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 44 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = nil2 -> -prog0(X)))) # label(axiom_050) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 45 (all X all X2 all X3 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(X2,X3) -> (X2 != a2 -> -prog0(X))))) # label(axiom_051) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.07 46 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,nil2) -> -prog0(X)))) # label(axiom_052) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 47 (all X all X4 all X5 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(X4,X5)) -> (X4 != a2 -> -prog0(X))))) # label(axiom_053) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 48 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,nil2)) -> -prog0(X)))) # label(axiom_054) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 49 (all X all X6 all X7 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(X6,X7))) -> (X6 != a2 -> -prog0(X))))) # label(axiom_055) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 50 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,nil2))) -> -prog0(X)))) # label(axiom_056) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 51 (all X all X8 all X9 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(X8,X9)))) -> (X8 != a2 -> -prog0(X))))) # label(axiom_057) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 52 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2)))) -> -prog0(X)))) # label(axiom_058) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 53 (all X all X10 all X11 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(X10,X11))))) -> (X10 != b -> -prog0(X))))) # label(axiom_059) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 54 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))) -> -prog0(X)))) # label(axiom_060) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 55 (all X all X12 all X13 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(X12,X13)))))) -> (X12 != b -> -prog0(X))))) # label(axiom_061) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 56 (all X (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2)))))) -> prog0(X)))) # label(axiom_062) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 57 (all X all X14 all X15 (runt(X,cons2(a2,nil2)) = cons2(a2,nil2) -> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))) = cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(X14,X15))))))) -> -prog0(X)))) # label(axiom_063) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 58 (all X all X16 all X17 (runt(X,cons2(a2,nil2)) = cons2(a2,cons2(X16,X17)) -> -prog0(X))) # label(axiom_064) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.09 59 -(exists X exists Y exists Z exists V exists W prog0(cons(pair22(pair23(zero,a2),X),cons(pair22(pair23(zero,b),Y),cons(pair22(pair23(one,a2),Z),cons(pair22(pair23(one,b),V),cons(pair22(pair23(two,a2),W),nil))))))) # label(goal_065) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.76/1.09 % 0.76/1.09 ============================== end of process non-clausal formulas === % 0.76/1.09 % 0.76/1.09 ============================== PROCESS INITIAL CLAUSES =============== % 0.76/1.09 % 0.76/1.09 ============================== PREDICATE ELIMINATION ================= % 0.76/1.09 % 0.76/1.09 ============================== end predicate elimination ============= % 0.76/1.09 % 0.76/1.09 Auto_denials: (non-Horn, no changes). % 0.76/1.09 % 0.76/1.09 Term ordering decisions: % 0.76/1.09 Function symbol KB weights: a2=1. nil2=1. b=1. o=1. one=1. stp=1. zero=1. nil=1. two=1. cons2=1. runt=1. pair24=1. apply=1. rev=1. cons=1. pair22=1. pair25=1. steps=1. pair23=1. step=1. right=1. split=1. left=1. succ=1. lft=1. rgt=1. head=1. head2=1. proj1Left=1. proj1Lft=1. proj1Rgt=1. proj1Right=1. proj1Succ=1. proj1pair=1. proj1pair2=1. proj1pair3=1. proj1pair4=1. proj1tuple=1. proj2pair=1. proj2pair2=1. proj2pair3=1. proj2pair4=1. proj2tuple=1. proj3tuple=1. tail=1. tail2=1. tuple2=1. act=1. % 169.43/169.70 % 169.43/169.70 ============================== end of process initial clauses ======== % 169.43/169.70 % 169.43/169.70 ============================== CLAUSES FOR SEARCH ==================== % 169.43/169.70 % 169.43/169.70 ============================== end of clauses for search ============= % 169.43/169.70 % 169.43/169.70 ============================== SEARCH ================================ % 169.43/169.70 % 169.43/169.70 % Starting search at 0.04 seconds. % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=58.000, iters=3975 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=49.000, iters=3586 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=48.000, iters=3480 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=47.000, iters=3343 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=46.000, iters=3334 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=45.000, iters=3333 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=44.000, iters=3333 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=40.000, iters=3670 % 169.43/169.70 % 169.43/169.70 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 33 (0.00 of 72.62 sec). % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=3944, wt=66.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=4338, wt=63.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=3934, wt=62.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=3922, wt=60.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=4376, wt=59.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=4363, wt=58.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=5708, wt=57.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=11011, wt=40.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=11014, wt=39.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=11026, wt=38.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=11042, wt=35.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=11126, wt=31.000 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=39.000, iters=3579 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=35.000, iters=3361 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=13241, wt=29.000 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=34.000, iters=3336 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=14365, wt=28.000 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=33.000, iters=3342 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=14389, wt=26.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=14395, wt=25.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=15049, wt=24.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=15070, wt=23.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=15549, wt=22.000 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=32.000, iters=3357 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=29337, wt=21.000 % 169.43/169.70 % 169.43/169.70 Low Water (displace): id=88126, wt=20.000 % 169.43/169.70 % 169.43/169.70 Low Water (keep): wt=31.000, iters=3334 % 169.43/169.70 % 169.43/169.70 ============================== STATISTICS ============================ % 169.43/169.70 % 169.43/169.70 Given=2004. Generated=4314755. Kept=468850. proofs=0. % 169.43/169.70 Usable=1974. Sos=9999. Demods=72. Limbo=534, Disabled=456408. Hints=0. % 169.43/169.70 Kept_by_rule=0, Deleted_by_rule=0. % 169.43/169.70 Forward_subsumed=3417310. Back_subsumed=302. % 169.43/169.70 Sos_limit_deleted=428594. Sos_displaced=456023. Sos_removed=0. % 169.43/169.70 New_demodulators=82 (1 lex), Back_demodulated=18. Back_unit_deleted=0. % 169.43/169.70 Demod_attempts=99523441. Demod_rewrites=31085. % 169.43/169.70 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 169.43/169.70 Nonunit_fsub_feature_tests=8805335. Nonunit_bsub_feature_tests=1095260. % 169.43/169.70 Megabytes=419.43. % 169.43/169.70 User_CPU=166.05, System_CPU=2.61, Wall_clock=169. % 169.43/169.70 % 169.43/169.70 Megs malloced by palloc(): 400. % 169.43/169.70 type (bytes each) gets frees in use bytes % 169.43/169.70 chunk ( 104) 1959 1959 0 0.0 K % 169.43/169.70 string_buf ( 8) 1830 1830 0 0.0 K % 169.43/169.70 token ( 20) 4615 4615 0 0.0 K % 169.43/169.70 pterm ( 16) 2675 2675 0 0.0 K % 169.43/169.70 hashtab ( 8) 59 59 0 0.0 K % 169.43/169.70 hashnode ( 8) 166 166 0 0.0 K % 169.43/169.70 term ( 20) 278008883 267124755 10884128 212580.6 K % 169.43/169.70 term arg arrays: 62315.9 K % 169.43/169.70 attribute ( 12) 383 0 383 4.5 K % 169.43/169.70 ilist ( 8) 534975331 531759024 3216307 25127.4 K % 169.43/169.70 plist ( 8) 17660429 17178055 482374 3768.5 K % 169.43/169.70 i2list ( 12) 86117371 86117371 0 0.0 K % 169.43/169.70 just ( 12) 4761720 4282484 479236 5616.0 K % 169.43/169.70 parajust ( 16) 814800 803149 11651 182.0 K % 169.43/169.70 instancejust ( 8) 0 0 0 0.0 K % 169.43/169.70 ivyjust ( 24) 0 0 0 0.0 K % 169.43/169.70 formula ( 28) 1482 844 638 17.4 K % 169.43/169.70 formula arg arrays: 2.0 K % 169.43/169.70 topform ( 52) 4314879 3845904 468975 23815.1 K % 169.43/169.70 clist_pos ( 20) 1395725 926738 468987 9159.9 K % 169.43/169.70 clist ( 16) 8 1 7 0.1 K % 169.43/169.70 context ( 808) 28631213 28631210 3 2.4 K % 169.43/169.70 trail ( 12) 639081441 639081437 4 0.0 K % 169.43/169.70 ac_match_pos (70044) 0 0 0 0.0 K % 169.43/169.70 ac_match_free_vars_pos (20020) % 169.43/169.70 0 0 0 0.0 K % 169.43/169.70 btm_state ( 60) 0 0 0 0.0 K % 169.43/169.70 btu_state ( 60) 0 0 0 0.0 K % 169.43/169.70 ac_position (285432) 0 0 0 0.0 K % 169.43/169.70 fpa_trie ( 20) 2977750 2889802 87948 1717.7 K % 169.43/169.70 fpa_state ( 28) 6889172 6888915 257 7.0 K % 169.43/169.70 fpa_index ( 12) 10 0 10 0.1 K % 169.43/169.70 fpa_chunk ( 20) 6541852 6488250 53602 1046.9 K % 169.43/169.70 fpa_list ( 16) 2913269 0 2913269 45519.8 K % 169.43/169.70 fpa_list chunks: 4828.5 K % 169.43/169.70 discrim ( 12) 2714664 2701246 13418 157.2 K % 169.43/169.70 discrim_pos ( 16) 3033437 3033437 0 0.0 K % 169.43/169.70 flat2 ( 32) 196776269 196776269 0 0.0 K % 169.43/169.70 flat ( 48) 0 0 0 0.0 K % 169.43/169.70 flatterm ( 32) 148170388 148170388 0 0.0 K % 169.43/169.70 mindex ( 28) 13 0 13 0.4 K % 169.43/169.70 mindex_pos ( 56) 19371690 19371688 2 0.1 K % 169.43/169.70 lindex ( 12) 5 0 5 0.1 K % 169.43/169.70 clash ( 40) 24255 24252 3 0.1 K % 169.43/169.70 di_tree ( 12) 1373814 797000 576814 6759.5 K % 169.43/169.70 avl_node ( 20) 936564 916566 19998 390.6 K % 169.43/169.70 % 169.43/169.70 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 169.43/169.70 List 1, length 16, 0.1 K % 169.43/169.70 List 2, length 189, 1.5 K % 169.43/169.70 List 3, length 3178, 37.2 K % 169.43/169.70 List 4, length 4, 0.1 K % 169.43/169.70 List 8, length 250, 7.8 K % 169.43/169.70 List 9, length 6, 0.2 K % 169.43/169.70 List 10, length 2, 0.1 K % 169.43/169.70 List 14, length 1, 0.1 K % 169.43/169.70 List 16, length 257, 16.1 K % 169.43/169.70 List 26, length 64, 6.5 K % 169.43/169.70 List 32, length 201, 25.1 K % 169.43/169.70 List 64, length 280, 70.0 K % 169.43/169.70 List 128, length 75, 37.5 K % 169.43/169.70 List 202, length 2, 1.6 K % 169.43/169.70 List 256, length 398, 398.0 K % 169.43/169.70 % 169.43/169.70 ============================== SELECTOR REPORT ======================= % 169.43/169.70 Sos_deleted=428594, Sos_displaced=456023, Sos_size=9999 % 169.43/169.70 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 169.43/169.70 I 2147483647 high age 0 65 % 169.43/169.70 H 1 high weight 0 0 % 169.43/169.70 A 1 low age 9999 259 % 169.43/169.70 F 4 low weight 290 648 % 169.43/169.70 T 4 low weight 9709 1032 % 169.43/169.70 ============================== end of selector report ================ % 169.43/169.70 % 169.43/169.70 ============================== end of statistics ===================== % 169.43/169.70 % 169.43/169.70 Exiting with failure. % 169.43/169.70 % 169.43/169.70 Process 10884 exit (max_megs) Wed Apr 29 01:52:17 2026 % 169.43/169.70 Prover9 interrupted %------------------------------------------------------------------------------