%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX188-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n010.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 182.53s 182.85s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX188-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.14/0.33 % Computer : n010.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Tue Apr 28 23:41:05 EDT 2026 % 0.14/0.33 % CPUTime : % 78.13/78.49 ============================== Prover9 =============================== % 78.13/78.49 Prover9 (32) version 2009-11A, November 2009. % 78.13/78.49 Process 23440 was started by sandbox on n010.cluster.edu, % 78.13/78.49 Tue Apr 28 23:41:06 2026 % 78.13/78.49 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_23270_n010.cluster.edu". % 78.13/78.49 ============================== end of head =========================== % 78.13/78.49 % 78.13/78.49 ============================== INPUT ================================= % 78.13/78.49 % 78.13/78.49 % Reading from file /tmp/Prover9_23270_n010.cluster.edu % 78.13/78.49 % 78.13/78.49 set(prolog_style_variables). % 78.13/78.49 set(auto2). % 78.13/78.49 % set(auto2) -> set(auto). % 78.13/78.49 % set(auto) -> set(auto_inference). % 78.13/78.49 % set(auto) -> set(auto_setup). % 78.13/78.49 % set(auto_setup) -> set(predicate_elim). % 78.13/78.49 % set(auto_setup) -> assign(eq_defs, unfold). % 78.13/78.49 % set(auto) -> set(auto_limits). % 78.13/78.49 % set(auto_limits) -> assign(max_weight, "100.000"). % 78.13/78.49 % set(auto_limits) -> assign(sos_limit, 20000). % 78.13/78.49 % set(auto) -> set(auto_denials). % 78.13/78.49 % set(auto) -> set(auto_process). % 78.13/78.49 % set(auto2) -> assign(new_constants, 1). % 78.13/78.49 % set(auto2) -> assign(fold_denial_max, 3). % 78.13/78.49 % set(auto2) -> assign(max_weight, "200.000"). % 78.13/78.49 % set(auto2) -> assign(max_hours, 1). % 78.13/78.49 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 78.13/78.49 % set(auto2) -> assign(max_seconds, 0). % 78.13/78.49 % set(auto2) -> assign(max_minutes, 5). % 78.13/78.49 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 78.13/78.49 % set(auto2) -> set(sort_initial_sos). % 78.13/78.49 % set(auto2) -> assign(sos_limit, -1). % 78.13/78.49 % set(auto2) -> assign(lrs_ticks, 3000). % 78.13/78.49 % set(auto2) -> assign(max_megs, 400). % 78.13/78.49 % set(auto2) -> assign(stats, some). % 78.13/78.49 % set(auto2) -> clear(echo_input). % 78.13/78.49 % set(auto2) -> set(quiet). % 78.13/78.49 % set(auto2) -> clear(print_initial_clauses). % 78.13/78.49 % set(auto2) -> clear(print_given). % 78.13/78.49 assign(lrs_ticks,-1). % 78.13/78.49 assign(sos_limit,10000). % 78.13/78.49 assign(order,kbo). % 78.13/78.49 set(lex_order_vars). % 78.13/78.49 clear(print_given). % 78.13/78.49 % 78.13/78.49 % formulas(sos). % not echoed (92 formulas) % 78.13/78.49 % 78.13/78.49 ============================== end of input ========================== % 78.13/78.49 % 78.13/78.49 % From the command line: assign(max_seconds, 300). % 78.13/78.49 % 78.13/78.49 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 78.13/78.49 % 78.13/78.49 % Formulas that are not ordinary clauses: % 78.13/78.49 % 78.13/78.49 ============================== end of process non-clausal formulas === % 78.13/78.49 % 78.13/78.49 ============================== PROCESS INITIAL CLAUSES =============== % 78.13/78.49 % 78.13/78.49 ============================== PREDICATE ELIMINATION ================= % 78.13/78.49 % 78.13/78.49 ============================== end predicate elimination ============= % 78.13/78.49 % 78.13/78.49 Auto_denials: % 78.13/78.49 % copying label goal to answer in negative clause % 78.13/78.49 % 78.13/78.49 Term ordering decisions: % 78.13/78.49 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. prop1=1. aux=1. % 78.13/78.49 % 78.13/78.49 ============================== end of process initial clauses ======== % 78.13/78.49 % 78.13/78.49 ============================== CLAUSES FOR SEARCH ==================== % 78.13/78.49 % 78.13/78.49 ============================== end of clauses for search ============= % 78.13/78.49 % 78.13/78.49 ============================== SEARCH ================================ % 78.13/78.49 % 78.13/78.49 % Starting search at 0.02 seconds. % 78.13/78.49 % 78.13/78.49 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 388 (0.00 of 0.45 sec). % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=23.000, iters=4117 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=20.000, iters=3458 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=19.000, iters=3333 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=18.000, iters=3409 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=17.000, iters=3371 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=16.000, iters=3335 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=15.000, iters=3333 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=14.000, iters=3462 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=5054, wt=41.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4671, wt=38.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=2735, wt=37.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4880, wt=36.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4882, wt=35.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=5192, wt=34.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4974, wt=33.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4993, wt=32.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4994, wt=31.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=4562, wt=30.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=5067, wt=29.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=5072, wt=28.000 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=15386, wt=13.000 % 78.13/78.49 % 78.13/78.49 Low Water (keep): wt=13.000, iters=3333 % 78.13/78.49 % 78.13/78.49 Low Water (displace): id=75457, wt=12.000 % 182.53/182.84 % 182.53/182.84 ============================== STATISTICS ============================ % 182.53/182.84 % 182.53/182.84 Given=16198. Generated=3339701. Kept=298984. proofs=0. % 182.53/182.84 Usable=16042. Sos=10000. Demods=15591. Limbo=608, Disabled=272426. Hints=0. % 182.53/182.84 Kept_by_rule=0, Deleted_by_rule=0. % 182.53/182.84 Forward_subsumed=1326778. Back_subsumed=11. % 182.53/182.84 Sos_limit_deleted=1713939. Sos_displaced=271413. Sos_removed=0. % 182.53/182.84 New_demodulators=18487 (4 lex), Back_demodulated=910. Back_unit_deleted=0. % 182.53/182.84 Demod_attempts=76634411. Demod_rewrites=2250681. % 182.53/182.84 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. % 182.53/182.84 Nonunit_fsub_feature_tests=76. Nonunit_bsub_feature_tests=49. % 182.53/182.84 Megabytes=419.43. % 182.53/182.84 User_CPU=179.74, System_CPU=2.12, Wall_clock=182. % 182.53/182.84 % 182.53/182.84 Megs malloced by palloc(): 400. % 182.53/182.84 type (bytes each) gets frees in use bytes % 182.53/182.84 chunk ( 104) 1545 1545 0 0.0 K % 182.53/182.84 string_buf ( 8) 1544 1544 0 0.0 K % 182.53/182.84 token ( 20) 3403 3403 0 0.0 K % 182.53/182.84 pterm ( 16) 2198 2198 0 0.0 K % 182.53/182.84 hashtab ( 8) 0 0 0 0.0 K % 182.53/182.84 hashnode ( 8) 0 0 0 0.0 K % 182.53/182.84 term ( 20) 104881454 95990955 8890499 173642.6 K % 182.53/182.84 term arg arrays: 37280.2 K % 182.53/182.84 attribute ( 12) 1188323 908841 279482 3275.2 K % 182.53/182.84 ilist ( 8) 2481823697 2478437064 3386633 26458.1 K % 182.53/182.84 plist ( 8) 10033416 9644297 389119 3040.0 K % 182.53/182.84 i2list ( 12) 17754738 17754738 0 0.0 K % 182.53/182.84 just ( 12) 4895199 4586039 309160 3623.0 K % 182.53/182.84 parajust ( 16) 3323654 3026118 297536 4649.0 K % 182.53/182.84 instancejust ( 8) 0 0 0 0.0 K % 182.53/182.84 ivyjust ( 24) 0 0 0 0.0 K % 182.53/182.84 formula ( 28) 105 105 0 0.0 K % 182.53/182.84 formula arg arrays: 0.0 K % 182.53/182.84 topform ( 52) 3339793 3040717 299076 15187.5 K % 182.53/182.84 clist_pos ( 20) 904563 589896 314667 6145.8 K % 182.53/182.84 clist ( 16) 8 1 7 0.1 K % 182.53/182.84 context ( 808) 9645344 9645344 0 0.0 K % 182.53/182.84 trail ( 12) 11403222 11403222 0 0.0 K % 182.53/182.84 ac_match_pos (70044) 0 0 0 0.0 K % 182.53/182.84 ac_match_free_vars_pos (20020) % 182.53/182.84 0 0 0 0.0 K % 182.53/182.84 btm_state ( 60) 0 0 0 0.0 K % 182.53/182.84 btu_state ( 60) 0 0 0 0.0 K % 182.53/182.84 ac_position (285432) 0 0 0 0.0 K % 182.53/182.84 fpa_trie ( 20) 7299604 6241486 1058118 20666.4 K % 182.53/182.84 fpa_state ( 28) 3000859 3000859 0 0.0 K % 182.53/182.84 fpa_index ( 12) 10 0 10 0.1 K % 182.53/182.84 fpa_chunk ( 20) 7596524 7484032 112492 2197.1 K % 182.53/182.84 fpa_list ( 16) 6305133 0 6305133 98517.7 K % 182.53/182.84 fpa_list chunks: 7371.5 K % 182.53/182.84 discrim ( 12) 5497470 5197253 300217 3518.2 K % 182.53/182.84 discrim_pos ( 16) 2919157 2919157 0 0.0 K % 182.53/182.84 flat2 ( 32) 20640076 20640076 0 0.0 K % 182.53/182.84 flat ( 48) 0 0 0 0.0 K % 182.53/182.84 flatterm ( 32) 102651193 102651193 0 0.0 K % 182.53/182.84 mindex ( 28) 13 0 13 0.4 K % 182.53/182.84 mindex_pos ( 56) 1530907 1530907 0 0.0 K % 182.53/182.84 lindex ( 12) 5 0 5 0.1 K % 182.53/182.84 clash ( 40) 36993 36993 0 0.0 K % 182.53/182.84 di_tree ( 12) 1023 116 907 10.6 K % 182.53/182.84 avl_node ( 20) 596655 576655 20000 390.6 K % 182.53/182.84 % 182.53/182.84 Memory report, 20 @ 20 = 400 megs (400.00 megs used). % 182.53/182.84 List 1, length 5, 0.0 K % 182.53/182.84 List 2, length 660, 5.2 K % 182.53/182.84 List 3, length 9325, 109.3 K % 182.53/182.84 List 5, length 9, 0.2 K % 182.53/182.84 List 6, length 17, 0.4 K % 182.53/182.84 List 7, length 22, 0.6 K % 182.53/182.84 List 8, length 85, 2.7 K % 182.53/182.84 List 10, length 2, 0.1 K % 182.53/182.84 List 13, length 1, 0.1 K % 182.53/182.84 List 14, length 2, 0.1 K % 182.53/182.84 List 16, length 189, 11.8 K % 182.53/182.84 List 26, length 28, 2.8 K % 182.53/182.84 List 32, length 229, 28.6 K % 182.53/182.84 List 64, length 2, 0.5 K % 182.53/182.84 List 128, length 239, 119.5 K % 182.53/182.84 List 202, length 4, 3.2 K % 182.53/182.84 % 182.53/182.84 ============================== SELECTOR REPORT ======================= % 182.53/182.84 Sos_deleted=1713939, Sos_displaced=271413, Sos_size=10000 % 182.53/182.84 SELECTOR PART PRIORITY ORDER SIZE SELECTED % 182.53/182.84 I 2147483647 high age 0 89 % 182.53/182.84 H 1 high weight 0 0 % 182.53/182.84 A 1 low age 10000 1832 % 182.53/182.84 F 4 low weight 2604 6953 % 182.53/182.84 T 4 low weight 7396 7324 % 182.53/182.84 ============================== end of selector report ================ % 182.53/182.84 % 182.53/182.84 ============================== end of statistics ===================== % 182.53/182.84 % 182.53/182.84 Exiting with failure. % 182.53/182.84 % 182.53/182.84 Process 23440 exit (max_megs) Tue Apr 28 23:44:08 2026 % 182.53/182.84 Prover9 interrupted %------------------------------------------------------------------------------