%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX189-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n012.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 : Unknown 243.49s 243.78s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWX189-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.10 % Command : tptp2X_and_run_prover9 %d %s % 0.12/0.30 % Computer : n012.cluster.edu % 0.12/0.30 % Model : x86_64 x86_64 % 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.30 % Memory : 8042.1875MB % 0.12/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.30 % CPULimit : 300 % 0.12/0.30 % WCLimit : 300 % 0.12/0.30 % DateTime : Tue Apr 28 23:46:15 EDT 2026 % 0.12/0.30 % CPUTime : % 243.49/243.78 ============================== Prover9 =============================== % 243.49/243.78 Prover9 (32) version 2009-11A, November 2009. % 243.49/243.78 Process 30597 was started by sandbox2 on n012.cluster.edu, % 243.49/243.78 Tue Apr 28 23:46:16 2026 % 243.49/243.78 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_30444_n012.cluster.edu". % 243.49/243.78 ============================== end of head =========================== % 243.49/243.78 % 243.49/243.78 ============================== INPUT ================================= % 243.49/243.78 % 243.49/243.78 % Reading from file /tmp/Prover9_30444_n012.cluster.edu % 243.49/243.78 % 243.49/243.78 set(prolog_style_variables). % 243.49/243.78 set(auto2). % 243.49/243.78 % set(auto2) -> set(auto). % 243.49/243.78 % set(auto) -> set(auto_inference). % 243.49/243.78 % set(auto) -> set(auto_setup). % 243.49/243.78 % set(auto_setup) -> set(predicate_elim). % 243.49/243.78 % set(auto_setup) -> assign(eq_defs, unfold). % 243.49/243.78 % set(auto) -> set(auto_limits). % 243.49/243.78 % set(auto_limits) -> assign(max_weight, "100.000"). % 243.49/243.78 % set(auto_limits) -> assign(sos_limit, 20000). % 243.49/243.78 % set(auto) -> set(auto_denials). % 243.49/243.78 % set(auto) -> set(auto_process). % 243.49/243.78 % set(auto2) -> assign(new_constants, 1). % 243.49/243.78 % set(auto2) -> assign(fold_denial_max, 3). % 243.49/243.78 % set(auto2) -> assign(max_weight, "200.000"). % 243.49/243.78 % set(auto2) -> assign(max_hours, 1). % 243.49/243.78 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 243.49/243.78 % set(auto2) -> assign(max_seconds, 0). % 243.49/243.78 % set(auto2) -> assign(max_minutes, 5). % 243.49/243.78 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 243.49/243.78 % set(auto2) -> set(sort_initial_sos). % 243.49/243.78 % set(auto2) -> assign(sos_limit, -1). % 243.49/243.78 % set(auto2) -> assign(lrs_ticks, 3000). % 243.49/243.78 % set(auto2) -> assign(max_megs, 400). % 243.49/243.78 % set(auto2) -> assign(stats, some). % 243.49/243.78 % set(auto2) -> clear(echo_input). % 243.49/243.78 % set(auto2) -> set(quiet). % 243.49/243.78 % set(auto2) -> clear(print_initial_clauses). % 243.49/243.78 % set(auto2) -> clear(print_given). % 243.49/243.78 assign(lrs_ticks,-1). % 243.49/243.78 assign(sos_limit,10000). % 243.49/243.78 assign(order,kbo). % 243.49/243.78 set(lex_order_vars). % 243.49/243.78 clear(print_given). % 243.49/243.78 % 243.49/243.78 % formulas(sos). % not echoed (92 formulas) % 243.49/243.78 % 243.49/243.78 ============================== end of input ========================== % 243.49/243.78 % 243.49/243.78 % From the command line: assign(max_seconds, 300). % 243.49/243.78 % 243.49/243.78 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 243.49/243.78 % 243.49/243.78 % Formulas that are not ordinary clauses: % 243.49/243.78 % 243.49/243.78 ============================== end of process non-clausal formulas === % 243.49/243.78 % 243.49/243.78 ============================== PROCESS INITIAL CLAUSES =============== % 243.49/243.78 % 243.49/243.78 ============================== PREDICATE ELIMINATION ================= % 243.49/243.78 % 243.49/243.78 ============================== end predicate elimination ============= % 243.49/243.78 % 243.49/243.78 Auto_denials: % 243.49/243.78 % copying label goal to answer in negative clause % 243.49/243.78 % 243.49/243.78 Term ordering decisions: % 243.49/243.78 Function symbol KB weights: x2=1. bfalse=1. z=1. btrue=1. x=1. y=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. prop2=1. aux=1. % 243.49/243.78 % 243.49/243.78 ============================== end of process initial clauses ======== % 243.49/243.78 % 243.49/243.78 ============================== CLAUSES FOR SEARCH ==================== % 243.49/243.78 % 243.49/243.78 ============================== end of clauses for search ============= % 243.49/243.78 % 243.49/243.78 ============================== SEARCH ================================ % 243.49/243.78 % 243.49/243.78 % Starting search at 0.01 seconds. % 243.49/243.78 % 243.49/243.78 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 473 (0.00 of 0.59 sec). % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=23.000, iters=4116 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=20.000, iters=3457 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=19.000, iters=3341 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=18.000, iters=3408 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=17.000, iters=3370 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=16.000, iters=3335 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=15.000, iters=3333 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=14.000, iters=3452 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=5051, wt=41.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=4667, wt=38.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=4690, wt=37.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=8616, wt=36.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=10701, wt=35.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=11132, wt=34.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=11680, wt=33.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=12692, wt=32.000 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=15768, wt=13.000 % 243.49/243.78 % 243.49/243.78 Low Water (keep): wt=13.000, iters=3386 % 243.49/243.78 % 243.49/243.78 Low Water (displace): id=79489, wt=12.000 % 243.49/243.78 % 243.49/243.78 ============================== STATISTICS ============================ % 243.49/243.78 % 243.49/243.78 Given=15965. Generated=3288733. Kept=292821. proofs=0. % 243.49/243.78 Usable=15813. Sos=9998. Demods=15308. Limbo=713, Disabled=266389. Hints=0. % 243.49/243.78 Kept_by_rule=0, Deleted_by_rule=0. % 243.49/243.78 Forward_subsumed=1298504. Back_subsumed=9. % 243.49/243.78 Sos_limit_deleted=1697407. Sos_displaced=265416. Sos_removed=0. % 243.49/243.78 New_demodulators=17949 (3 lex), Back_demodulated=872. Back_unit_deleted=0. % 243.49/243.78 Demod_attempts=76657815. Demod_rewrites=2195516. % 243.49/243.78 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 243.49/243.78 Nonunit_fsub_feature_tests=48. Nonunit_bsub_feature_tests=44. % 243.49/243.78 Megabytes=419.43. % 243.49/243.78 User_CPU=240.36, System_CPU=2.50, Wall_clock=243. % 243.49/243.78 % 243.49/243.78 Megs malloced by palloc(): 400. % 243.49/243.78 type (bytes each) gets frees in use bytes % 243.49/243.78 chunk ( 104) 1545 1545 0 0.0 K % 243.49/243.78 string_buf ( 8) 1544 1544 0 0.0 K % 243.49/243.78 token ( 20) 3401 3401 0 0.0 K % 243.49/243.78 pterm ( 16) 2198 2198 0 0.0 K % 243.49/243.78 hashtab ( 8) 0 0 0 0.0 K % 243.49/243.78 hashnode ( 8) 0 0 0 0.0 K % 243.49/243.78 term ( 20) 104624929 95643269 8981660 175423.0 K % 243.49/243.78 term arg arrays: 37618.1 K % 243.49/243.78 attribute ( 12) 1174387 900529 273858 3209.3 K % 243.49/243.78 ilist ( 8) 2351138802 2347821808 3316994 25914.0 K % 243.49/243.78 plist ( 8) 10082893 9700043 382850 2991.0 K % 243.49/243.78 i2list ( 12) 17519318 17519318 0 0.0 K % 243.49/243.78 just ( 12) 4809585 4506883 302702 3547.3 K % 243.49/243.78 parajust ( 16) 3272946 2981559 291387 4552.9 K % 243.49/243.78 instancejust ( 8) 0 0 0 0.0 K % 243.49/243.78 ivyjust ( 24) 0 0 0 0.0 K % 243.49/243.78 formula ( 28) 105 105 0 0.0 K % 243.49/243.78 formula arg arrays: 0.0 K % 243.49/243.78 topform ( 52) 3288825 2995911 292914 14874.5 K % 243.49/243.78 clist_pos ( 20) 885324 577103 308221 6019.9 K % 243.49/243.78 clist ( 16) 8 1 7 0.1 K % 243.49/243.78 context ( 808) 9505692 9505690 2 1.6 K % 243.49/243.78 trail ( 12) 10575459 10575457 2 0.0 K % 243.49/243.78 ac_match_pos (70044) 0 0 0 0.0 K % 243.49/243.78 ac_match_free_vars_pos (20020) % 243.49/243.78 0 0 0 0.0 K % 243.49/243.78 btm_state ( 60) 0 0 0 0.0 K % 243.49/243.78 btu_state ( 60) 0 0 0 0.0 K % 243.49/243.78 ac_position (285432) 0 0 0 0.0 K % 243.49/243.78 fpa_trie ( 20) 7201322 6164771 1036551 20245.1 K % 243.49/243.78 fpa_state ( 28) 2941984 2941984 0 0.0 K % 243.49/243.78 fpa_index ( 12) 10 0 10 0.1 K % 243.49/243.78 fpa_chunk ( 20) 7486499 7370654 115845 2262.6 K % 243.49/243.78 fpa_list ( 16) 6229698 0 6229698 97339.0 K % 243.49/243.78 fpa_list chunks: 8190.5 K % 243.49/243.78 discrim ( 12) 5666202 5352662 313540 3674.3 K % 243.49/243.78 discrim_pos ( 16) 2859101 2859101 0 0.0 K % 243.49/243.78 flat2 ( 32) 20865648 20865648 0 0.0 K % 243.49/243.78 flat ( 48) 0 0 0 0.0 K % 243.49/243.78 flatterm ( 32) 102183749 102183715 34 1.1 K % 243.49/243.78 mindex ( 28) 13 0 13 0.4 K % 243.49/243.78 mindex_pos ( 56) 1504895 1504895 0 0.0 K % 243.49/243.78 lindex ( 12) 5 0 5 0.1 K % 243.49/243.78 clash ( 40) 36445 36445 0 0.0 K % 243.49/243.78 di_tree ( 12) 907 0 907 10.6 K % 243.49/243.78 avl_node ( 20) 584119 564123 19996 390.5 K % 243.49/243.78 % 243.49/243.78 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 243.49/243.78 List 1, length 5, 0.0 K % 243.49/243.78 List 2, length 104, 0.8 K % 243.49/243.78 List 3, length 3872, 45.4 K % 243.49/243.78 List 8, length 12, 0.4 K % 243.49/243.78 List 10, length 2, 0.1 K % 243.49/243.78 List 14, length 2, 0.1 K % 243.49/243.78 List 16, length 48, 3.0 K % 243.49/243.78 List 26, length 28, 2.8 K % 243.49/243.78 List 32, length 44, 5.5 K % 243.49/243.78 List 64, length 668, 167.0 K % 243.49/243.78 List 128, length 26, 13.0 K % 243.49/243.78 List 202, length 2, 1.6 K % 243.49/243.78 % 243.49/243.78 ============================== SELECTOR REPORT ======================= % 243.49/243.78 Sos_deleted=1697407, Sos_displaced=265416, Sos_size=9998 % 243.49/243.78 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 243.49/243.78 I 2147483647 high age 0 91 % 243.49/243.78 H 1 high weight 0 0 % 243.49/243.78 A 1 low age 9998 1806 % 243.49/243.78 F 4 low weight 2755 6848 % 243.49/243.78 T 4 low weight 7243 7220 % 243.49/243.78 ============================== end of selector report ================ % 243.49/243.78 % 243.49/243.78 ============================== end of statistics ===================== % 243.49/243.78 % 243.49/243.78 Exiting with failure. % 243.49/243.78 % 243.49/243.78 Process 30597 exit (max_megs) Tue Apr 28 23:50:19 2026 % 243.49/243.78 Prover9 interrupted %------------------------------------------------------------------------------