%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NUM923+5 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n021.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 : 600s
% DateTime : Mon Jul 18 14:23:05 EDT 2022
% Result : Unknown 0.20s 0.53s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM923+5 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n021.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Wed Jul 6 01:34:48 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.20/0.38 ----- Otter 3.2, August 2001 -----
% 0.20/0.38 The process was started by sandbox2 on n021.cluster.edu,
% 0.20/0.38 Wed Jul 6 01:34:48 2022
% 0.20/0.38 The command was "./sos". The process ID is 14655.
% 0.20/0.38
% 0.20/0.38 set(prolog_style_variables).
% 0.20/0.38 set(auto).
% 0.20/0.38 dependent: set(auto1).
% 0.20/0.38 dependent: set(process_input).
% 0.20/0.38 dependent: clear(print_kept).
% 0.20/0.38 dependent: clear(print_new_demod).
% 0.20/0.38 dependent: clear(print_back_demod).
% 0.20/0.38 dependent: clear(print_back_sub).
% 0.20/0.38 dependent: set(control_memory).
% 0.20/0.38 dependent: assign(max_mem, 12000).
% 0.20/0.38 dependent: assign(pick_given_ratio, 4).
% 0.20/0.38 dependent: assign(stats_level, 1).
% 0.20/0.38 dependent: assign(pick_semantic_ratio, 3).
% 0.20/0.38 dependent: assign(sos_limit, 5000).
% 0.20/0.38 dependent: assign(max_weight, 60).
% 0.20/0.38 clear(print_given).
% 0.20/0.38
% 0.20/0.38 formula_list(usable).
% 0.20/0.38
% 0.20/0.38 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4.
% 0.20/0.38
% 0.20/0.38 This ia a non-Horn set with equality. The strategy will be
% 0.20/0.38 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.20/0.38 unit deletion, with positive clauses in sos and nonpositive
% 0.20/0.38 clauses in usable.
% 0.20/0.38
% 0.20/0.38 dependent: set(knuth_bendix).
% 0.20/0.38 dependent: set(para_from).
% 0.20/0.38 dependent: set(para_into).
% 0.20/0.38 dependent: clear(para_from_right).
% 0.20/0.38 dependent: clear(para_into_right).
% 0.20/0.38 dependent: set(para_from_vars).
% 0.20/0.38 dependent: set(eq_units_both_ways).
% 0.20/0.38 dependent: set(dynamic_demod_all).
% 0.20/0.38 dependent: set(dynamic_demod).
% 0.20/0.38 dependent: set(order_eq).
% 0.20/0.38 dependent: set(back_demod).
% 0.20/0.38 dependent: set(lrpo).
% 0.20/0.38 dependent: set(hyper_res).
% 0.20/0.38 dependent: set(unit_deletion).
% 0.20/0.38 dependent: set(factor).
% 0.20/0.38
% 0.20/0.38 ------------> process usable:
% 0.20/0.38 Following clause subsumed by 22 during input processing: 0 [] {-} -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)|ti(A,B)=ti(A,D).
% 0.20/0.38 Following clause subsumed by 24 during input processing: 0 [] {-} -cancel_semigroup_add(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)|ti(A,C)=ti(A,D).
% 0.20/0.38 Following clause subsumed by 32 during input processing: 0 [] {-} -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)).
% 0.20/0.38 Following clause subsumed by 35 during input processing: 0 [flip.2] {-} -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)).
% 0.20/0.38 Following clause subsumed by 36 during input processing: 0 [] {-} -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)).
% 0.20/0.38 Following clause subsumed by 38 during input processing: 0 [flip.2] {-} -real_normed_algebra(A)|hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),C),D)).
% 0.20/0.38 Following clause subsumed by 41 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)=ti(A,C)|ti(A,D)=ti(A,E)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),E))!=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)).
% 0.20/0.38 Following clause subsumed by 42 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),D)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),E))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),E)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)).
% 0.20/0.39 Following clause subsumed by 43 during input processing: 0 [] {-} -semiri456707255roduct(A)|ti(A,B)!=ti(A,C)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),B)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),C))=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),E),B)).
% 0.20/0.39 Following clause subsumed by 48 during input processing: 0 [] {-} -minus(A)|hAPP(B,A,hAPP(fun(B,A),fun(B,A),hAPP(fun(B,A),fun(fun(B,A),fun(B,A)),minus_minus(fun(B,A)),C),D),E)=hAPP(A,A,hAPP(A,fun(A,A),minus_minus(A),hAPP(B,A,C,E)),hAPP(B,A,D,E)).
% 0.20/0.39 Following clause subsumed by 49 during input processing: 0 [] {-} hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)!=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(B,C)=ti(B,E).
% 0.20/0.39 Following clause subsumed by 50 during input processing: 0 [] {-} hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),C),D)!=hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),E),F)|ti(A,D)=ti(A,F).
% 0.20/0.39 Following clause subsumed by 52 during input processing: 0 [] {-} -ab_sem1668676832m_mult(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),B)=ti(A,B).
% 0.20/0.39 Following clause subsumed by 57 during input processing: 0 [] {-} -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),D)).
% 0.20/0.39 Following clause subsumed by 57 during input processing: 0 [] {-} -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),C),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))).
% 0.20/0.39 Following clause subsumed by 55 during input processing: 0 [] {-} -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),E))=hAPP(A,A,hAPP(A,fun(A,A),times_times(A),D),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),hAPP(A,A,hAPP(A,fun(A,A),times_times(A),B),C)),E)).
% 0.20/0.39 Following clause subsumed by 63 during input processing: 0 [] {-} -comm_semiring_1(A)|hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),D)=hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),C),D)).
% 0.20/0.39 Following clause subsumed by 76 during input processing: 0 [] {-} -hBOOL(hAPP(A,bool,hAPP(B,fun(A,bool),hAPP(fun(product_prod(B,A),bool),fun(B,fun(A,bool)),product_curry(B,A,bool),C),D),E))|hBOOL(hAPP(product_prod(B,A),bool,C,hAPP(A,product_prod(B,A),hAPP(B,fun(A,product_prod(B,A)),product_Pair(B,A),D),E))).
% 0.20/0.39 Following clause subsumed by 84 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),D)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),C),D)).
% 0.20/0.39 Following clause subsumed by 85 during input processing: 0 [] {-} -ordere236663937imp_le(A)| -hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),B),C)),hAPP(A,A,hAPP(A,fun(A,A),plus_plus(A),D),C)))|hBOOL(hAPP(A,bool,hAPP(A,fun(A,bool),ord_less_eq(A),B),D)).
% 0.20/0.39
% 0.20/0.39 ------------> process sos:
% 0.20/0.39 Following clause subsumed by 145 during input processing: 0 [copy,145,flip.1] {-} hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)=hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),A).
% 0.20/0.39 Following clause subsumed by 148 during input processing: 0 [copy,148,flip.1] {-} hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),C))=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),C)).
% 0.20/0.39 Following clause subsumed by 149 during input processing: 0 [copy,149,flip.1] {-} hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),B),A).
% 0.20/0.39 Following clause subsumed by 194 during input processing: 0 [copy,194,flip.1] {-} A=A.
% 0.20/0.39 194 back subsumes 105.
% 0.20/0.39 Following clause subsumed by 134 during input processing: 0 [copy,195,flip.1] {-} hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C))),D)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),E),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),F))),G))=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),D)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),E),G))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),C),D)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),F),G)))).
% 0.20/0.39 Following clause subsumed by 138 during input processing: 0 [copy,196,flip.1] {-} hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C)).
% 0.20/0.39 Following clause subsumed by 142 during input processing: 0 [copy,197,flip.1] {-} hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)),C)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),C)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),C)).
% 0.20/0.39 Following clause subsumed by 167 during input processing: 0 [copy,198,flip.1] {-} hAPP(A,B,hAPP(C,fun(A,B),hAPP(fun(product_prod(C,A),B),fun(C,fun(A,B)),product_curry(C,A,B),D),E),F)=hAPP(product_prod(C,A),B,D,hAPP(A,product_prod(C,A),hAPP(C,fun(A,product_prod(C,A)),product_Pair(C,A),E),F)).
% 0.20/0.39
% 0.20/0.39 ======= end of input processing =======
% 0.20/0.52
% 0.20/0.52
% 0.20/0.52 Failed to model usable list: disabling FINDER
% 0.20/0.52
% 0.20/0.52
% 0.20/0.52
% 0.20/0.52 -------------- Softie stats --------------
% 0.20/0.52
% 0.20/0.52 UPDATE_STOP: 300
% 0.20/0.52 SFINDER_TIME_LIMIT: 2
% 0.20/0.52 SHORT_CLAUSE_CUTOFF: 4
% 0.20/0.52 number of clauses in intial UL: 95
% 0.20/0.52 number of clauses initially in problem: 177
% 0.20/0.52 percentage of clauses intially in UL: 53
% 0.20/0.52 percentage of distinct symbols occuring in initial UL: 80
% 0.20/0.52 percent of all initial clauses that are short: 98
% 0.20/0.52 absolute distinct symbol count: 86
% 0.20/0.52 distinct predicate count: 23
% 0.20/0.52 distinct function count: 55
% 0.20/0.52 distinct constant count: 8
% 0.20/0.52
% 0.20/0.52 ---------- no more Softie stats ----------
% 0.20/0.52
% 0.20/0.52
% 0.20/0.52
% 0.20/0.52 =========== start of search ===========
% 0.20/0.52
% 0.20/0.52
% 0.20/0.52 Changing weight limit from 60 to 101.
% 0.20/0.52
% 0.20/0.52 Resetting weight limit to 101 after 5 givens.
% 0.20/0.52
% 0.20/0.53 ti(int,A)=hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),A),B)),B).
% 0.20/0.53
% 0.20/0.53 ------------- memory usage ------------
% 0.20/0.53 79 mallocs of 32700 bytes each, 2522.8 K.
% 0.20/0.53 type (bytes each) gets frees in use avail bytes
% 0.20/0.53 sym_ent ( 304) 272 0 272 0 80.8 K
% 0.20/0.53 term ( 32) 137004 128589 8415 181 268.6 K
% 0.20/0.53 rel ( 40) 127367 116142 11225 37 439.9 K
% 0.20/0.53 term_ptr ( 16) 53650 1630 52020 81 814.1 K
% 0.20/0.53 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 0.20/0.53 fpa_head ( 24) 9377 310 9067 0 212.5 K
% 0.20/0.53 fpa_tree ( 56) 9516 9516 0 183 10.0 K
% 0.20/0.53 context (1288) 3434 3434 0 5 6.3 K
% 0.20/0.53 trail ( 24) 2903 2903 0 7 0.2 K
% 0.20/0.53 imd_tree ( 32) 340 16 324 0 10.1 K
% 0.20/0.53 imd_pos (4024) 11376 11376 0 9 35.4 K
% 0.20/0.53 is_tree ( 24) 7363 586 6777 35 159.7 K
% 0.20/0.53 is_pos (2424) 32960 32960 0 58 137.3 K
% 0.20/0.53 fsub_pos ( 16) 1617 1617 0 1 0.0 K
% 0.20/0.53 literal ( 32) 2029 997 1032 1 32.3 K
% 0.20/0.53 clause ( 88) 918 386 532 1 45.8 K
% 0.20/0.53 list ( 272) 159 152 7 2 2.4 K
% 0.20/0.53 clash_nd ( 80) 61 61 0 2 0.2 K
% 0.20/0.53 clause_ptr ( 16) 492 87 405 4 6.4 K
% 0.20/0.53 int_ptr ( 16) 4102 2318 1784 8 28.0 K
% 0.20/0.53 ci_ptr ( 24) 0 0 0 0 0.0 K
% 0.20/0.53 link_node ( 120) 0 0 0 0 0.0 K
% 0.20/0.53 ans_lit_node( 24) 0 0 0 0 0.0 K
% 0.20/0.53 formula_box( 168) 0 0 0 0 0.0 K
% 0.20/0.53 formula( 40) 1248 1248 0 916 35.8 K
% 0.20/0.53 formula_ptr( 16) 149 149 0 149 2.3 K
% 0.20/0.53 cl_attribute( 24) 0 0 0 0 0.0 K
% 0.20/0.53
% 0.20/0.53 ********** is_delete, can't find end.
% 0.20/0.53 0
% 0.20/0.53 post_process time 0.00
% 0.20/0.53 back demod time 0.00
% 0.20/0.53 back subsume 0.00
% 0.20/0.53 factor time 0.00
% 0.20/0.53 FINDER time 0.00
% 0.20/0.53 unindex time 0.00
% 0.20/0.53
% 0.20/0.53 Forward subsumption counts, subsumer:number_subsumed.
% 0.20/0.53 1:0 2:0 3:0 4:0 5:0 6:0 7:0 8:0 9:0 10:0
% 0.20/0.53 11:0 12:0 13:0 14:0 15:0 16:0 17:0 18:0 19:0 20:0
% 0.20/0.53 21:0 22:1 23:0 24:1 25:0 26:0 27:0 28:0 29:0 30:0
% 0.20/0.53 31:0 32:1 33:0 34:0 35:1 36:1 37:0 38:1 39:0 40:0
% 0.20/0.53 41:1 42:1 43:1 44:0 45:0 46:0 47:0 48:1 49:1 50:1
% 0.20/0.53 51:0 52:1 53:0 54:0 55:1 56:0 57:2 58:0 59:0 60:0
% 0.20/0.53 61:0 62:0 63:1 64:0 65:0 66:0 67:0 68:0 69:0 70:0
% 0.20/0.53 71:0 72:0 73:0 74:0 75:0 76:1 77:0 78:0 79:0 80:0
% 0.20/0.53 81:0 82:0 83:0 84:1 85:1 86:0 87:0 88:0 89:0 90:0
% 0.20/0.53 91:0 92:0 93:0 94:6 95:0 96:0 97:0 98:0 99:0
% 0.20/0.53 All others: 131.
% 0.20/0.53
% 0.20/0.53 ********** ABNORMAL END **********
% 0.20/0.53
% 0.20/0.53 ********** is_delete, can't find end.
%------------------------------------------------------------------------------