%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX192-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n027.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 206.53s 206.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX192-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 : n027.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 : Tue Apr 28 23:59:04 EDT 2026 % 0.17/0.34 % CPUTime : % 206.53/206.82 ============================== Prover9 =============================== % 206.53/206.82 Prover9 (32) version 2009-11A, November 2009. % 206.53/206.82 Process 28240 was started by sandbox on n027.cluster.edu, % 206.53/206.82 Tue Apr 28 23:59:05 2026 % 206.53/206.82 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_28087_n027.cluster.edu". % 206.53/206.82 ============================== end of head =========================== % 206.53/206.82 % 206.53/206.82 ============================== INPUT ================================= % 206.53/206.82 % 206.53/206.82 % Reading from file /tmp/Prover9_28087_n027.cluster.edu % 206.53/206.82 % 206.53/206.82 set(prolog_style_variables). % 206.53/206.82 set(auto2). % 206.53/206.82 % set(auto2) -> set(auto). % 206.53/206.82 % set(auto) -> set(auto_inference). % 206.53/206.82 % set(auto) -> set(auto_setup). % 206.53/206.82 % set(auto_setup) -> set(predicate_elim). % 206.53/206.82 % set(auto_setup) -> assign(eq_defs, unfold). % 206.53/206.82 % set(auto) -> set(auto_limits). % 206.53/206.82 % set(auto_limits) -> assign(max_weight, "100.000"). % 206.53/206.82 % set(auto_limits) -> assign(sos_limit, 20000). % 206.53/206.82 % set(auto) -> set(auto_denials). % 206.53/206.82 % set(auto) -> set(auto_process). % 206.53/206.82 % set(auto2) -> assign(new_constants, 1). % 206.53/206.82 % set(auto2) -> assign(fold_denial_max, 3). % 206.53/206.82 % set(auto2) -> assign(max_weight, "200.000"). % 206.53/206.82 % set(auto2) -> assign(max_hours, 1). % 206.53/206.82 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 206.53/206.82 % set(auto2) -> assign(max_seconds, 0). % 206.53/206.82 % set(auto2) -> assign(max_minutes, 5). % 206.53/206.82 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 206.53/206.82 % set(auto2) -> set(sort_initial_sos). % 206.53/206.82 % set(auto2) -> assign(sos_limit, -1). % 206.53/206.82 % set(auto2) -> assign(lrs_ticks, 3000). % 206.53/206.82 % set(auto2) -> assign(max_megs, 400). % 206.53/206.82 % set(auto2) -> assign(stats, some). % 206.53/206.82 % set(auto2) -> clear(echo_input). % 206.53/206.82 % set(auto2) -> set(quiet). % 206.53/206.82 % set(auto2) -> clear(print_initial_clauses). % 206.53/206.82 % set(auto2) -> clear(print_given). % 206.53/206.82 assign(lrs_ticks,-1). % 206.53/206.82 assign(sos_limit,10000). % 206.53/206.82 assign(order,kbo). % 206.53/206.82 set(lex_order_vars). % 206.53/206.82 clear(print_given). % 206.53/206.82 % 206.53/206.82 % formulas(sos). % not echoed (92 formulas) % 206.53/206.82 % 206.53/206.82 ============================== end of input ========================== % 206.53/206.82 % 206.53/206.82 % From the command line: assign(max_seconds, 300). % 206.53/206.82 % 206.53/206.82 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 206.53/206.82 % 206.53/206.82 % Formulas that are not ordinary clauses: % 206.53/206.82 % 206.53/206.82 ============================== end of process non-clausal formulas === % 206.53/206.82 % 206.53/206.82 ============================== PROCESS INITIAL CLAUSES =============== % 206.53/206.82 % 206.53/206.82 ============================== PREDICATE ELIMINATION ================= % 206.53/206.82 % 206.53/206.82 ============================== end predicate elimination ============= % 206.53/206.82 % 206.53/206.82 Auto_denials: % 206.53/206.82 % copying label goal to answer in negative clause % 206.53/206.82 % 206.53/206.82 Term ordering decisions: % 206.53/206.82 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. propm5=1. aux=1. % 206.53/206.82 % 206.53/206.82 ============================== end of process initial clauses ======== % 206.53/206.82 % 206.53/206.82 ============================== CLAUSES FOR SEARCH ==================== % 206.53/206.82 % 206.53/206.82 ============================== end of clauses for search ============= % 206.53/206.82 % 206.53/206.82 ============================== SEARCH ================================ % 206.53/206.82 % 206.53/206.82 % Starting search at 0.02 seconds. % 206.53/206.82 % 206.53/206.82 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 473 (0.00 of 0.45 sec). % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=23.000, iters=4116 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=20.000, iters=3457 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=19.000, iters=3341 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=18.000, iters=3408 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=17.000, iters=3370 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=16.000, iters=3335 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=15.000, iters=3333 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=14.000, iters=3452 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=4690, wt=73.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=9577, wt=59.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=9527, wt=58.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=10735, wt=57.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=10304, wt=56.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=9233, wt=55.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=8616, wt=54.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=10701, wt=53.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=11132, wt=52.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=11680, wt=51.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=12692, wt=50.000 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=15666, wt=13.000 % 206.53/206.82 % 206.53/206.82 Low Water (keep): wt=13.000, iters=3381 % 206.53/206.82 % 206.53/206.82 Low Water (displace): id=79513, wt=12.000 % 206.53/206.82 % 206.53/206.82 ============================== STATISTICS ============================ % 206.53/206.82 % 206.53/206.82 Given=14372. Generated=2682563. Kept=227197. proofs=0. % 206.53/206.82 Usable=14220. Sos=9996. Demods=14229. Limbo=1233, Disabled=201839. Hints=0. % 206.53/206.82 Kept_by_rule=0, Deleted_by_rule=0. % 206.53/206.82 Forward_subsumed=1015309. Back_subsumed=9. % 206.53/206.82 Sos_limit_deleted=1440057. Sos_displaced=200879. Sos_removed=0. % 206.53/206.82 New_demodulators=16811 (3 lex), Back_demodulated=859. Back_unit_deleted=0. % 206.53/206.82 Demod_attempts=79498530. Demod_rewrites=1766158. % 206.53/206.82 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 206.53/206.82 Nonunit_fsub_feature_tests=48. Nonunit_bsub_feature_tests=44. % 206.53/206.82 Megabytes=419.43. % 206.53/206.82 User_CPU=204.15, System_CPU=1.67, Wall_clock=206. % 206.53/206.82 % 206.53/206.82 Megs malloced by palloc(): 400. % 206.53/206.82 type (bytes each) gets frees in use bytes % 206.53/206.82 chunk ( 104) 1563 1563 0 0.0 K % 206.53/206.82 string_buf ( 8) 1562 1562 0 0.0 K % 206.53/206.82 token ( 20) 3446 3446 0 0.0 K % 206.53/206.82 pterm ( 16) 2234 2234 0 0.0 K % 206.53/206.82 hashtab ( 8) 0 0 0 0.0 K % 206.53/206.82 hashnode ( 8) 0 0 0 0.0 K % 206.53/206.82 term ( 20) 102335877 91725662 10610215 207230.8 K % 206.53/206.82 term arg arrays: 43319.2 K % 206.53/206.82 attribute ( 12) 979663 770291 209372 2453.6 K % 206.53/206.82 ilist ( 8) 2467469883 2464936724 2533159 19790.3 K % 206.53/206.82 plist ( 8) 11165581 10850471 315110 2461.8 K % 206.53/206.82 i2list ( 12) 13382235 13382235 0 0.0 K % 206.53/206.82 just ( 12) 3896498 3660633 235865 2764.0 K % 206.53/206.82 parajust ( 16) 2668253 2442487 225766 3527.6 K % 206.53/206.82 instancejust ( 8) 0 0 0 0.0 K % 206.53/206.82 ivyjust ( 24) 0 0 0 0.0 K % 206.53/206.82 formula ( 28) 105 105 0 0.0 K % 206.53/206.82 formula arg arrays: 0.0 K % 206.53/206.82 topform ( 52) 2682655 2455366 227289 11542.0 K % 206.53/206.82 clist_pos ( 20) 686273 444756 241517 4717.1 K % 206.53/206.82 clist ( 16) 8 1 7 0.1 K % 206.53/206.82 context ( 808) 7704352 7704350 2 1.6 K % 206.53/206.82 trail ( 12) 9043645 9043643 2 0.0 K % 206.53/206.82 ac_match_pos (70044) 0 0 0 0.0 K % 206.53/206.82 ac_match_free_vars_pos (20020) % 206.53/206.82 0 0 0 0.0 K % 206.53/206.82 btm_state ( 60) 0 0 0 0.0 K % 206.53/206.82 btu_state ( 60) 0 0 0 0.0 K % 206.53/206.82 ac_position (285432) 0 0 0 0.0 K % 206.53/206.82 fpa_trie ( 20) 5316682 4406717 909965 17772.8 K % 206.53/206.82 fpa_state ( 28) 2330616 2330616 0 0.0 K % 206.53/206.82 fpa_index ( 12) 10 0 10 0.1 K % 206.53/206.82 fpa_chunk ( 20) 5533209 5412339 120870 2360.7 K % 206.53/206.82 fpa_list ( 16) 4471042 0 4471042 69860.0 K % 206.53/206.82 fpa_list chunks: 12986.8 K % 206.53/206.82 discrim ( 12) 8075198 7579340 495858 5810.8 K % 206.53/206.82 discrim_pos ( 16) 2281449 2281449 0 0.0 K % 206.53/206.82 flat2 ( 32) 22676876 22676876 0 0.0 K % 206.53/206.82 flat ( 48) 0 0 0 0.0 K % 206.53/206.82 flatterm ( 32) 99276818 99276818 0 0.0 K % 206.53/206.82 mindex ( 28) 13 0 13 0.4 K % 206.53/206.82 mindex_pos ( 56) 1168834 1168834 0 0.0 K % 206.53/206.82 lindex ( 12) 5 0 5 0.1 K % 206.53/206.82 clash ( 40) 32809 32809 0 0.0 K % 206.53/206.82 di_tree ( 12) 907 0 907 10.6 K % 206.53/206.82 avl_node ( 20) 451829 431837 19992 390.5 K % 206.53/206.82 % 206.53/206.82 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 206.53/206.82 List 1, length 5, 0.0 K % 206.53/206.82 List 2, length 107, 0.8 K % 206.53/206.82 List 6, length 12, 0.3 K % 206.53/206.82 List 7, length 9, 0.2 K % 206.53/206.82 List 8, length 68, 2.1 K % 206.53/206.82 List 10, length 2, 0.1 K % 206.53/206.82 List 14, length 2, 0.1 K % 206.53/206.82 List 26, length 46, 4.7 K % 206.53/206.82 List 64, length 4649, 1162.2 K % 206.53/206.83 List 202, length 2, 1.6 K % 206.53/206.83 % 206.53/206.83 ============================== SELECTOR REPORT ======================= % 206.53/206.83 Sos_deleted=1440057, Sos_displaced=200879, Sos_size=9996 % 206.53/206.83 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 206.53/206.83 I 2147483647 high age 0 91 % 206.53/206.83 H 1 high weight 0 0 % 206.53/206.83 A 1 low age 9996 1629 % 206.53/206.83 F 4 low weight 2931 6140 % 206.53/206.83 T 4 low weight 7065 6512 % 206.53/206.83 ============================== end of selector report ================ % 206.53/206.83 % 206.53/206.83 ============================== end of statistics ===================== % 206.53/206.83 % 206.53/206.83 Exiting with failure. % 206.53/206.83 % 206.53/206.83 Process 28240 exit (max_megs) Wed Apr 29 00:02:31 2026 % 206.53/206.83 Prover9 interrupted %------------------------------------------------------------------------------