%------------------------------------------------------------------------------ % 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 : n025.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 227.81s 228.15s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX191-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.33 % Computer : n025.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue Apr 28 23:54:43 EDT 2026 % 0.15/0.34 % CPUTime : % 227.81/228.14 ============================== Prover9 =============================== % 227.81/228.14 Prover9 (32) version 2009-11A, November 2009. % 227.81/228.14 Process 343 was started by sandbox2 on n025.cluster.edu, % 227.81/228.14 Tue Apr 28 23:54:43 2026 % 227.81/228.14 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_32658_n025.cluster.edu". % 227.81/228.14 ============================== end of head =========================== % 227.81/228.14 % 227.81/228.14 ============================== INPUT ================================= % 227.81/228.14 % 227.81/228.14 % Reading from file /tmp/Prover9_32658_n025.cluster.edu % 227.81/228.14 % 227.81/228.14 set(prolog_style_variables). % 227.81/228.14 set(auto2). % 227.81/228.14 % set(auto2) -> set(auto). % 227.81/228.14 % set(auto) -> set(auto_inference). % 227.81/228.14 % set(auto) -> set(auto_setup). % 227.81/228.14 % set(auto_setup) -> set(predicate_elim). % 227.81/228.14 % set(auto_setup) -> assign(eq_defs, unfold). % 227.81/228.14 % set(auto) -> set(auto_limits). % 227.81/228.14 % set(auto_limits) -> assign(max_weight, "100.000"). % 227.81/228.14 % set(auto_limits) -> assign(sos_limit, 20000). % 227.81/228.14 % set(auto) -> set(auto_denials). % 227.81/228.14 % set(auto) -> set(auto_process). % 227.81/228.14 % set(auto2) -> assign(new_constants, 1). % 227.81/228.14 % set(auto2) -> assign(fold_denial_max, 3). % 227.81/228.14 % set(auto2) -> assign(max_weight, "200.000"). % 227.81/228.14 % set(auto2) -> assign(max_hours, 1). % 227.81/228.14 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 227.81/228.14 % set(auto2) -> assign(max_seconds, 0). % 227.81/228.14 % set(auto2) -> assign(max_minutes, 5). % 227.81/228.14 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 227.81/228.14 % set(auto2) -> set(sort_initial_sos). % 227.81/228.14 % set(auto2) -> assign(sos_limit, -1). % 227.81/228.14 % set(auto2) -> assign(lrs_ticks, 3000). % 227.81/228.14 % set(auto2) -> assign(max_megs, 400). % 227.81/228.14 % set(auto2) -> assign(stats, some). % 227.81/228.14 % set(auto2) -> clear(echo_input). % 227.81/228.14 % set(auto2) -> set(quiet). % 227.81/228.14 % set(auto2) -> clear(print_initial_clauses). % 227.81/228.14 % set(auto2) -> clear(print_given). % 227.81/228.14 assign(lrs_ticks,-1). % 227.81/228.14 assign(sos_limit,10000). % 227.81/228.14 assign(order,kbo). % 227.81/228.14 set(lex_order_vars). % 227.81/228.14 clear(print_given). % 227.81/228.14 % 227.81/228.14 % formulas(sos). % not echoed (92 formulas) % 227.81/228.14 % 227.81/228.14 ============================== end of input ========================== % 227.81/228.14 % 227.81/228.14 % From the command line: assign(max_seconds, 300). % 227.81/228.14 % 227.81/228.14 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 227.81/228.14 % 227.81/228.14 % Formulas that are not ordinary clauses: % 227.81/228.14 % 227.81/228.14 ============================== end of process non-clausal formulas === % 227.81/228.14 % 227.81/228.14 ============================== PROCESS INITIAL CLAUSES =============== % 227.81/228.14 % 227.81/228.14 ============================== PREDICATE ELIMINATION ================= % 227.81/228.14 % 227.81/228.14 ============================== end predicate elimination ============= % 227.81/228.14 % 227.81/228.14 Auto_denials: % 227.81/228.14 % copying label goal to answer in negative clause % 227.81/228.14 % 227.81/228.14 Term ordering decisions: % 227.81/228.14 Function symbol KB weights: x2=1. bfalse=1. z=1. btrue=1. y=1. x=1. eq2=1. fail32=1. fail1=1. fail22=1. fail12=1. fail=1. fail3=1. fail2=1. eq=1. fail4=1. addNat=1. eq3=1. mulNat=1. impl=1. n=1. s=1. opt=1. d=1. propm4=1. aux=1. % 227.81/228.14 % 227.81/228.14 ============================== end of process initial clauses ======== % 227.81/228.14 % 227.81/228.14 ============================== CLAUSES FOR SEARCH ==================== % 227.81/228.14 % 227.81/228.14 ============================== end of clauses for search ============= % 227.81/228.14 % 227.81/228.14 ============================== SEARCH ================================ % 227.81/228.14 % 227.81/228.14 % Starting search at 0.02 seconds. % 227.81/228.14 % 227.81/228.14 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 473 (0.00 of 0.45 sec). % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=23.000, iters=4116 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=20.000, iters=3457 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=19.000, iters=3341 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=18.000, iters=3408 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=17.000, iters=3370 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=16.000, iters=3335 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=15.000, iters=3333 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=14.000, iters=3452 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=4690, wt=53.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=9577, wt=49.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=9527, wt=48.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=10735, wt=47.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=10304, wt=46.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=9233, wt=45.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=8616, wt=44.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=10701, wt=43.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=11132, wt=42.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=11680, wt=41.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=12692, wt=40.000 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=15666, wt=13.000 % 227.81/228.14 % 227.81/228.14 Low Water (keep): wt=13.000, iters=3381 % 227.81/228.14 % 227.81/228.14 Low Water (displace): id=79513, wt=12.000 % 227.81/228.14 % 227.81/228.14 ============================== STATISTICS ============================ % 227.81/228.14 % 227.81/228.14 Given=15272. Generated=2994090. Kept=261803. proofs=0. % 227.81/228.14 Usable=15120. Sos=9994. Demods=15093. Limbo=625, Disabled=236156. Hints=0. % 227.81/228.14 Kept_by_rule=0, Deleted_by_rule=0. % 227.81/228.14 Forward_subsumed=1155236. Back_subsumed=9. % 227.81/228.14 Sos_limit_deleted=1577051. Sos_displaced=235187. Sos_removed=0. % 227.81/228.14 New_demodulators=17711 (3 lex), Back_demodulated=868. Back_unit_deleted=0. % 227.81/228.14 Demod_attempts=77930658. Demod_rewrites=1975676. % 227.81/228.14 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 227.81/228.14 Nonunit_fsub_feature_tests=48. Nonunit_bsub_feature_tests=44. % 227.81/228.14 Megabytes=419.43. % 227.81/228.14 User_CPU=225.06, System_CPU=2.03, Wall_clock=228. % 227.81/228.14 % 227.81/228.14 Megs malloced by palloc(): 400. % 227.81/228.14 type (bytes each) gets frees in use bytes % 227.81/228.14 chunk ( 104) 1553 1553 0 0.0 K % 227.81/228.14 string_buf ( 8) 1552 1552 0 0.0 K % 227.81/228.14 token ( 20) 3421 3421 0 0.0 K % 227.81/228.14 pterm ( 16) 2214 2214 0 0.0 K % 227.81/228.14 hashtab ( 8) 0 0 0 0.0 K % 227.81/228.14 hashnode ( 8) 0 0 0 0.0 K % 227.81/228.14 term ( 20) 103344182 93466658 9877524 192920.4 K % 227.81/228.14 term arg arrays: 40765.7 K % 227.81/228.14 attribute ( 12) 1076825 833747 243078 2848.6 K % 227.81/228.14 ilist ( 8) 2425475340 2422533465 2941875 22983.4 K % 227.81/228.14 plist ( 8) 10739496 10388626 350870 2741.2 K % 227.81/228.14 i2list ( 12) 15707922 15707922 0 0.0 K % 227.81/228.14 just ( 12) 4364340 4093038 271302 3179.3 K % 227.81/228.14 parajust ( 16) 2978945 2718573 260372 4068.3 K % 227.81/228.14 instancejust ( 8) 0 0 0 0.0 K % 227.81/228.14 ivyjust ( 24) 0 0 0 0.0 K % 227.81/228.14 formula ( 28) 105 105 0 0.0 K % 227.81/228.14 formula arg arrays: 0.0 K % 227.81/228.14 topform ( 52) 2994183 2732287 261896 13299.4 K % 227.81/228.14 clist_pos ( 20) 792212 515224 276988 5409.9 K % 227.81/228.14 clist ( 16) 8 1 7 0.1 K % 227.81/228.14 context ( 808) 8632493 8632491 2 1.6 K % 227.81/228.14 trail ( 12) 9820710 9820708 2 0.0 K % 227.81/228.14 ac_match_pos (70044) 0 0 0 0.0 K % 227.81/228.14 ac_match_free_vars_pos (20020) % 227.81/228.14 0 0 0 0.0 K % 227.81/228.14 btm_state ( 60) 0 0 0 0.0 K % 227.81/228.14 btu_state ( 60) 0 0 0 0.0 K % 227.81/228.14 ac_position (285432) 0 0 0 0.0 K % 227.81/228.14 fpa_trie ( 20) 6149402 5191140 958262 18716.1 K % 227.81/228.14 fpa_state ( 28) 2655349 2655349 0 0.0 K % 227.81/228.14 fpa_index ( 12) 10 0 10 0.1 K % 227.81/228.14 fpa_chunk ( 20) 6452821 6336990 115831 2262.3 K % 227.81/228.14 fpa_list ( 16) 5254188 0 5254188 82096.7 K % 227.81/228.14 fpa_list chunks: 10161.2 K % 227.81/228.14 discrim ( 12) 6927086 6547309 379777 4450.5 K % 227.81/228.14 discrim_pos ( 16) 2565931 2565931 0 0.0 K % 227.81/228.14 flat2 ( 32) 21881058 21881058 0 0.0 K % 227.81/228.14 flat ( 48) 0 0 0 0.0 K % 227.81/228.14 flatterm ( 32) 100697998 100697998 0 0.0 K % 227.81/228.14 mindex ( 28) 13 0 13 0.4 K % 227.81/228.14 mindex_pos ( 56) 1341508 1341508 0 0.0 K % 227.81/228.14 lindex ( 12) 5 0 5 0.1 K % 227.81/228.14 clash ( 40) 34861 34861 0 0.0 K % 227.81/228.14 di_tree ( 12) 907 0 907 10.6 K % 227.81/228.14 avl_node ( 20) 522259 502271 19988 390.4 K % 227.81/228.14 % 227.81/228.14 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 227.81/228.14 List 1, length 5, 0.0 K % 227.81/228.14 List 2, length 106, 0.8 K % 227.81/228.14 List 3, length 16130, 189.0 K % 227.81/228.14 List 4, length 1, 0.0 K % 227.81/228.14 List 8, length 51, 1.6 K % 227.81/228.14 List 10, length 2, 0.1 K % 227.81/228.14 List 14, length 2, 0.1 K % 227.81/228.14 List 16, length 67, 4.2 K % 227.81/228.14 List 26, length 36, 3.7 K % 227.81/228.14 List 32, length 22, 2.8 K % 227.81/228.14 List 64, length 2488, 622.0 K % 227.81/228.14 List 128, length 76, 38.0 K % 227.81/228.14 List 202, length 2, 1.6 K % 227.81/228.14 List 256, length 150, 150.0 K % 227.81/228.14 % 227.81/228.14 ============================== SELECTOR REPORT ======================= % 227.81/228.14 Sos_deleted=1577051, Sos_displaced=235187, Sos_size=9994 % 227.81/228.14 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 227.81/228.14 I 2147483647 high age 0 91 % 227.81/228.14 H 1 high weight 0 0 % 227.81/228.14 A 1 low age 9994 1729 % 227.81/228.14 F 4 low weight 2565 6540 % 227.81/228.14 T 4 low weight 7429 6912 % 227.81/228.14 ============================== end of selector report ================ % 227.81/228.14 % 227.81/228.14 ============================== end of statistics ===================== % 227.81/228.14 % 227.81/228.14 Exiting with failure. % 227.81/228.14 % 227.81/228.14 Process 343 exit (max_megs) Tue Apr 28 23:58:31 2026 % 227.81/228.15 Prover9 interrupted %------------------------------------------------------------------------------