%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SCT170+1 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n011.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 22:12:29 EDT 2022
% Result : Unknown 0.67s 0.90s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SCT170+1 : TPTP v8.1.0. Released v5.3.0.
% 0.06/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n011.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 : Sat Jul 2 08:05:34 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.46 ----- Otter 3.2, August 2001 -----
% 0.19/0.46 The process was started by sandbox on n011.cluster.edu,
% 0.19/0.46 Sat Jul 2 08:05:34 2022
% 0.19/0.46 The command was "./sos". The process ID is 20540.
% 0.19/0.46
% 0.19/0.46 set(prolog_style_variables).
% 0.19/0.46 set(auto).
% 0.19/0.46 dependent: set(auto1).
% 0.19/0.46 dependent: set(process_input).
% 0.19/0.46 dependent: clear(print_kept).
% 0.19/0.46 dependent: clear(print_new_demod).
% 0.19/0.46 dependent: clear(print_back_demod).
% 0.19/0.46 dependent: clear(print_back_sub).
% 0.19/0.46 dependent: set(control_memory).
% 0.19/0.46 dependent: assign(max_mem, 12000).
% 0.19/0.46 dependent: assign(pick_given_ratio, 4).
% 0.19/0.46 dependent: assign(stats_level, 1).
% 0.19/0.46 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.46 dependent: assign(sos_limit, 5000).
% 0.19/0.46 dependent: assign(max_weight, 60).
% 0.19/0.46 clear(print_given).
% 0.19/0.46
% 0.19/0.46 formula_list(usable).
% 0.19/0.46
% 0.19/0.46 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=14.
% 0.19/0.46
% 0.19/0.46 This ia a non-Horn set with equality. The strategy will be
% 0.19/0.46 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.19/0.46 unit deletion, with positive clauses in sos and nonpositive
% 0.19/0.46 clauses in usable.
% 0.19/0.46
% 0.19/0.46 dependent: set(knuth_bendix).
% 0.19/0.46 dependent: set(para_from).
% 0.19/0.46 dependent: set(para_into).
% 0.19/0.46 dependent: clear(para_from_right).
% 0.19/0.46 dependent: clear(para_into_right).
% 0.19/0.46 dependent: set(para_from_vars).
% 0.19/0.46 dependent: set(eq_units_both_ways).
% 0.19/0.46 dependent: set(dynamic_demod_all).
% 0.19/0.46 dependent: set(dynamic_demod).
% 0.19/0.46 dependent: set(order_eq).
% 0.19/0.46 dependent: set(back_demod).
% 0.19/0.46 dependent: set(lrpo).
% 0.19/0.46 dependent: set(hyper_res).
% 0.19/0.46 dependent: set(unit_deletion).
% 0.19/0.46 dependent: set(factor).
% 0.19/0.46
% 0.19/0.46 ------------> process usable:
% 0.19/0.46 Following clause subsumed by 74 during input processing: 0 [] {-} -is_Arr553848933le_alt(A)| -is_Arr553848933le_alt(B)| -is_Arr553848933le_alt(C)| -is_Arr553848933le_alt(D)|produc171383831le_alt(A,B)!=produc171383831le_alt(C,D)|A=C.
% 0.19/0.46 Following clause subsumed by 75 during input processing: 0 [] {-} -is_Arr553848933le_alt(A)| -is_Arr553848933le_alt(B)| -is_Arr553848933le_alt(C)| -is_Arr553848933le_alt(D)|produc171383831le_alt(A,B)!=produc171383831le_alt(C,D)|B=D.
% 0.19/0.46 Following clause subsumed by 89 during input processing: 0 [] {-} -is_Arr553848933le_alt(A)| -is_Arr553848933le_alt(B)| -hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(C),arrow_1239002508le_Lin))|A=B| -hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(produc171383831le_alt(A,B)),C))| -hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(produc171383831le_alt(B,A)),C)).
% 0.19/0.46 Following clause subsumed by 125 during input processing: 0 [flip.1] {-} cons_A2055670914le_alt(B,A)!=A.
% 0.19/0.46 Following clause subsumed by 121 during input processing: 0 [] {-} cons_A2055670914le_alt(A,B)!=nil_Ar965638354le_alt.
% 0.19/0.46 Following clause subsumed by 133 during input processing: 0 [] {-} -hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(A),pi_Pro2135156861t_bool(B,C)))| -hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(D),B))|hBOOL(hAPP_f387058535l_bool(member_bool(hAPP_P2075002375t_bool(A,D)),hAPP_P2127852789l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 141 during input processing: 0 [] {-} -hBOOL(hAPP_f460310451l_bool(member765089840e_indi(A),pi_Pro437273841e_indi(B,C)))| -hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(D),B))|hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(hAPP_P2024088443e_indi(A,D)),hAPP_P907763049i_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 142 during input processing: 0 [] {-} -hBOOL(hAPP_f234874197l_bool(member1105181906e_indi(A),pi_fun1736243859e_indi(B,C)))| -hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(D),B))|hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(hAPP_f1818473245e_indi(A,D)),hAPP_f749892423i_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 143 during input processing: 0 [] {-} -hBOOL(hAPP_f500145249l_bool(member1661336414l_bool(A),pi_fun1494794527l_bool(B,C)))| -hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(D),B))|hBOOL(hAPP_f387058535l_bool(member_bool(hAPP_f1636546729l_bool(A,D)),hAPP_f313042899l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 144 during input processing: 0 [] {-} -hBOOL(hAPP_f592909149l_bool(member329987264e_indi(A),pi_fun972956463e_indi(B,C)))| -hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(D),B))|hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(hAPP_f1659504677e_indi(A,D)),hAPP_f352490559i_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 145 during input processing: 0 [] {-} -hBOOL(hAPP_f526292585l_bool(member1033316428l_bool(A),pi_fun1727820731l_bool(B,C)))| -hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(D),B))|hBOOL(hAPP_f387058535l_bool(member_bool(hAPP_f745298353l_bool(A,D)),hAPP_f417299659l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 146 during input processing: 0 [] {-} -hBOOL(hAPP_f1766869725l_bool(member1122398042e_indi(A),pi_fun2075749915e_indi(B,C)))| -hBOOL(hAPP_f213304539l_bool(member1622429502t_bool(D),B))|hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(hAPP_f618619045e_indi(A,D)),hAPP_f355113919i_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 147 during input processing: 0 [] {-} -hBOOL(hAPP_f1279200745l_bool(member387398118l_bool(A),pi_fun525942951l_bool(B,C)))| -hBOOL(hAPP_f213304539l_bool(member1622429502t_bool(D),B))|hBOOL(hAPP_f387058535l_bool(member_bool(hAPP_f785543729l_bool(A,D)),hAPP_f497468491l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 134 during input processing: 0 [] {-} -hBOOL(hAPP_f483434675l_bool(member859582768le_alt(A),pi_Arr149813489le_alt(B,C)))| -hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(D),B))|hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(hAPP_A1736628091le_alt(A,D)),hAPP_A1374816149t_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 135 during input processing: 0 [] {-} -hBOOL(hAPP_f1895985727l_bool(member42699324le_alt(A),pi_boo1877522301le_alt(B,C)))| -hBOOL(hAPP_f387058535l_bool(member_bool(D),B))|hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(hAPP_b1817367815le_alt(A,D)),hAPP_b1024867081t_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 136 during input processing: 0 [] {-} -hBOOL(hAPP_f204273237l_bool(member1833291218t_bool(A),pi_Arr1511953043t_bool(B,C)))| -hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(D),B))|hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(hAPP_A1594182429t_bool(A,D)),hAPP_A1912483895l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 137 during input processing: 0 [] {-} -hBOOL(hAPP_f1018082273l_bool(member1911067358t_bool(A),pi_boo691944735t_bool(B,C)))| -hBOOL(hAPP_f387058535l_bool(member_bool(D),B))|hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(hAPP_b833696937t_bool(A,D)),hAPP_b1719629739l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 138 during input processing: 0 [] {-} -hBOOL(hAPP_f1550037191l_bool(member497701034t_bool(A),pi_boo2007389459t_bool(B,C)))| -hBOOL(hAPP_f387058535l_bool(member_bool(D),B))|hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(hAPP_b1024867081t_bool(A,D)),hAPP_b1965422783l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 139 during input processing: 0 [] {-} -hBOOL(hAPP_f1012384989l_bool(member1467476314t_bool(A),pi_Arr372473371t_bool(B,C)))| -hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(D),B))|hBOOL(hAPP_f213304539l_bool(member1622429502t_bool(hAPP_A1062826149t_bool(A,D)),hAPP_A1964572607l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 140 during input processing: 0 [] {-} -hBOOL(hAPP_f1271180905l_bool(member2081512038t_bool(A),pi_boo71521447t_bool(B,C)))| -hBOOL(hAPP_f387058535l_bool(member_bool(D),B))|hBOOL(hAPP_f213304539l_bool(member1622429502t_bool(hAPP_b331122225t_bool(A,D)),hAPP_b990649139l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 148 during input processing: 0 [] {-} -hBOOL(hAPP_f213304539l_bool(member1622429502t_bool(A),pi_fun433100839t_bool(B,C)))| -hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(D),B))|hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(hAPP_f695124765t_bool(A,D)),hAPP_f861484971l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 149 during input processing: 0 [] {-} -hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(A),pi_Arr688267935t_bool(B,C)))| -hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(D),B))|hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(hAPP_A1374816149t_bool(A,D)),hAPP_A1944296755l_bool(C,D))).
% 0.19/0.46 Following clause subsumed by 277 during input processing: 0 [] {-} -hBOOL(hAPP_P2075002375t_bool(A,produc171383831le_alt(B,C)))|hBOOL(produc362057470t_bool(A,B,C)).
% 0.67/0.89 Following clause subsumed by 276 during input processing: 0 [] {-} -hBOOL(produc362057470t_bool(A,B,C))|hBOOL(hAPP_P2075002375t_bool(A,produc171383831le_alt(B,C))).
% 0.67/0.89 Following clause subsumed by 276 during input processing: 0 [] {-} -hBOOL(produc362057470t_bool(A,B,C))|hBOOL(hAPP_P2075002375t_bool(A,produc171383831le_alt(B,C))).
% 0.67/0.89 Following clause subsumed by 276 during input processing: 0 [] {-} -hBOOL(produc362057470t_bool(A,B,C))|hBOOL(hAPP_P2075002375t_bool(A,produc171383831le_alt(B,C))).
% 0.67/0.89 Following clause subsumed by 277 during input processing: 0 [] {-} hBOOL(produc362057470t_bool(A,B,C))| -hBOOL(hAPP_P2075002375t_bool(A,produc171383831le_alt(B,C))).
% 0.67/0.89 Following clause subsumed by 279 during input processing: 0 [] {-} -hBOOL(hAPP_l1656811191t_bool(null_A1200409306le_alt,A))|A=nil_Ar965638354le_alt.
% 0.67/0.89 Following clause subsumed by 278 during input processing: 0 [] {-} hBOOL(hAPP_l1656811191t_bool(null_A1200409306le_alt,A))|A!=nil_Ar965638354le_alt.
% 0.67/0.89 360 back subsumes 356.
% 0.67/0.89 404 back subsumes 401.
% 0.67/0.89 404 back subsumes 397.
% 0.67/0.89 404 back subsumes 385.
% 0.67/0.89 414 back subsumes 387.
% 0.67/0.89 416 back subsumes 389.
% 0.67/0.89 422 back subsumes 418.
% 0.67/0.89 422 back subsumes 398.
% 0.67/0.89 423 back subsumes 419.
% 0.67/0.89 423 back subsumes 399.
% 0.67/0.89
% 0.67/0.89 ------------> process sos:
% 0.67/0.89 Following clause subsumed by 762 during input processing: 0 [] {-} hBOOL(hAPP_f387058535l_bool(member_bool(A),top_to1647826457l_bool)).
% 0.67/0.89 Following clause subsumed by 763 during input processing: 0 [] {-} hBOOL(hAPP_f919661787l_bool(member2074804542e_indi(A),top_to1256827021i_bool)).
% 0.67/0.89 Following clause subsumed by 764 during input processing: 0 [] {-} hBOOL(hAPP_f745298353l_bool(member1056080916le_alt(A),top_to2034604131t_bool)).
% 0.67/0.89 Following clause subsumed by 765 during input processing: 0 [] {-} hBOOL(hAPP_f453661011l_bool(member1277417654t_bool(A),top_to1194196741l_bool)).
% 0.67/0.89 Following clause subsumed by 766 during input processing: 0 [] {-} hBOOL(hAPP_f503012287l_bool(member1965683644t_bool(A),top_to2005687013l_bool)).
% 0.67/0.89 Following clause subsumed by 767 during input processing: 0 [] {-} hBOOL(hAPP_f213304539l_bool(member1622429502t_bool(A),top_to40512653l_bool)).
% 0.67/0.89 751 back subsumes 286.
% 0.67/0.89 752 back subsumes 288.
% 0.67/0.89 753 back subsumes 290.
% 0.67/0.89 754 back subsumes 292.
% 0.67/0.89 755 back subsumes 294.
% 0.67/0.89 Following clause subsumed by 794 during input processing: 0 [copy,794,flip.1] {-} A=A.
% 0.67/0.89 794 back subsumes 579.
% 0.67/0.89 794 back subsumes 578.
% 0.67/0.89 794 back subsumes 577.
% 0.67/0.89 794 back subsumes 576.
% 0.67/0.89 794 back subsumes 575.
% 0.67/0.89 794 back subsumes 574.
% 0.67/0.89 794 back subsumes 573.
% 0.67/0.89 794 back subsumes 572.
% 0.67/0.89 794 back subsumes 571.
% 0.67/0.89 794 back subsumes 570.
% 0.67/0.89 794 back subsumes 567.
% 0.67/0.89 794 back subsumes 566.
% 0.67/0.89 794 back subsumes 564.
% 0.67/0.89 794 back subsumes 563.
% 0.67/0.89 794 back subsumes 558.
% 0.67/0.89 794 back subsumes 557.
% 0.67/0.89 794 back subsumes 553.
% 0.67/0.89 794 back subsumes 551.
% 0.67/0.89 794 back subsumes 549.
% 0.67/0.89 794 back subsumes 545.
% 0.67/0.89 794 back subsumes 544.
% 0.67/0.89 794 back subsumes 541.
% 0.67/0.89 794 back subsumes 540.
% 0.67/0.89 794 back subsumes 539.
% 0.67/0.89 794 back subsumes 538.
% 0.67/0.89 794 back subsumes 537.
% 0.67/0.89 794 back subsumes 533.
% 0.67/0.89 794 back subsumes 531.
% 0.67/0.89 794 back subsumes 529.
% 0.67/0.89 794 back subsumes 528.
% 0.67/0.89 794 back subsumes 525.
% 0.67/0.89 794 back subsumes 524.
% 0.67/0.89 794 back subsumes 523.
% 0.67/0.89 794 back subsumes 517.
% 0.67/0.89 794 back subsumes 516.
% 0.67/0.89 794 back subsumes 515.
% 0.67/0.89 794 back subsumes 514.
% 0.67/0.89 794 back subsumes 513.
% 0.67/0.89 794 back subsumes 509.
% 0.67/0.89 794 back subsumes 508.
% 0.67/0.89 794 back subsumes 506.
% 0.67/0.89 794 back subsumes 503.
% 0.67/0.89 794 back subsumes 501.
% 0.67/0.89 794 back subsumes 499.
% 0.67/0.89 794 back subsumes 497.
% 0.67/0.89 794 back subsumes 496.
% 0.67/0.89 794 back subsumes 494.
% 0.67/0.89 794 back subsumes 493.
% 0.67/0.89 794 back subsumes 491.
% 0.67/0.89 794 back subsumes 488.
% 0.67/0.89 794 back subsumes 484.
% 0.67/0.89 794 back subsumes 482.
% 0.67/0.89 794 back subsumes 481.
% 0.67/0.89 794 back subsumes 480.
% 0.67/0.89 794 back subsumes 478.
% 0.67/0.89 794 back subsumes 476.
% 0.67/0.89 794 back subsumes 475.
% 0.67/0.89 794 back subsumes 473.
% 0.67/0.89 794 back subsumes 470.
% 0.67/0.89 794 back subsumes 468.
% 0.67/0.89 794 back subsumes 467.
% 0.67/0.89 794 back subsumes 463.
% 0.67/0.89 794 back subsumes 457.
% 0.67/0.89 794 back subsumes 456.
% 0.67/0.89 794 back subsumes 455.
% 0.67/0.89 794 back subsumes 453.
% 0.67/0.89 794 back subsumes 452.
% 0.67/0.89 794 back subsumes 451.
% 0.67/0.89 794 back subsumes 449.
% 0.67/0.89 794 back subsumes 440.
% 0.67/0.89 794 back subsumes 431.
% 0.67/0.89 794 back subsumes 427.
% 0.67/0.89 794 back subsumes 425.
% 0.67/0.89 794 back subsumes 420.
% 0.67/0.89 794 back subsumes 416.
% 0.67/0.89 794 back subsumes 415.
% 0.67/0.89 794 back subsumes 412.
% 0.67/0.89 794 back subsumes 410.
% 0.67/0.90 794 back subsumes 406.
% 0.67/0.90 794 back subsumes 405.
% 0.67/0.90 794 back subsumes 402.
% 0.67/0.90 794 back subsumes 391.
% 0.67/0.90 794 back subsumes 390.
% 0.67/0.90 794 back subsumes 388.
% 0.67/0.90 794 back subsumes 386.
% 0.67/0.90 794 back subsumes 384.
% 0.67/0.90 794 back subsumes 383.
% 0.67/0.90 794 back subsumes 382.
% 0.67/0.90 794 back subsumes 381.
% 0.67/0.90 794 back subsumes 379.
% 0.67/0.90 794 back subsumes 377.
% 0.67/0.90 794 back subsumes 375.
% 0.67/0.90 794 back subsumes 372.
% 0.67/0.90 794 back subsumes 366.
% 0.67/0.90 794 back subsumes 359.
% 0.67/0.90 794 back subsumes 357.
% 0.67/0.90 794 back subsumes 355.
% 0.67/0.90 794 back subsumes 353.
% 0.67/0.90 794 back subsumes 345.
% 0.67/0.90 794 back subsumes 342.
% 0.67/0.90 794 back subsumes 341.
% 0.67/0.90 794 back subsumes 338.
% 0.67/0.90
% 0.67/0.90 ======= end of input processing =======
% 0.67/0.90
% 0.67/0.90 SEGMENTATION FAULT!! This is probably caused by a
% 0.67/0.90 bug in Otter. Please send copy of the input file to
% 0.67/0.90 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.67/0.90 using, and send any other info that might be useful.
% 0.67/0.90
% 0.67/0.90
% 0.67/0.90 SEGMENTATION FAULT!! This is probably caused by a
% 0.67/0.90 bug in Otter. Please send copy of the input file to
% 0.67/0.90 otter@mcs.anl.gov, let us know what version of Otter you are
% 0.67/0.90 using, and send any other info that might be useful.
% 0.67/0.90
% 0.67/0.90
% 0.67/0.90 The job finished Sat Jul 2 08:05:35 2022
%------------------------------------------------------------------------------