%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : ALG180+1 : TPTP v8.1.0. Released v2.7.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 : Thu Jul 14 18:01:12 EDT 2022
% Result : Theorem 156.77s 156.94s
% Output : Refutation 156.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG180+1 : TPTP v8.1.0. Released v2.7.0.
% 0.06/0.13 % Command : sos-script %s
% 0.14/0.35 % Computer : n021.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Tue Jun 7 22:05:36 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.14/0.38 ----- Otter 3.2, August 2001 -----
% 0.14/0.38 The process was started by sandbox2 on n021.cluster.edu,
% 0.14/0.38 Tue Jun 7 22:05:36 2022
% 0.14/0.38 The command was "./sos". The process ID is 21131.
% 0.14/0.38
% 0.14/0.38 set(prolog_style_variables).
% 0.14/0.38 set(auto).
% 0.14/0.38 dependent: set(auto1).
% 0.14/0.38 dependent: set(process_input).
% 0.14/0.38 dependent: clear(print_kept).
% 0.14/0.38 dependent: clear(print_new_demod).
% 0.14/0.38 dependent: clear(print_back_demod).
% 0.14/0.38 dependent: clear(print_back_sub).
% 0.14/0.38 dependent: set(control_memory).
% 0.14/0.38 dependent: assign(max_mem, 12000).
% 0.14/0.38 dependent: assign(pick_given_ratio, 4).
% 0.14/0.38 dependent: assign(stats_level, 1).
% 0.14/0.38 dependent: assign(pick_semantic_ratio, 3).
% 0.14/0.38 dependent: assign(sos_limit, 5000).
% 0.14/0.38 dependent: assign(max_weight, 60).
% 0.14/0.38 clear(print_given).
% 0.14/0.38
% 0.14/0.38 formula_list(usable).
% 0.14/0.38
% 0.14/0.38 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5.
% 0.14/0.38
% 0.14/0.38 This ia a non-Horn set with equality. The strategy will be
% 0.14/0.38 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.14/0.38 unit deletion, with positive clauses in sos and nonpositive
% 0.14/0.38 clauses in usable.
% 0.14/0.38
% 0.14/0.38 dependent: set(knuth_bendix).
% 0.14/0.38 dependent: set(para_from).
% 0.14/0.38 dependent: set(para_into).
% 0.14/0.38 dependent: clear(para_from_right).
% 0.14/0.38 dependent: clear(para_into_right).
% 0.14/0.38 dependent: set(para_from_vars).
% 0.14/0.38 dependent: set(eq_units_both_ways).
% 0.14/0.38 dependent: set(dynamic_demod_all).
% 0.14/0.38 dependent: set(dynamic_demod).
% 0.14/0.38 dependent: set(order_eq).
% 0.14/0.38 dependent: set(back_demod).
% 0.14/0.38 dependent: set(lrpo).
% 0.14/0.38 dependent: set(hyper_res).
% 0.14/0.38 dependent: set(unit_deletion).
% 0.14/0.38 dependent: set(factor).
% 0.14/0.38
% 0.14/0.38 ------------> process usable:
% 0.14/0.38
% 0.14/0.38 ------------> process sos:
% 0.14/0.38 Following clause subsumed by 379 during input processing: 0 [copy,379,flip.1] {-} A=A.
% 0.14/0.38
% 0.14/0.38 ======= end of input processing =======
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44 Failed to model usable list: disabling FINDER
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44 -------------- Softie stats --------------
% 0.21/0.44
% 0.21/0.44 UPDATE_STOP: 300
% 0.21/0.44 SFINDER_TIME_LIMIT: 2
% 0.21/0.44 SHORT_CLAUSE_CUTOFF: 4
% 0.21/0.44 number of clauses in intial UL: 45
% 0.21/0.44 number of clauses initially in problem: 273
% 0.21/0.44 percentage of clauses intially in UL: 16
% 0.21/0.44 percentage of distinct symbols occuring in initial UL: 73
% 0.21/0.44 percent of all initial clauses that are short: 100
% 0.21/0.44 absolute distinct symbol count: 15
% 0.21/0.44 distinct predicate count: 1
% 0.21/0.44 distinct function count: 4
% 0.21/0.44 distinct constant count: 10
% 0.21/0.44
% 0.21/0.44 ---------- no more Softie stats ----------
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44 =========== start of search ===========
% 6.25/6.47
% 6.25/6.47
% 6.25/6.47 Changing weight limit from 60 to 44.
% 6.25/6.47
% 6.25/6.47 Resetting weight limit to 44 after 110 givens.
% 6.25/6.47
% 12.92/13.10
% 12.92/13.10
% 12.92/13.10 Changing weight limit from 44 to 41.
% 12.92/13.10
% 12.92/13.10 Resetting weight limit to 41 after 115 givens.
% 12.92/13.10
% 20.95/21.18
% 20.95/21.18
% 20.95/21.18 Changing weight limit from 41 to 38.
% 20.95/21.18
% 20.95/21.18 Resetting weight limit to 38 after 125 givens.
% 20.95/21.18
% 31.01/31.21
% 31.01/31.21
% 31.01/31.21 Changing weight limit from 38 to 37.
% 31.01/31.21
% 31.01/31.21 Resetting weight limit to 37 after 145 givens.
% 31.01/31.21
% 32.51/32.75
% 32.51/32.75
% 32.51/32.75 Changing weight limit from 37 to 35.
% 32.51/32.75
% 32.51/32.75 Resetting weight limit to 35 after 150 givens.
% 32.51/32.75
% 42.11/42.33
% 42.11/42.33
% 42.11/42.33 Changing weight limit from 35 to 34.
% 42.11/42.33
% 42.11/42.33 Resetting weight limit to 34 after 175 givens.
% 42.11/42.33
% 43.81/44.05
% 43.81/44.05
% 43.81/44.05 Changing weight limit from 34 to 32.
% 43.81/44.05
% 43.81/44.05 Resetting weight limit to 32 after 180 givens.
% 43.81/44.05
% 67.40/67.58
% 67.40/67.58
% 67.40/67.58 Changing weight limit from 32 to 31.
% 67.40/67.58
% 67.40/67.58 Resetting weight limit to 31 after 260 givens.
% 67.40/67.58
% 81.30/81.48
% 81.30/81.48
% 81.30/81.48 Changing weight limit from 31 to 29.
% 81.30/81.48
% 81.30/81.48 Resetting weight limit to 29 after 295 givens.
% 81.30/81.48
% 120.49/120.70
% 120.49/120.70
% 120.49/120.70 Changing weight limit from 29 to 28.
% 120.49/120.70
% 120.49/120.70 Modelling stopped after 300 given clauses and 0.00 seconds
% 120.49/120.70
% 120.49/120.70
% 120.49/120.70 Resetting weight limit to 28 after 460 givens.
% 120.49/120.70
% 124.37/124.57
% 124.37/124.57
% 124.37/124.57 Changing weight limit from 28 to 27.
% 124.37/124.57
% 124.37/124.57 Resetting weight limit to 27 after 485 givens.
% 124.37/124.57
% 127.17/127.34
% 127.17/127.34
% 127.17/127.34 Changing weight limit from 27 to 26.
% 127.17/127.34
% 127.17/127.34 Resetting weight limit to 26 after 535 givens.
% 127.17/127.34
% 138.18/138.36
% 138.18/138.36
% 138.18/138.36 Changing weight limit from 26 to 25.
% 138.18/138.36
% 138.18/138.36 Resetting weight limit to 25 after 650 givens.
% 138.18/138.36
% 139.08/139.34
% 139.08/139.34
% 139.08/139.34 Changing weight limit from 25 to 24.
% 139.08/139.34
% 139.08/139.34 Resetting weight limit to 24 after 660 givens.
% 139.08/139.34
% 147.71/147.90
% 147.71/147.90
% 147.71/147.90 Changing weight limit from 24 to 23.
% 147.71/147.90
% 147.71/147.90 Resetting weight limit to 23 after 760 givens.
% 147.71/147.90
% 151.89/152.09
% 151.89/152.09
% 151.89/152.09 Changing weight limit from 23 to 24.
% 151.89/152.09
% 151.89/152.09 Resetting weight limit to 24 after 810 givens.
% 151.89/152.09
% 152.14/152.34
% 152.14/152.34
% 152.14/152.34 Changing weight limit from 24 to 25.
% 152.14/152.34
% 152.14/152.34 Resetting weight limit to 25 after 815 givens.
% 152.14/152.34
% 152.37/152.56
% 152.37/152.56
% 152.37/152.56 Changing weight limit from 25 to 26.
% 152.37/152.56
% 152.37/152.56 Resetting weight limit to 26 after 820 givens.
% 152.37/152.56
% 152.37/152.60
% 152.37/152.60
% 152.37/152.60 Changing weight limit from 26 to 27.
% 152.37/152.60
% 152.37/152.60 Resetting weight limit to 27 after 825 givens.
% 152.37/152.60
% 152.44/152.64
% 152.44/152.64
% 152.44/152.64 Changing weight limit from 27 to 28.
% 152.44/152.64
% 152.44/152.64 Resetting weight limit to 28 after 830 givens.
% 152.44/152.64
% 152.49/152.68
% 152.49/152.68
% 152.49/152.68 Changing weight limit from 28 to 29.
% 152.49/152.68
% 152.49/152.68 Resetting weight limit to 29 after 835 givens.
% 152.49/152.68
% 152.58/152.79
% 152.58/152.79
% 152.58/152.79 Changing weight limit from 29 to 30.
% 152.58/152.79
% 152.58/152.79 Resetting weight limit to 30 after 840 givens.
% 152.58/152.79
% 152.78/152.95
% 152.78/152.95
% 152.78/152.95 Changing weight limit from 30 to 31.
% 152.78/152.95
% 152.78/152.95 Resetting weight limit to 31 after 845 givens.
% 152.78/152.95
% 152.86/153.06
% 152.86/153.06
% 152.86/153.06 Changing weight limit from 31 to 32.
% 152.86/153.06
% 152.86/153.06 Resetting weight limit to 32 after 850 givens.
% 152.86/153.06
% 152.98/153.16
% 152.98/153.16
% 152.98/153.16 Changing weight limit from 32 to 33.
% 152.98/153.16
% 152.98/153.16 Resetting weight limit to 33 after 855 givens.
% 152.98/153.16
% 153.04/153.23
% 153.04/153.23
% 153.04/153.23 Changing weight limit from 33 to 34.
% 153.04/153.23
% 153.04/153.23 Resetting weight limit to 34 after 860 givens.
% 153.04/153.23
% 153.77/153.98
% 153.77/153.98
% 153.77/153.98 Changing weight limit from 34 to 32.
% 153.77/153.98
% 153.77/153.98 Resetting weight limit to 32 after 980 givens.
% 153.77/153.98
% 154.18/154.42
% 154.18/154.42
% 154.18/154.42 Changing weight limit from 32 to 31.
% 154.18/154.42
% 154.18/154.42 Resetting weight limit to 31 after 990 givens.
% 154.18/154.42
% 154.44/154.62
% 154.44/154.62
% 154.44/154.62 Changing weight limit from 31 to 30.
% 154.44/154.62
% 154.44/154.62 Resetting weight limit to 30 after 1000 givens.
% 154.44/154.62
% 154.47/154.68
% 154.47/154.68
% 154.47/154.68 Changing weight limit from 30 to 29.
% 154.47/154.68
% 154.47/154.68 Resetting weight limit to 29 after 1005 givens.
% 154.47/154.68
% 155.60/155.83
% 155.60/155.83
% 155.60/155.83 Changing weight limit from 29 to 28.
% 155.60/155.83
% 155.60/155.83 Resetting weight limit to 28 after 1045 givens.
% 155.60/155.83
% 156.18/156.38
% 156.18/156.38
% 156.18/156.38 Changing weight limit from 28 to 27.
% 156.18/156.38
% 156.18/156.38 Resetting weight limit to 27 after 1070 givens.
% 156.18/156.38
% 156.27/156.45
% 156.27/156.45
% 156.27/156.45 Changing weight limit from 27 to 26.
% 156.27/156.45
% 156.27/156.45 Resetting weight limit to 26 after 1075 givens.
% 156.27/156.45
% 156.77/156.94
% 156.77/156.94 -- HEY sandbox2, WE HAVE A PROOF!! --
% 156.77/156.94
% 156.77/156.94 -----> EMPTY CLAUSE at 156.52 sec ----> 56567 [back_demod,56064,demod,56550,56550,56550,132,96,92,203,56558,56558,182,418,56550,56550,56550,56550,56550,92,98,94,96,unit_del,34,8] {-} $F.
% 156.77/156.94
% 156.77/156.94 Length of proof is 97. Level of proof is 28.
% 156.77/156.94
% 156.77/156.94 ---------------- PROOF ----------------
% 156.77/156.94 % SZS status Theorem
% 156.77/156.94 % SZS output start Refutation
% 156.77/156.94
% 156.77/156.94 1 [] {-} e10!=e11.
% 156.77/156.94 2 [copy,1,flip.1] {+} e11!=e10.
% 156.77/156.94 3 [] {-} e10!=e12.
% 156.77/156.94 4 [copy,3,flip.1] {+} e12!=e10.
% 156.77/156.94 5 [] {-} e10!=e13.
% 156.77/156.94 6 [copy,5,flip.1] {+} e13!=e10.
% 156.77/156.94 7 [] {-} e10!=e14.
% 156.77/156.94 8 [copy,7,flip.1] {+} e14!=e10.
% 156.77/156.94 19 [] {-} e13!=e14.
% 156.77/156.94 20 [copy,19,flip.1] {+} e14!=e13.
% 156.77/156.94 21 [] {-} e20!=e21.
% 156.77/156.94 22 [copy,21,flip.1] {+} e21!=e20.
% 156.77/156.94 23 [] {-} e20!=e22.
% 156.77/156.94 24 [copy,23,flip.1] {+} e22!=e20.
% 156.77/156.94 27 [] {-} e20!=e24.
% 156.77/156.94 28 [copy,27,flip.1] {+} e24!=e20.
% 156.77/156.94 29 [] {-} e21!=e22.
% 156.77/156.94 30 [copy,29,flip.1] {+} e22!=e21.
% 156.77/156.94 33 [] {-} e21!=e24.
% 156.77/156.94 34 [copy,33,flip.1] {+} e24!=e21.
% 156.77/156.94 37 [] {-} e22!=e24.
% 156.77/156.94 38 [copy,37,flip.1] {+} e24!=e22.
% 156.77/156.94 39 [] {-} e23!=e24.
% 156.77/156.94 40 [copy,39,flip.1] {+} e24!=e23.
% 156.77/156.94 92,91 [] {-} op1(e10,e10)=e13.
% 156.77/156.94 94,93 [] {-} op1(e10,e11)=e12.
% 156.77/156.94 96,95 [] {-} op1(e10,e12)=e10.
% 156.77/156.94 98,97 [] {-} op1(e10,e13)=e11.
% 156.77/156.94 102,101 [] {-} op1(e11,e10)=e10.
% 156.77/156.94 104,103 [] {-} op1(e11,e11)=e14.
% 156.77/156.94 112,111 [] {-} op1(e12,e10)=e11.
% 156.77/156.94 122,121 [] {-} op1(e13,e10)=e14.
% 156.77/156.94 128,127 [] {-} op1(e13,e13)=e10.
% 156.77/156.94 132,131 [] {-} op1(e14,e10)=e12.
% 156.77/156.94 134,133 [] {-} op1(e14,e11)=e10.
% 156.77/156.94 140,139 [] {-} op1(e14,e14)=e11.
% 156.77/156.94 142,141 [] {-} op2(e20,e20)=e24.
% 156.77/156.94 144,143 [] {-} op2(e20,e21)=e22.
% 156.77/156.94 146,145 [] {-} op2(e20,e22)=e20.
% 156.77/156.94 148,147 [] {-} op2(e20,e23)=e21.
% 156.77/156.94 150,149 [] {-} op2(e20,e24)=e23.
% 156.77/156.94 152,151 [] {-} op2(e21,e20)=e20.
% 156.77/156.94 168,167 [] {-} op2(e22,e23)=e20.
% 156.77/156.94 170,169 [] {-} op2(e22,e24)=e22.
% 156.77/156.94 176,175 [] {-} op2(e23,e22)=e24.
% 156.77/156.94 178,177 [] {-} op2(e23,e23)=e22.
% 156.77/156.94 180,179 [] {-} op2(e23,e24)=e21.
% 156.77/156.94 182,181 [] {-} op2(e24,e20)=e22.
% 156.77/156.94 186,185 [] {-} op2(e24,e22)=e21.
% 156.77/156.94 188,187 [] {-} op2(e24,e23)=e24.
% 156.77/156.94 190,189 [] {-} op2(e24,e24)=e20.
% 156.77/156.94 191 [] {-} h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 196 [] {-} j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e13|j(e20)=e14.
% 156.77/156.94 201 [] {-} h(op1(e10,e10))=op2(h(e10),h(e10)).
% 156.77/156.94 203,202 [copy,201,demod,92] {-} h(e13)=op2(h(e10),h(e10)).
% 156.77/156.94 210 [] {-} h(op1(e10,e13))=op2(h(e10),h(e13)).
% 156.77/156.94 212,211 [copy,210,demod,98,203] {-} h(e11)=op2(h(e10),op2(h(e10),h(e10))).
% 156.77/156.94 216 [] {-} h(op1(e11,e10))=op2(h(e11),h(e10)).
% 156.77/156.94 217 [copy,216,demod,102,212,flip.1] {-} op2(op2(h(e10),op2(h(e10),h(e10))),h(e10))=h(e10).
% 156.77/156.94 219 [] {-} h(op1(e11,e11))=op2(h(e11),h(e11)).
% 156.77/156.94 221,220 [copy,219,demod,104,212,212] {-} h(e14)=op2(op2(h(e10),op2(h(e10),h(e10))),op2(h(e10),op2(h(e10),h(e10)))).
% 156.77/156.94 246 [] {-} h(op1(e13,e10))=op2(h(e13),h(e10)).
% 156.77/156.94 248,247 [copy,246,demod,122,221,203] {-} op2(op2(h(e10),op2(h(e10),h(e10))),op2(h(e10),op2(h(e10),h(e10))))=op2(op2(h(e10),h(e10)),h(e10)).
% 156.77/156.94 276 [] {-} j(op2(e20,e20))=op1(j(e20),j(e20)).
% 156.77/156.94 278,277 [copy,276,demod,142] {-} j(e24)=op1(j(e20),j(e20)).
% 156.77/156.94 279 [] {-} j(op2(e20,e21))=op1(j(e20),j(e21)).
% 156.77/156.94 281,280 [copy,279,demod,144] {-} j(e22)=op1(j(e20),j(e21)).
% 156.77/156.94 282 [] {-} j(op2(e20,e22))=op1(j(e20),j(e22)).
% 156.77/156.94 283 [copy,282,demod,146,281,flip.1] {-} op1(j(e20),op1(j(e20),j(e21)))=j(e20).
% 156.77/156.94 285 [] {-} j(op2(e20,e23))=op1(j(e20),j(e23)).
% 156.77/156.94 286 [copy,285,demod,148,flip.1] {-} op1(j(e20),j(e23))=j(e21).
% 156.77/156.94 288 [] {-} j(op2(e20,e24))=op1(j(e20),j(e24)).
% 156.77/156.94 290,289 [copy,288,demod,150,278] {-} j(e23)=op1(j(e20),op1(j(e20),j(e20))).
% 156.77/156.94 291 [] {-} j(op2(e21,e20))=op1(j(e21),j(e20)).
% 156.77/156.94 292 [copy,291,demod,152,flip.1] {-} op1(j(e21),j(e20))=j(e20).
% 156.77/156.94 333 [] {-} j(op2(e23,e24))=op1(j(e23),j(e24)).
% 156.77/156.94 335,334 [copy,333,demod,180,290,278] {-} j(e21)=op1(op1(j(e20),op1(j(e20),j(e20))),op1(j(e20),j(e20))).
% 156.77/156.94 336 [] {-} j(op2(e24,e20))=op1(j(e24),j(e20)).
% 156.77/156.94 338,337 [copy,336,demod,182,281,335,278] {-} op1(j(e20),op1(op1(j(e20),op1(j(e20),j(e20))),op1(j(e20),j(e20))))=op1(op1(j(e20),j(e20)),j(e20)).
% 156.77/156.94 342 [] {-} j(op2(e24,e22))=op1(j(e24),j(e22)).
% 156.77/156.94 344,343 [copy,342,demod,186,335,278,281,335,338] {-} op1(op1(j(e20),op1(j(e20),j(e20))),op1(j(e20),j(e20)))=op1(op1(j(e20),j(e20)),op1(op1(j(e20),j(e20)),j(e20))).
% 156.77/156.94 351 [] {-} h(j(e20))=e20.
% 156.77/156.94 353 [] {-} h(j(e21))=e21.
% 156.77/156.94 354 [copy,353,demod,335,344] {-} h(op1(op1(j(e20),j(e20)),op1(op1(j(e20),j(e20)),j(e20))))=e21.
% 156.77/156.94 359 [] {-} h(j(e23))=e23.
% 156.77/156.94 360 [copy,359,demod,290] {-} h(op1(j(e20),op1(j(e20),j(e20))))=e23.
% 156.77/156.94 362 [] {-} h(j(e24))=e24.
% 156.77/156.94 363 [copy,362,demod,278] {-} h(op1(j(e20),j(e20)))=e24.
% 156.77/156.94 365 [] {-} j(h(e10))=e10.
% 156.77/156.94 367 [] {-} j(h(e11))=e11.
% 156.77/156.94 368 [copy,367,demod,212] {-} j(op2(h(e10),op2(h(e10),h(e10))))=e11.
% 156.77/156.94 373 [] {-} j(h(e13))=e13.
% 156.77/156.94 374 [copy,373,demod,203] {-} j(op2(h(e10),h(e10)))=e13.
% 156.77/156.94 376 [] {-} j(h(e14))=e14.
% 156.77/156.94 377 [copy,376,demod,221,248] {-} j(op2(op2(h(e10),h(e10)),h(e10)))=e14.
% 156.77/156.94 399,398 [back_demod,286,demod,290,335,344,flip.1] {-} op1(op1(j(e20),j(e20)),op1(op1(j(e20),j(e20)),j(e20)))=op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))).
% 156.77/156.94 415 [back_demod,283,demod,335,344,399] {-} op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20))))))=j(e20).
% 156.77/156.94 418,417 [back_demod,280,demod,335,344,399] {-} j(e22)=op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20))))).
% 156.77/156.94 429 [back_demod,292,demod,335,344,399] {-} op1(op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))),j(e20))=j(e20).
% 156.77/156.94 434,433 [back_demod,337,demod,344,399,flip.1] {-} op1(op1(j(e20),j(e20)),j(e20))=op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20))))).
% 156.77/156.94 435 [back_demod,334,demod,344,434] {-} j(e21)=op1(op1(j(e20),j(e20)),op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))))).
% 156.77/156.94 439 [back_demod,354,demod,434] {-} h(op1(op1(j(e20),j(e20)),op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))))))=e21.
% 156.77/156.94 444,443 [back_demod,398,demod,434] {-} op1(op1(j(e20),j(e20)),op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20))))))=op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))).
% 156.77/156.94 447 [back_demod,439,demod,444] {-} h(op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))))=e21.
% 156.77/156.94 452,451 [back_demod,435,demod,444] {-} j(e21)=op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))).
% 156.77/156.94 453 [para_from,191.1.1,365.1.1.1] {-} j(e20)=e10|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 454 [para_from,191.2.1,365.1.1.1,demod,452] {-} op1(j(e20),op1(j(e20),op1(j(e20),j(e20))))=e10|h(e10)=e20|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 455 [para_from,191.3.1,365.1.1.1,demod,418] {-} op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),j(e20)))))=e10|h(e10)=e20|h(e10)=e21|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 458 [para_into,374.1.1.1.1,191.5.1] {-} j(op2(e24,h(e10)))=e13|h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23.
% 156.77/156.94 468 [para_from,196.1.1,351.1.1.1] {-} h(e10)=e20|j(e20)=e11|j(e20)=e12|j(e20)=e13|j(e20)=e14.
% 156.77/156.94 478 [para_from,196.4.1,363.1.1.1.2] {-} h(op1(j(e20),e13))=e24|j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e14.
% 156.77/156.94 488 [para_into,360.1.1.1.2.1,196.5.1] {-} h(op1(j(e20),op1(e14,j(e20))))=e23|j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e13.
% 156.77/156.94 2522 [para_into,458.1.1.1.2,191.5.1,demod,190,factor_simp,factor_simp,factor_simp,factor_simp] {-} j(e20)=e13|h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23.
% 156.77/156.94 3040 [para_into,2522.2.1,453.5.1,unit_del,28,factor_simp,factor_simp,factor_simp] {-} j(e20)=e13|h(e10)=e21|h(e10)=e22|h(e10)=e23|j(e20)=e10.
% 156.77/156.94 11057 [para_into,478.1.1.1.1,196.4.1,demod,128,factor_simp,factor_simp,factor_simp,factor_simp] {-} h(e10)=e24|j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e14.
% 156.77/156.94 11224 [para_into,11057.2.1,468.4.1,unit_del,6,factor_simp,factor_simp,factor_simp] {-} h(e10)=e24|j(e20)=e11|j(e20)=e12|j(e20)=e14|h(e10)=e20.
% 156.77/156.94 16658 [para_from,454.1.1,429.1.1.1] {-} op1(e10,j(e20))=j(e20)|h(e10)=e20|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 16955 [para_from,455.1.1,415.1.1.2] {-} op1(j(e20),e10)=j(e20)|h(e10)=e20|h(e10)=e21|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 20168 [para_into,488.1.1.1.2.2,196.5.1,demod,140,factor_simp,factor_simp,factor_simp,factor_simp] {-} h(op1(j(e20),e11))=e23|j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e13.
% 156.77/156.94 23246 [para_into,20168.1.1.1.1,196.5.1,demod,134,factor_simp,factor_simp,factor_simp,factor_simp] {-} h(e10)=e23|j(e20)=e10|j(e20)=e11|j(e20)=e12|j(e20)=e13.
% 156.77/156.94 23418 [para_into,23246.2.1,468.5.1,unit_del,8,factor_simp,factor_simp,factor_simp] {-} h(e10)=e23|j(e20)=e11|j(e20)=e12|j(e20)=e13|h(e10)=e20.
% 156.77/156.94 23589 [para_into,23418.4.1,11224.4.1,unit_del,20,factor_simp,factor_simp,factor_simp] {-} h(e10)=e23|j(e20)=e11|j(e20)=e12|h(e10)=e20|h(e10)=e24.
% 156.77/156.94 23807 [para_from,23589.2.1,16658.1.1.2,demod,94,factor_simp,factor_simp,factor_simp,factor_simp] {-} j(e20)=e12|h(e10)=e20|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 23820 [para_from,23589.3.1,16955.1.1.1,demod,112,factor_simp,factor_simp,factor_simp,factor_simp] {-} j(e20)=e11|h(e10)=e20|h(e10)=e21|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 23974 [para_from,23807.1.1,16658.1.1.2,demod,96,factor_simp,factor_simp,factor_simp,factor_simp] {-} j(e20)=e10|h(e10)=e20|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 24482 [para_into,23974.1.1,23807.1.1,unit_del,4,factor_simp,factor_simp,factor_simp,factor_simp] {-} h(e10)=e20|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 24526 [para_into,23974.2.1,453.2.1,unit_del,22,factor_simp,factor_simp,factor_simp,factor_simp] {-} j(e20)=e10|h(e10)=e22|h(e10)=e23|h(e10)=e24.
% 156.77/156.94 24591 [para_into,24482.2.1,23820.3.1,unit_del,30,factor_simp,factor_simp,factor_simp] {-} h(e10)=e20|h(e10)=e23|h(e10)=e24|j(e20)=e11.
% 156.77/156.94 24592 [para_into,24482.2.1,16955.3.1,unit_del,30,factor_simp,factor_simp,factor_simp] {-} h(e10)=e20|h(e10)=e23|h(e10)=e24|op1(j(e20),e10)=j(e20).
% 156.77/156.94 24756 [para_into,24526.4.1,3040.2.1,unit_del,34,factor_simp,factor_simp,factor_simp] {-} j(e20)=e10|h(e10)=e22|h(e10)=e23|j(e20)=e13.
% 156.77/156.94 24852 [para_into,24591.1.1,24526.2.1,unit_del,24,factor_simp,factor_simp] {-} h(e10)=e23|h(e10)=e24|j(e20)=e11|j(e20)=e10.
% 156.77/156.94 27942 [para_into,24592.4.1.1,24852.3.1,demod,102,factor_simp,factor_simp,factor_simp] {-} h(e10)=e20|h(e10)=e23|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 28023 [para_into,27942.1.1,24526.2.1,unit_del,24,factor_simp,factor_simp,factor_simp] {-} h(e10)=e23|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 28051 [para_into,28023.2.1,24756.2.1,unit_del,38,factor_simp,factor_simp] {-} h(e10)=e23|j(e20)=e10|j(e20)=e13.
% 156.77/156.94 28078 [para_from,28023.1.1,377.1.1.1.2] {-} j(op2(op2(h(e10),h(e10)),e23))=e14|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 28083 [para_from,28023.1.1,217.1.1.2] {-} op2(op2(h(e10),op2(h(e10),h(e10))),e23)=h(e10)|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 28098 [para_from,28023.1.1,368.1.1.1.2.2] {-} j(op2(h(e10),op2(h(e10),e23)))=e11|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 28131 [para_from,28023.2.1,217.1.1.1.1] {-} op2(op2(e24,op2(h(e10),h(e10))),h(e10))=h(e10)|h(e10)=e23|j(e20)=e10.
% 156.77/156.94 28458 [para_from,28051.3.1,351.1.1.1,demod,203] {-} op2(h(e10),h(e10))=e20|h(e10)=e23|j(e20)=e10.
% 156.77/156.94 36558 [para_into,28078.1.1.1.1.1,28023.1.1,factor_simp,factor_simp] {-} j(op2(op2(e23,h(e10)),e23))=e14|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 36741 [para_into,36558.1.1.1.1.2,28023.1.1,demod,178,168,factor_simp,factor_simp] {-} j(e20)=e14|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 37057 [para_into,36741.2.1,28051.1.1,unit_del,40,factor_simp] {-} j(e20)=e14|j(e20)=e10|j(e20)=e13.
% 156.77/156.94 37473 [para_from,37057.2.1,351.1.1.1] {-} h(e10)=e20|j(e20)=e14|j(e20)=e13.
% 156.77/156.94 41296 [para_into,28098.1.1.1.2.1,28023.1.1,demod,178,factor_simp,factor_simp] {-} j(op2(h(e10),e22))=e11|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 41335 [para_into,41296.1.1.1.1,28023.1.1,demod,176,278,factor_simp,factor_simp] {-} op1(j(e20),j(e20))=e11|h(e10)=e24|j(e20)=e10.
% 156.77/156.94 44793 [para_into,28131.1.1.1.2,28458.1.1,demod,182,factor_simp,factor_simp] {-} op2(e22,h(e10))=h(e10)|h(e10)=e23|j(e20)=e10.
% 156.77/156.94 44858 [para_into,44793.1.1.2,28023.2.1,demod,170,factor_simp,factor_simp] {-} h(e10)=e22|h(e10)=e23|j(e20)=e10.
% 156.77/156.94 45062 [para_into,44858.1.1,28023.2.1,unit_del,38,factor_simp,factor_simp] {-} h(e10)=e23|j(e20)=e10.
% 156.77/156.94 45224 [para_into,45062.1.1,41335.2.1,unit_del,40,factor_simp] {-} j(e20)=e10|op1(j(e20),j(e20))=e11.
% 156.77/156.94 45246 [para_into,45062.1.1,36741.2.1,unit_del,40,factor_simp] {-} j(e20)=e10|j(e20)=e14.
% 156.77/156.94 45283 [para_into,45062.1.1,28083.2.1,unit_del,40,factor_simp] {-} j(e20)=e10|op2(op2(h(e10),op2(h(e10),h(e10))),e23)=h(e10).
% 156.77/156.94 45423 [para_into,45246.1.1,37473.3.1,unit_del,6,factor_simp] {-} j(e20)=e14|h(e10)=e20.
% 156.77/156.94 45644 [para_from,45423.2.1,377.1.1.1.2] {-} j(op2(op2(h(e10),h(e10)),e20))=e14|j(e20)=e14.
% 156.77/156.94 46338 [para_from,45224.1.1,363.1.1.1.1] {-} h(op1(e10,j(e20)))=e24|op1(j(e20),j(e20))=e11.
% 156.77/156.94 46353 [para_from,45224.2.1,363.1.1.1,demod,212] {-} op2(h(e10),op2(h(e10),h(e10)))=e24|j(e20)=e10.
% 156.77/156.94 56064 [para_from,45644.2.1,447.1.1.1.2.2.1] {-} h(op1(j(e20),op1(j(e20),op1(e14,j(e20)))))=e21|j(op2(op2(h(e10),h(e10)),e20))=e14.
% 156.77/156.94 56248 [para_from,46338.2.1,415.1.1.2.2.2.2] {-} op1(j(e20),op1(j(e20),op1(j(e20),op1(j(e20),e11))))=j(e20)|h(op1(e10,j(e20)))=e24.
% 156.77/156.94 56482 [para_into,45283.2.1.1,46353.1.1,demod,188,factor_simp] {-} j(e20)=e10|h(e10)=e24.
% 156.77/156.94 56550,56549 [para_into,56482.2.1,45062.1.1,unit_del,40,factor_simp] {-} j(e20)=e10.
% 156.77/156.94 56558,56557 [back_demod,56248,demod,56550,56550,56550,56550,94,96,92,98,56550,56550,92,203,unit_del,2] {-} op2(h(e10),h(e10))=e24.
% 156.77/156.94 56567 [back_demod,56064,demod,56550,56550,56550,132,96,92,203,56558,56558,182,418,56550,56550,56550,56550,56550,92,98,94,96,unit_del,34,8] {-} $F.
% 156.77/156.94
% 156.77/156.94 % SZS output end Refutation
% 156.77/156.94 ------------ end of proof -------------
% 156.77/156.94
% 156.77/156.94
% 156.77/156.94 Search stopped by max_proofs option.
% 156.77/156.94
% 156.77/156.94
% 156.77/156.94 Search stopped by max_proofs option.
% 156.77/156.94
% 156.77/156.94 ============ end of search ============
% 156.77/156.94
% 156.77/156.94 That finishes the proof of the theorem.
% 156.77/156.94
% 156.77/156.94 Process 21131 finished Tue Jun 7 22:08:13 2022
%------------------------------------------------------------------------------