%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX191+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n024.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:03 PM UTC 2026 % Result : Unknown 71.10s 71.48s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWX191+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : tptp2X_and_run_prover9 %d %s % 0.07/0.25 % Computer : n024.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Tue Apr 28 18:51:56 EDT 2026 % 0.07/0.25 % CPUTime : % 0.40/0.73 ============================== Prover9 =============================== % 0.40/0.73 Prover9 (32) version 2009-11A, November 2009. % 0.40/0.73 Process 5533 was started by sandbox on n024.cluster.edu, % 0.40/0.73 Tue Apr 28 18:51:57 2026 % 0.40/0.73 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_5379_n024.cluster.edu". % 0.40/0.73 ============================== end of head =========================== % 0.40/0.73 % 0.40/0.73 ============================== INPUT ================================= % 0.40/0.73 % 0.40/0.73 % Reading from file /tmp/Prover9_5379_n024.cluster.edu % 0.40/0.73 % 0.40/0.73 set(prolog_style_variables). % 0.40/0.73 set(auto2). % 0.40/0.73 % set(auto2) -> set(auto). % 0.40/0.73 % set(auto) -> set(auto_inference). % 0.40/0.73 % set(auto) -> set(auto_setup). % 0.40/0.73 % set(auto_setup) -> set(predicate_elim). % 0.40/0.73 % set(auto_setup) -> assign(eq_defs, unfold). % 0.40/0.73 % set(auto) -> set(auto_limits). % 0.40/0.73 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.40/0.73 % set(auto_limits) -> assign(sos_limit, 20000). % 0.40/0.73 % set(auto) -> set(auto_denials). % 0.40/0.73 % set(auto) -> set(auto_process). % 0.40/0.73 % set(auto2) -> assign(new_constants, 1). % 0.40/0.73 % set(auto2) -> assign(fold_denial_max, 3). % 0.40/0.73 % set(auto2) -> assign(max_weight, "200.000"). % 0.40/0.73 % set(auto2) -> assign(max_hours, 1). % 0.40/0.73 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.40/0.73 % set(auto2) -> assign(max_seconds, 0). % 0.40/0.73 % set(auto2) -> assign(max_minutes, 5). % 0.40/0.73 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.40/0.73 % set(auto2) -> set(sort_initial_sos). % 0.40/0.73 % set(auto2) -> assign(sos_limit, -1). % 0.40/0.73 % set(auto2) -> assign(lrs_ticks, 3000). % 0.40/0.73 % set(auto2) -> assign(max_megs, 400). % 0.40/0.73 % set(auto2) -> assign(stats, some). % 0.40/0.73 % set(auto2) -> clear(echo_input). % 0.40/0.73 % set(auto2) -> set(quiet). % 0.40/0.73 % set(auto2) -> clear(print_initial_clauses). % 0.40/0.73 % set(auto2) -> clear(print_given). % 0.40/0.73 assign(lrs_ticks,-1). % 0.40/0.73 assign(sos_limit,10000). % 0.40/0.73 assign(order,kbo). % 0.40/0.73 set(lex_order_vars). % 0.40/0.73 clear(print_given). % 0.40/0.73 % 0.40/0.73 % formulas(sos). % not echoed (54 formulas) % 0.40/0.73 % 0.40/0.73 ============================== end of input ========================== % 0.40/0.73 % 0.40/0.73 % From the command line: assign(max_seconds, 300). % 0.40/0.73 % 0.40/0.73 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.40/0.73 % 0.40/0.73 % Formulas that are not ordinary clauses: % 0.40/0.73 1 (all X proj1S(s(X)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 2 (all X s(X) != z) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 3 (all X proj1N(n(X)) = X) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 4 (all X all X2 proj1(x(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 5 (all X all X2 proj2(x(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 6 (all X all X2 proj12(y(X,X2)) = X) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 7 (all X all X2 proj22(y(X,X2)) = X2) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 8 (all X all X2 all X3 n(X) != x(X2,X3)) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 9 (all X all X2 all X3 n(X) != y(X2,X3)) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 10 (all X n(X) != x2) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 11 (all X all X2 all X3 all X4 x(X,X2) != y(X3,X4)) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 12 (all X all X2 x(X,X2) != x2) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 13 (all X all X2 y(X,X2) != x2) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 14 (all Y all E (Y = E -> fail2(Y,E) = y(n(s(s(z))),opt(Y)))) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 15 (all Y all E (Y != E -> (Y != x(proj1(Y),proj2(Y)) -> fail2(Y,E) = x(opt(Y),opt(E))))) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 16 (all E all A all B (x(A,B) != E -> fail2(x(A,B),E) = opt(x(A,x(B,E))))) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 17 (all Y all E (Y != n(proj1N(Y)) -> fail1(Y,E) = fail2(Y,E))) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 18 (all E all C (E != n(proj1N(E)) -> fail1(n(C),E) = fail2(n(C),E))) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 19 (all C all B2 fail1(n(C),n(B2)) = n(addNat(C,B2))) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 20 (all Y all E (E != n(proj1N(E)) -> fail(Y,E) = fail1(Y,E))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 21 (all Y all X2 fail(Y,n(s(X2))) = fail1(Y,n(s(X2)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 22 (all Y fail(Y,n(z)) = Y) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 23 (all X5 all E2 fail4(X5,E2) = y(opt(X5),opt(E2))) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 24 (all X5 all E2 (X5 != n(proj1N(X5)) -> (X5 != y(proj12(X5),proj22(X5)) -> fail32(X5,E2) = fail4(X5,E2)))) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 25 (all E2 all A2 (E2 != n(proj1N(E2)) -> fail32(n(A2),E2) = fail4(n(A2),E2))) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 26 (all A2 all B3 fail32(n(A2),n(B3)) = n(mulNat(A2,B3))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 27 (all E2 all A3 all B4 fail32(y(A3,B4),E2) = opt(y(A3,y(B4,E2)))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 28 (all X5 all E2 (E2 != n(proj1N(E2)) -> fail22(X5,E2) = fail32(X5,E2))) # label(axiom_028) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 29 (all X5 all X8 fail22(X5,n(s(s(X8)))) = fail32(X5,n(s(s(X8))))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 30 (all X5 fail22(X5,n(s(z))) = X5) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 31 (all X5 fail22(X5,n(z)) = fail32(X5,n(z))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 32 (all X5 all E2 (X5 != n(proj1N(X5)) -> fail12(X5,E2) = fail22(X5,E2))) # label(axiom_032) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 33 (all E2 all X11 fail12(n(s(s(X11))),E2) = fail22(n(s(s(X11))),E2)) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 34 (all E2 fail12(n(s(z)),E2) = E2) # label(axiom_034) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 35 (all E2 fail12(n(z),E2) = fail22(n(z),E2)) # label(axiom_035) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 36 (all X5 all E2 (E2 != n(proj1N(E2)) -> fail3(X5,E2) = fail12(X5,E2))) # label(axiom_036) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 37 (all X5 all X13 fail3(X5,n(s(X13))) = fail12(X5,n(s(X13)))) # label(axiom_037) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 38 (all X5 fail3(X5,n(z)) = n(z)) # label(axiom_038) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 39 (all Y d(n(Y)) = n(z)) # label(axiom_039) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 40 (all F all G d(x(F,G)) = x(d(F),d(G))) # label(axiom_040) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 41 (all H all G2 d(y(H,G2)) = x(y(d(H),G2),y(H,d(G2)))) # label(axiom_041) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 42 (all Y all Z addNat(s(Z),Y) = s(addNat(Z,Y))) # label(axiom_043) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 43 (all Y addNat(z,Y) = Y) # label(axiom_044) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 44 (all Y all Z mulNat(s(Z),Y) = addNat(Y,mulNat(Z,Y))) # label(axiom_045) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 45 (all Y mulNat(z,Y) = z) # label(axiom_046) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 46 (all X (X != x(proj1(X),proj2(X)) -> (X != y(proj12(X),proj22(X)) -> opt(X) = X))) # label(axiom_047) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 47 (all Y all E (Y != n(proj1N(Y)) -> opt(x(Y,E)) = fail(Y,E))) # label(axiom_048) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 48 (all E all X4 opt(x(n(s(X4)),E)) = fail(n(s(X4)),E)) # label(axiom_049) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 49 (all E opt(x(n(z),E)) = E) # label(axiom_050) # label(axiom) # label(non_clause). [assumption]. % 0.40/0.73 50 (all X5 all E2 (X5 != n(proj1N(X5)) -> opt(y(X5,E2)) = fail3(X5,E2))) # label(axiom_051) # label(axiom) # label(non_clause). [assumption]. % 71.10/71.47 51 (all E2 all X15 opt(y(n(s(X15)),E2)) = fail3(n(s(X15)),E2)) # label(axiom_052) # label(axiom) # label(non_clause). [assumption]. % 71.10/71.47 52 (all E2 opt(y(n(z),E2)) = n(z)) # label(axiom_053) # label(axiom) # label(non_clause). [assumption]. % 71.10/71.47 53 -(exists E opt(d(E)) = x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))) # label(goal_054) # label(negated_conjecture) # label(non_clause). [assumption]. % 71.10/71.47 % 71.10/71.47 ============================== end of process non-clausal formulas === % 71.10/71.47 % 71.10/71.47 ============================== PROCESS INITIAL CLAUSES =============== % 71.10/71.47 % 71.10/71.47 ============================== PREDICATE ELIMINATION ================= % 71.10/71.47 % 71.10/71.47 ============================== end predicate elimination ============= % 71.10/71.47 % 71.10/71.47 Auto_denials: (non-Horn, no changes). % 71.10/71.47 % 71.10/71.47 Term ordering decisions: % 71.10/71.47 Function symbol KB weights: z=1. x2=1. x=1. y=1. fail22=1. fail32=1. fail12=1. addNat=1. fail=1. fail1=1. fail2=1. fail3=1. mulNat=1. fail4=1. n=1. s=1. opt=1. proj1N=1. d=1. proj1=1. proj12=1. proj2=1. proj22=1. proj1S=1. % 71.10/71.47 % 71.10/71.47 ============================== end of process initial clauses ======== % 71.10/71.47 % 71.10/71.47 ============================== CLAUSES FOR SEARCH ==================== % 71.10/71.47 % 71.10/71.47 ============================== end of clauses for search ============= % 71.10/71.47 % 71.10/71.47 ============================== SEARCH ================================ % 71.10/71.47 % 71.10/71.47 % Starting search at 0.01 seconds. % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=59.000, iters=3523 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=56.000, iters=3511 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=31.000, iters=3493 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=29.000, iters=3525 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=27.000, iters=3421 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=25.000, iters=3355 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=24.000, iters=3344 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=23.000, iters=3463 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=22.000, iters=3424 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=21.000, iters=3341 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=20.000, iters=3433 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=19.000, iters=3357 % 71.10/71.47 % 71.10/71.47 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 214 (0.00 of 0.65 sec). % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=18.000, iters=3390 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=17.000, iters=3385 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=13.000, iters=3358 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=12.000, iters=3337 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=3343, wt=59.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=3790, wt=57.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=3083, wt=52.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=3478, wt=51.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=3789, wt=48.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=3477, wt=43.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=1750, wt=42.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=10929, wt=23.000 % 71.10/71.47 % 71.10/71.47 Low Water (displace): id=12797, wt=10.000 % 71.10/71.47 % 71.10/71.47 Low Water (keep): wt=11.000, iters=3333 % 71.10/71.47 % 71.10/71.47 ============================== STATISTICS ============================ % 71.10/71.47 % 71.10/71.47 Given=7261. Generated=2036619. Kept=722682. proofs=0. % 71.10/71.47 Usable=6754. Sos=9999. Demods=4186. Limbo=144, Disabled=705839. Hints=0. % 71.10/71.47 Kept_by_rule=0, Deleted_by_rule=0. % 71.10/71.47 Forward_subsumed=396150. Back_subsumed=35. % 71.10/71.47 Sos_limit_deleted=917787. Sos_displaced=702520. Sos_removed=0. % 71.10/71.47 New_demodulators=7635 (8 lex), Back_demodulated=3215. Back_unit_deleted=15. % 71.10/71.47 Demod_attempts=37261128. Demod_rewrites=1223598. % 71.10/71.47 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 71.10/71.47 Nonunit_fsub_feature_tests=96980. Nonunit_bsub_feature_tests=38090. % 71.10/71.47 Megabytes=419.43. % 71.10/71.47 User_CPU=69.26, System_CPU=1.50, Wall_clock=70. % 71.10/71.47 % 71.10/71.47 Megs malloced by palloc(): 400. % 71.10/71.47 type (bytes each) gets frees in use bytes % 71.10/71.47 chunk ( 104) 1306 1306 0 0.0 K % 71.10/71.47 string_buf ( 8) 1232 1232 0 0.0 K % 71.10/71.47 token ( 20) 3027 3027 0 0.0 K % 71.10/71.47 pterm ( 16) 1681 1681 0 0.0 K % 71.10/71.47 hashtab ( 8) 53 53 0 0.0 K % 71.10/71.47 hashnode ( 8) 79 79 0 0.0 K % 71.10/71.47 term ( 20) 56622045 47957840 8664205 169222.8 K % 71.10/71.47 term arg arrays: 37687.4 K % 71.10/71.47 attribute ( 12) 329 0 329 3.9 K % 71.10/71.47 ilist ( 8) 431394347 428201597 3192750 24943.4 K % 71.10/71.47 plist ( 8) 11754797 11008329 746468 5831.8 K % 71.10/71.47 i2list ( 12) 13059024 13059024 0 0.0 K % 71.10/71.47 just ( 12) 2733916 1944362 789554 9252.6 K % 71.10/71.48 parajust ( 16) 1271441 1206462 64979 1015.3 K % 71.10/71.48 instancejust ( 8) 0 0 0 0.0 K % 71.10/71.48 ivyjust ( 24) 0 0 0 0.0 K % 71.10/71.48 formula ( 28) 808 396 412 11.3 K % 71.10/71.48 formula arg arrays: 1.2 K % 71.10/71.48 topform ( 52) 2036727 1313937 722790 36704.2 K % 71.10/71.48 clist_pos ( 20) 2166009 1439087 726922 14197.7 K % 71.10/71.48 clist ( 16) 8 1 7 0.1 K % 71.10/71.48 context ( 808) 16763417 16763415 2 1.6 K % 71.10/71.48 trail ( 12) 16276536 16276535 1 0.0 K % 71.10/71.48 ac_match_pos (70044) 0 0 0 0.0 K % 71.10/71.48 ac_match_free_vars_pos (20020) % 71.10/71.48 0 0 0 0.0 K % 71.10/71.48 btm_state ( 60) 0 0 0 0.0 K % 71.10/71.48 btu_state ( 60) 0 0 0 0.0 K % 71.10/71.48 ac_position (285432) 0 0 0 0.0 K % 71.10/71.48 fpa_trie ( 20) 5899191 5239867 659324 12877.4 K % 71.10/71.48 fpa_state ( 28) 26070713 26070710 3 0.1 K % 71.10/71.48 fpa_index ( 12) 10 0 10 0.1 K % 71.10/71.48 fpa_chunk ( 20) 6433564 6390811 42753 835.0 K % 71.10/71.48 fpa_list ( 16) 5266373 0 5266373 82287.1 K % 71.10/71.48 fpa_list chunks: 2031.6 K % 71.10/71.48 discrim ( 12) 3575960 3520784 55176 646.6 K % 71.10/71.48 discrim_pos ( 16) 1456204 1456204 0 0.0 K % 71.10/71.48 flat2 ( 32) 41602644 41602644 0 0.0 K % 71.10/71.48 flat ( 48) 0 0 0 0.0 K % 71.10/71.48 flatterm ( 32) 52273851 52273851 0 0.0 K % 71.10/71.48 mindex ( 28) 13 0 13 0.4 K % 71.10/71.48 mindex_pos ( 56) 11184391 11184390 1 0.1 K % 71.10/71.48 lindex ( 12) 5 0 5 0.1 K % 71.10/71.48 clash ( 40) 1026346 1026344 2 0.1 K % 71.10/71.48 di_tree ( 12) 233639 54188 179451 2102.9 K % 71.10/71.48 avl_node ( 20) 1445021 1425023 19998 390.6 K % 71.10/71.48 % 71.10/71.48 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 71.10/71.48 List 1, length 4, 0.0 K % 71.10/71.48 List 2, length 97, 0.8 K % 71.10/71.48 List 3, length 2088, 24.5 K % 71.10/71.48 List 7, length 2, 0.1 K % 71.10/71.48 List 8, length 127, 4.0 K % 71.10/71.48 List 10, length 1, 0.0 K % 71.10/71.48 List 14, length 2, 0.1 K % 71.10/71.48 List 16, length 29, 1.8 K % 71.10/71.48 List 26, length 35, 3.6 K % 71.10/71.48 List 32, length 102, 12.8 K % 71.10/71.48 List 64, length 57, 14.2 K % 71.10/71.48 List 128, length 19, 9.5 K % 71.10/71.48 List 202, length 3, 2.4 K % 71.10/71.48 % 71.10/71.48 ============================== SELECTOR REPORT ======================= % 71.10/71.48 Sos_deleted=917787, Sos_displaced=702520, Sos_size=9999 % 71.10/71.48 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 71.10/71.48 I 2147483647 high age 0 55 % 71.10/71.48 H 1 high weight 0 0 % 71.10/71.48 A 1 low age 9999 801 % 71.10/71.48 F 4 low weight 1899 3204 % 71.10/71.48 T 4 low weight 8100 3201 % 71.10/71.48 ============================== end of selector report ================ % 71.10/71.48 % 71.10/71.48 ============================== end of statistics ===================== % 71.10/71.48 % 71.10/71.48 Exiting with failure. % 71.10/71.48 % 71.10/71.48 Process 5533 exit (max_megs) Tue Apr 28 18:53:07 2026 % 71.10/71.48 Prover9 interrupted %------------------------------------------------------------------------------