%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX193-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n001.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 203.60s 203.91s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX193-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.33 % Computer : n001.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % 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 00:05:33 EDT 2026 % 0.17/0.34 % CPUTime : % 203.60/203.90 ============================== Prover9 =============================== % 203.60/203.90 Prover9 (32) version 2009-11A, November 2009. % 203.60/203.90 Process 17988 was started by sandbox2 on n001.cluster.edu, % 203.60/203.90 Wed Apr 29 00:05:34 2026 % 203.60/203.90 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_17834_n001.cluster.edu". % 203.60/203.90 ============================== end of head =========================== % 203.60/203.90 % 203.60/203.90 ============================== INPUT ================================= % 203.60/203.90 % 203.60/203.90 % Reading from file /tmp/Prover9_17834_n001.cluster.edu % 203.60/203.90 % 203.60/203.90 set(prolog_style_variables). % 203.60/203.90 set(auto2). % 203.60/203.90 % set(auto2) -> set(auto). % 203.60/203.90 % set(auto) -> set(auto_inference). % 203.60/203.90 % set(auto) -> set(auto_setup). % 203.60/203.90 % set(auto_setup) -> set(predicate_elim). % 203.60/203.90 % set(auto_setup) -> assign(eq_defs, unfold). % 203.60/203.90 % set(auto) -> set(auto_limits). % 203.60/203.90 % set(auto_limits) -> assign(max_weight, "100.000"). % 203.60/203.90 % set(auto_limits) -> assign(sos_limit, 20000). % 203.60/203.90 % set(auto) -> set(auto_denials). % 203.60/203.90 % set(auto) -> set(auto_process). % 203.60/203.90 % set(auto2) -> assign(new_constants, 1). % 203.60/203.90 % set(auto2) -> assign(fold_denial_max, 3). % 203.60/203.90 % set(auto2) -> assign(max_weight, "200.000"). % 203.60/203.90 % set(auto2) -> assign(max_hours, 1). % 203.60/203.90 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 203.60/203.90 % set(auto2) -> assign(max_seconds, 0). % 203.60/203.90 % set(auto2) -> assign(max_minutes, 5). % 203.60/203.90 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 203.60/203.90 % set(auto2) -> set(sort_initial_sos). % 203.60/203.90 % set(auto2) -> assign(sos_limit, -1). % 203.60/203.90 % set(auto2) -> assign(lrs_ticks, 3000). % 203.60/203.90 % set(auto2) -> assign(max_megs, 400). % 203.60/203.90 % set(auto2) -> assign(stats, some). % 203.60/203.90 % set(auto2) -> clear(echo_input). % 203.60/203.90 % set(auto2) -> set(quiet). % 203.60/203.90 % set(auto2) -> clear(print_initial_clauses). % 203.60/203.90 % set(auto2) -> clear(print_given). % 203.60/203.90 assign(lrs_ticks,-1). % 203.60/203.90 assign(sos_limit,10000). % 203.60/203.90 assign(order,kbo). % 203.60/203.90 set(lex_order_vars). % 203.60/203.90 clear(print_given). % 203.60/203.90 % 203.60/203.90 % formulas(sos). % not echoed (92 formulas) % 203.60/203.90 % 203.60/203.90 ============================== end of input ========================== % 203.60/203.90 % 203.60/203.90 % From the command line: assign(max_seconds, 300). % 203.60/203.90 % 203.60/203.90 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 203.60/203.90 % 203.60/203.90 % Formulas that are not ordinary clauses: % 203.60/203.90 % 203.60/203.90 ============================== end of process non-clausal formulas === % 203.60/203.90 % 203.60/203.90 ============================== PROCESS INITIAL CLAUSES =============== % 203.60/203.90 % 203.60/203.90 ============================== PREDICATE ELIMINATION ================= % 203.60/203.90 % 203.60/203.90 ============================== end predicate elimination ============= % 203.60/203.90 % 203.60/203.90 Auto_denials: % 203.60/203.90 % copying label goal to answer in negative clause % 203.60/203.90 % 203.60/203.90 Term ordering decisions: % 203.60/203.90 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. propm6=1. aux=1. % 203.60/203.90 % 203.60/203.90 ============================== end of process initial clauses ======== % 203.60/203.90 % 203.60/203.90 ============================== CLAUSES FOR SEARCH ==================== % 203.60/203.90 % 203.60/203.90 ============================== end of clauses for search ============= % 203.60/203.90 % 203.60/203.90 ============================== SEARCH ================================ % 203.60/203.90 % 203.60/203.90 % Starting search at 0.02 seconds. % 203.60/203.90 % 203.60/203.90 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 473 (0.00 of 0.44 sec). % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=23.000, iters=4116 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=20.000, iters=3457 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=19.000, iters=3341 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=18.000, iters=3408 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=17.000, iters=3370 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=16.000, iters=3335 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=15.000, iters=3333 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=14.000, iters=3452 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=4690, wt=97.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=9577, wt=71.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=9527, wt=70.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=10735, wt=69.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=10304, wt=68.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=9233, wt=67.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=8616, wt=66.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=10701, wt=65.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=11132, wt=64.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=11680, wt=63.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=12692, wt=62.000 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=15666, wt=13.000 % 203.60/203.90 % 203.60/203.90 Low Water (keep): wt=13.000, iters=3381 % 203.60/203.90 % 203.60/203.90 Low Water (displace): id=79513, wt=12.000 % 203.60/203.90 % 203.60/203.90 ============================== STATISTICS ============================ % 203.60/203.90 % 203.60/203.90 Given=13139. Generated=2464136. Kept=196107. proofs=0. % 203.60/203.90 Usable=12987. Sos=9995. Demods=13863. Limbo=1242, Disabled=171975. Hints=0. % 203.60/203.90 Kept_by_rule=0, Deleted_by_rule=0. % 203.60/203.90 Forward_subsumed=924543. Back_subsumed=9. % 203.60/203.90 Sos_limit_deleted=1343486. Sos_displaced=171056. Sos_removed=0. % 203.60/203.90 New_demodulators=16404 (3 lex), Back_demodulated=818. Back_unit_deleted=0. % 203.60/203.90 Demod_attempts=83479947. Demod_rewrites=1627363. % 203.60/203.90 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 203.60/203.90 Nonunit_fsub_feature_tests=48. Nonunit_bsub_feature_tests=44. % 203.60/203.90 Megabytes=419.43. % 203.60/203.90 User_CPU=201.16, System_CPU=1.71, Wall_clock=203. % 203.60/203.90 % 203.60/203.90 Megs malloced by palloc(): 400. % 203.60/203.90 type (bytes each) gets frees in use bytes % 203.60/203.90 chunk ( 104) 1576 1576 0 0.0 K % 203.60/203.90 string_buf ( 8) 1574 1574 0 0.0 K % 203.60/203.90 token ( 20) 3476 3476 0 0.0 K % 203.60/203.90 pterm ( 16) 2258 2258 0 0.0 K % 203.60/203.90 hashtab ( 8) 0 0 0 0.0 K % 203.60/203.90 hashnode ( 8) 0 0 0 0.0 K % 203.60/203.90 term ( 20) 105339719 94105369 11234350 219420.9 K % 203.60/203.90 term arg arrays: 45499.4 K % 203.60/203.90 attribute ( 12) 895210 716521 178689 2094.0 K % 203.60/203.90 ilist ( 8) 2403122652 2400946818 2175834 16998.7 K % 203.60/203.90 plist ( 8) 11561506 11279077 282429 2206.5 K % 203.60/203.90 i2list ( 12) 11986630 11986630 0 0.0 K % 203.60/203.90 just ( 12) 3588382 3384234 204148 2392.4 K % 203.60/203.90 parajust ( 16) 2451085 2256401 194684 3041.9 K % 203.60/203.90 instancejust ( 8) 0 0 0 0.0 K % 203.60/203.90 ivyjust ( 24) 0 0 0 0.0 K % 203.60/203.90 formula ( 28) 105 105 0 0.0 K % 203.60/203.90 formula arg arrays: 0.0 K % 203.60/203.90 topform ( 52) 2464229 2268029 196200 9963.3 K % 203.60/203.90 clist_pos ( 20) 592582 382520 210062 4102.8 K % 203.60/203.90 clist ( 16) 8 1 7 0.1 K % 203.60/203.90 context ( 808) 6962789 6962787 2 1.6 K % 203.60/203.90 trail ( 12) 8426251 8426249 2 0.0 K % 203.60/203.90 ac_match_pos (70044) 0 0 0 0.0 K % 203.60/203.90 ac_match_free_vars_pos (20020) % 203.60/203.90 0 0 0 0.0 K % 203.60/203.90 btm_state ( 60) 0 0 0 0.0 K % 203.60/203.90 btu_state ( 60) 0 0 0 0.0 K % 203.60/203.90 ac_position (285432) 0 0 0 0.0 K % 203.60/203.90 fpa_trie ( 20) 4636524 3808691 827833 16168.6 K % 203.60/203.90 fpa_state ( 28) 2035007 2035007 0 0.0 K % 203.60/203.90 fpa_index ( 12) 10 0 10 0.1 K % 203.60/203.90 fpa_chunk ( 20) 4824920 4700299 124621 2434.0 K % 203.60/203.90 fpa_list ( 16) 3875852 0 3875852 60560.2 K % 203.60/203.90 fpa_list chunks: 15429.6 K % 203.60/203.90 discrim ( 12) 9067980 8492614 575366 6742.6 K % 203.60/203.90 discrim_pos ( 16) 2082458 2082458 0 0.0 K % 203.60/203.90 flat2 ( 32) 23536555 23536555 0 0.0 K % 203.60/203.90 flat ( 48) 0 0 0 0.0 K % 203.60/203.90 flatterm ( 32) 101373048 101373048 0 0.0 K % 203.60/203.90 mindex ( 28) 13 0 13 0.4 K % 203.60/203.90 mindex_pos ( 56) 1016037 1016037 0 0.0 K % 203.60/203.90 lindex ( 12) 5 0 5 0.1 K % 203.60/203.90 clash ( 40) 29825 29825 0 0.0 K % 203.60/203.90 di_tree ( 12) 907 0 907 10.6 K % 203.60/203.90 avl_node ( 20) 389633 369643 19990 390.4 K % 203.60/203.90 % 203.60/203.90 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 203.60/203.90 List 1, length 5, 0.0 K % 203.60/203.90 List 2, length 106, 0.8 K % 203.60/203.90 List 4, length 6, 0.1 K % 203.60/203.90 List 6, length 25, 0.6 K % 203.60/203.90 List 8, length 63, 2.0 K % 203.60/203.90 List 10, length 2, 0.1 K % 203.60/203.90 List 14, length 2, 0.1 K % 203.60/203.90 List 26, length 59, 6.0 K % 203.60/203.90 List 32, length 29, 3.6 K % 203.60/203.91 List 64, length 6673, 1668.2 K % 203.60/203.91 List 202, length 2, 1.6 K % 203.60/203.91 List 256, length 58, 58.0 K % 203.60/203.91 % 203.60/203.91 ============================== SELECTOR REPORT ======================= % 203.60/203.91 Sos_deleted=1343486, Sos_displaced=171056, Sos_size=9995 % 203.60/203.91 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 203.60/203.91 I 2147483647 high age 0 91 % 203.60/203.91 H 1 high weight 0 0 % 203.60/203.91 A 1 low age 9995 1492 % 203.60/203.91 F 4 low weight 2611 5592 % 203.60/203.91 T 4 low weight 7384 5964 % 203.60/203.91 ============================== end of selector report ================ % 203.60/203.91 % 203.60/203.91 ============================== end of statistics ===================== % 203.60/203.91 % 203.60/203.91 Exiting with failure. % 203.60/203.91 % 203.60/203.91 Process 17988 exit (max_megs) Wed Apr 29 00:08:57 2026 % 203.60/203.91 Prover9 interrupted %------------------------------------------------------------------------------