%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP106_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n007.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 : Tue May 5 07:14:06 PM UTC 2026
% Result : Theorem 50.31s 51.85s
% Output : Proof 50.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYP106_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_nanocopm %s %d
% 0.15/0.33 % Computer : n007.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 17:40:53 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.18/0.46 % Logic is t
% 0.18/0.47 % Designation is rigid
% 0.30/0.47 % Terms are local
% 0.30/0.48 % Domains are const
% 0.30/0.49 ------------ Start QMF file ---------------
% 0.30/0.49 %------------------------------------------------------------------------------
% 0.30/0.49 % File : SYP106_1 : TPTP v9.3.0. Released v9.3.0.
% 0.30/0.49 % Domain : Syntactic
% 0.30/0.49 % Problem : Logic KT, problem k_lin, size 10
% 0.30/0.49 % Version : Especial.
% 0.30/0.49 % English :
% 0.30/0.49 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.30/0.49 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.30/0.49 % Source : [Ste24]
% 0.30/0.49 % Names : KT/k_lin_n/10.p
% 0.30/0.49 % Status : CounterSatisfiable
% 0.30/0.49 % Rating : ? v9.2.0
% 0.30/0.49 % Syntax : Number of formulae : 38 ( 0 unt; 37 typ; 0 def)
% 0.30/0.49 % Number of atoms : 529 ( 0 equ)
% 0.30/0.49 % Maximal formula atoms : 529 ( 529 avg)
% 0.30/0.49 % Number of connectives : 1092 ( 70 ~; 141 |; 140 &)
% 0.30/0.49 % ( 0 <=>; 247 =>; 0 <=; 0 <~>)
% 0.30/0.49 % ( 494 {.}; 0 {#})
% 0.30/0.49 % Maximal formula depth : 80 ( 80 avg)
% 0.30/0.49 % Maximal term depth : 0 ( 0 avg)
% 0.30/0.49 % Number of types : 1 ( 0 usr)
% 0.30/0.49 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.30/0.49 % Number of predicates : 37 ( 37 usr; 37 prp; 0-0 aty)
% 0.30/0.49 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.30/0.49 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.30/0.49 % SPC : NX0_CSA_PRP_NEQ_NAR
% 0.30/0.49 % Comments :
% 0.30/0.49 %------------------------------------------------------------------------------
% 0.30/0.49 qmf(10,conjecture,(~ ( #box : ( ( ( #dia : ( p1 ) & #box : ( #dia : ( p1 ) ) ) => p2 ) ) | #box : ( ( ( p2 & #box : ( p2 ) ) => #dia : ( p1 ) ) ) ) | ~ ( #box : ( ( ( ( p1 => #box : ( p2 ) ) & #box : ( ( p1 => #box : ( p2 ) ) ) ) => p2 ) ) | #box : ( ( ( p2 & #box : ( p2 ) ) => ( p1 => #box : ( p2 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p2 ) & #box : ( #dia : ( p2 ) ) ) => p3 ) ) | #box : ( ( ( p3 & #box : ( p3 ) ) => #dia : ( p2 ) ) ) ) | ~ ( #box : ( ( ( ( p2 => #box : ( p3 ) ) & #box : ( ( p2 => #box : ( p3 ) ) ) ) => p3 ) ) | #box : ( ( ( p3 & #box : ( p3 ) ) => ( p2 => #box : ( p3 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p3 ) & #box : ( #dia : ( p3 ) ) ) => p4 ) ) | #box : ( ( ( p4 & #box : ( p4 ) ) => #dia : ( p3 ) ) ) ) | ~ ( #box : ( ( ( ( p3 => #box : ( p4 ) ) & #box : ( ( p3 => #box : ( p4 ) ) ) ) => p4 ) ) | #box : ( ( ( p4 & #box : ( p4 ) ) => ( p3 => #box : ( p4 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p4 ) & #box : ( #dia : ( p4 ) ) ) => p5 ) ) | #box : ( ( ( p5 & #box : ( p5 ) ) => #dia : ( p4 ) ) ) ) | ~ ( #box : ( ( ( ( p4 => #box : ( p5 ) ) & #box : ( ( p4 => #box : ( p5 ) ) ) ) => p5 ) ) | #box : ( ( ( p5 & #box : ( p5 ) ) => ( p4 => #box : ( p5 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p5 ) & #box : ( #dia : ( p5 ) ) ) => p6 ) ) | #box : ( ( ( p6 & #box : ( p6 ) ) => #dia : ( p5 ) ) ) ) | ~ ( #box : ( ( ( ( p5 => #box : ( p6 ) ) & #box : ( ( p5 => #box : ( p6 ) ) ) ) => p6 ) ) | #box : ( ( ( p6 & #box : ( p6 ) ) => ( p5 => #box : ( p6 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p6 ) & #box : ( #dia : ( p6 ) ) ) => p7 ) ) | #box : ( ( ( p7 & #box : ( p7 ) ) => #dia : ( p6 ) ) ) ) | ~ ( #box : ( ( ( ( p6 => #box : ( p7 ) ) & #box : ( ( p6 => #box : ( p7 ) ) ) ) => p7 ) ) | #box : ( ( ( p7 & #box : ( p7 ) ) => ( p6 => #box : ( p7 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p7 ) & #box : ( #dia : ( p7 ) ) ) => p8 ) ) | #box : ( ( ( p8 & #box : ( p8 ) ) => #dia : ( p7 ) ) ) ) | ~ ( #box : ( ( ( ( p7 => #box : ( p8 ) ) & #box : ( ( p7 => #box : ( p8 ) ) ) ) => p8 ) ) | #box : ( ( ( p8 & #box : ( p8 ) ) => ( p7 => #box : ( p8 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p8 ) & #box : ( #dia : ( p8 ) ) ) => p9 ) ) | #box : ( ( ( p9 & #box : ( p9 ) ) => #dia : ( p8 ) ) ) ) | ~ ( #box : ( ( ( ( p8 => #box : ( p9 ) ) & #box : ( ( p8 => #box : ( p9 ) ) ) ) => p9 ) ) | #box : ( ( ( p9 & #box : ( p9 ) ) => ( p8 => #box : ( p9 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p9 ) & #box : ( #dia : ( p9 ) ) ) => p10 ) ) | #box : ( ( ( p10 & #box : ( p10 ) ) => #dia : ( p9 ) ) ) ) | ~ ( #box : ( ( ( ( p9 => #box : ( p10 ) ) & #box : ( ( p9 => #box : ( p10 ) ) ) ) => p10 ) ) | #box : ( ( ( p10 & #box : ( p10 ) ) => ( p9 => #box : ( p10 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p10 ) & #box : ( #dia : ( p10 ) ) ) => p11 ) ) | #box : ( ( ( p11 & #box : ( p11 ) ) => #dia : ( p10 ) ) ) ) | ~ ( #box : ( ( ( ( p10 => #box : ( p11 ) ) & #box : ( ( p10 => #box : ( p11 ) ) ) ) => p11 ) ) | #box : ( ( ( p11 & #box : ( p11 ) ) => ( p10 => #box : ( p11 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p11 ) & #box : ( #dia : ( p11 ) ) ) => p12 ) ) | #box : ( ( ( p12 & #box : ( p12 ) ) => #dia : ( p11 ) ) ) ) | ~ ( #box : ( ( ( ( p11 => #box : ( p12 ) ) & #box : ( ( p11 => #box : ( p12 ) ) ) ) => p12 ) ) | #box : ( ( ( p12 & #box : ( p12 ) ) => ( p11 => #box : ( p12 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p12 ) & #box : ( #dia : ( p12 ) ) ) => p13 ) ) | #box : ( ( ( p13 & #box : ( p13 ) ) => #dia : ( p12 ) ) ) ) | ~ ( #box : ( ( ( ( p12 => #box : ( p13 ) ) & #box : ( ( p12 => #box : ( p13 ) ) ) ) => p13 ) ) | #box : ( ( ( p13 & #box : ( p13 ) ) => ( p12 => #box : ( p13 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p13 ) & #box : ( #dia : ( p13 ) ) ) => p14 ) ) | #box : ( ( ( p14 & #box : ( p14 ) ) => #dia : ( p13 ) ) ) ) | ~ ( #box : ( ( ( ( p13 => #box : ( p14 ) ) & #box : ( ( p13 => #box : ( p14 ) ) ) ) => p14 ) ) | #box : ( ( ( p14 & #box : ( p14 ) ) => ( p13 => #box : ( p14 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p14 ) & #box : ( #dia : ( p14 ) ) ) => p15 ) ) | #box : ( ( ( p15 & #box : ( p15 ) ) => #dia : ( p14 ) ) ) ) | ~ ( #box : ( ( ( ( p14 => #box : ( p15 ) ) & #box : ( ( p14 => #box : ( p15 ) ) ) ) => p15 ) ) | #box : ( ( ( p15 & #box : ( p15 ) ) => ( p14 => #box : ( p15 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p15 ) & #box : ( #dia : ( p15 ) ) ) => p16 ) ) | #box : ( ( ( p16 & #box : ( p16 ) ) => #dia : ( p15 ) ) ) ) | ~ ( #box : ( ( ( ( p15 => #box : ( p16 ) ) & #box : ( ( p15 => #box : ( p16 ) ) ) ) => p16 ) ) | #box : ( ( ( p16 & #box : ( p16 ) ) => ( p15 => #box : ( p16 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p16 ) & #box : ( #dia : ( p16 ) ) ) => p17 ) ) | #box : ( ( ( p17 & #box : ( p17 ) ) => #dia : ( p16 ) ) ) ) | ~ ( #box : ( ( ( ( p16 => #box : ( p17 ) ) & #box : ( ( p16 => #box : ( p17 ) ) ) ) => p17 ) ) | #box : ( ( ( p17 & #box : ( p17 ) ) => ( p16 => #box : ( p17 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p17 ) & #box : ( #dia : ( p17 ) ) ) => p18 ) ) | #box : ( ( ( p18 & #box : ( p18 ) ) => #dia : ( p17 ) ) ) ) | ~ ( #box : ( ( ( ( p17 => #box : ( p18 ) ) & #box : ( ( p17 => #box : ( p18 ) ) ) ) => p18 ) ) | #box : ( ( ( p18 & #box : ( p18 ) ) => ( p17 => #box : ( p18 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p18 ) & #box : ( #dia : ( p18 ) ) ) => p19 ) ) | #box : ( ( ( p19 & #box : ( p19 ) ) => #dia : ( p18 ) ) ) ) | ~ ( #box : ( ( ( ( p18 => #box : ( p19 ) ) & #box : ( ( p18 => #box : ( p19 ) ) ) ) => p19 ) ) | #box : ( ( ( p19 & #box : ( p19 ) ) => ( p18 => #box : ( p19 ) ) ) ) ) | #box : ( ( #box : ( p10 ) => p10 ) ) | #box : ( ( #box : ( p10 ) => p10 ) ) | ~ ( #box : ( ( ( #dia : ( p20 ) & #box : ( #dia : ( p20 ) ) ) => p21 ) ) | #box : ( ( ( p21 & #box : ( p21 ) ) => #dia : ( p20 ) ) ) ) | ~ ( #box : ( ( ( ( p20 => #box : ( p21 ) ) & #box : ( ( p20 => #box : ( p21 ) ) ) ) => p21 ) ) | #box : ( ( ( p21 & #box : ( p21 ) ) => ( p20 => #box : ( p21 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p21 ) & #box : ( #dia : ( p21 ) ) ) => p22 ) ) | #box : ( ( ( p22 & #box : ( p22 ) ) => #dia : ( p21 ) ) ) ) | ~ ( #box : ( ( ( ( p21 => #box : ( p22 ) ) & #box : ( ( p21 => #box : ( p22 ) ) ) ) => p22 ) ) | #box : ( ( ( p22 & #box : ( p22 ) ) => ( p21 => #box : ( p22 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p22 ) & #box : ( #dia : ( p22 ) ) ) => p23 ) ) | #box : ( ( ( p23 & #box : ( p23 ) ) => #dia : ( p22 ) ) ) ) | ~ ( #box : ( ( ( ( p22 => #box : ( p23 ) ) & #box : ( ( p22 => #box : ( p23 ) ) ) ) => p23 ) ) | #box : ( ( ( p23 & #box : ( p23 ) ) => ( p22 => #box : ( p23 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p23 ) & #box : ( #dia : ( p23 ) ) ) => p24 ) ) | #box : ( ( ( p24 & #box : ( p24 ) ) => #dia : ( p23 ) ) ) ) | ~ ( #box : ( ( ( ( p23 => #box : ( p24 ) ) & #box : ( ( p23 => #box : ( p24 ) ) ) ) => p24 ) ) | #box : ( ( ( p24 & #box : ( p24 ) ) => ( p23 => #box : ( p24 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p24 ) & #box : ( #dia : ( p24 ) ) ) => p25 ) ) | #box : ( ( ( p25 & #box : ( p25 ) ) => #dia : ( p24 ) ) ) ) | ~ ( #box : ( ( ( ( p24 => #box : ( p25 ) ) & #box : ( ( p24 => #box : ( p25 ) ) ) ) => p25 ) ) | #box : ( ( ( p25 & #box : ( p25 ) ) => ( p24 => #box : ( p25 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p25 ) & #box : ( #dia : ( p25 ) ) ) => p26 ) ) | #box : ( ( ( p26 & #box : ( p26 ) ) => #dia : ( p25 ) ) ) ) | ~ ( #box : ( ( ( ( p25 => #box : ( p26 ) ) & #box : ( ( p25 => #box : ( p26 ) ) ) ) => p26 ) ) | #box : ( ( ( p26 & #box : ( p26 ) ) => ( p25 => #box : ( p26 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p26 ) & #box : ( #dia : ( p26 ) ) ) => p27 ) ) | #box : ( ( ( p27 & #box : ( p27 ) ) => #dia : ( p26 ) ) ) ) | ~ ( #box : ( ( ( ( p26 => #box : ( p27 ) ) & #box : ( ( p26 => #box : ( p27 ) ) ) ) => p27 ) ) | #box : ( ( ( p27 & #box : ( p27 ) ) => ( p26 => #box : ( p27 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p27 ) & #box : ( #dia : ( p27 ) ) ) => p28 ) ) | #box : ( ( ( p28 & #box : ( p28 ) ) => #dia : ( p27 ) ) ) ) | ~ ( #box : ( ( ( ( p27 => #box : ( p28 ) ) & #box : ( ( p27 => #box : ( p28 ) ) ) ) => p28 ) ) | #box : ( ( ( p28 & #box : ( p28 ) ) => ( p27 => #box : ( p28 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p28 ) & #box : ( #dia : ( p28 ) ) ) => p29 ) ) | #box : ( ( ( p29 & #box : ( p29 ) ) => #dia : ( p28 ) ) ) ) | ~ ( #box : ( ( ( ( p28 => #box : ( p29 ) ) & #box : ( ( p28 => #box : ( p29 ) ) ) ) => p29 ) ) | #box : ( ( ( p29 & #box : ( p29 ) ) => ( p28 => #box : ( p29 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p29 ) & #box : ( #dia : ( p29 ) ) ) => p30 ) ) | #box : ( ( ( p30 & #box : ( p30 ) ) => #dia : ( p29 ) ) ) ) | ~ ( #box : ( ( ( ( p29 => #box : ( p30 ) ) & #box : ( ( p29 => #box : ( p30 ) ) ) ) => p30 ) ) | #box : ( ( ( p30 & #box : ( p30 ) ) => ( p29 => #box : ( p30 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p30 ) & #box : ( #dia : ( p30 ) ) ) => p31 ) ) | #box : ( ( ( p31 & #box : ( p31 ) ) => #dia : ( p30 ) ) ) ) | ~ ( #box : ( ( ( ( p30 => #box : ( p31 ) ) & #box : ( ( p30 => #box : ( p31 ) ) ) ) => p31 ) ) | #box : ( ( ( p31 & #box : ( p31 ) ) => ( p30 => #box : ( p31 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p31 ) & #box : ( #dia : ( p31 ) ) ) => p32 ) ) | #box : ( ( ( p32 & #box : ( p32 ) ) => #dia : ( p31 ) ) ) ) | ~ ( #box : ( ( ( ( p31 => #box : ( p32 ) ) & #box : ( ( p31 => #box : ( p32 ) ) ) ) => p32 ) ) | #box : ( ( ( p32 & #box : ( p32 ) ) => ( p31 => #box : ( p32 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p32 ) & #box : ( #dia : ( p32 ) ) ) => p33 ) ) | #box : ( ( ( p33 & #box : ( p33 ) ) => #dia : ( p32 ) ) ) ) | ~ ( #box : ( ( ( ( p32 => #box : ( p33 ) ) & #box : ( ( p32 => #box : ( p33 ) ) ) ) => p33 ) ) | #box : ( ( ( p33 & #box : ( p33 ) ) => ( p32 => #box : ( p33 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p33 ) & #box : ( #dia : ( p33 ) ) ) => p34 ) ) | #box : ( ( ( p34 & #box : ( p34 ) ) => #dia : ( p33 ) ) ) ) | ~ ( #box : ( ( ( ( p33 => #box : ( p34 ) ) & #box : ( ( p33 => #box : ( p34 ) ) ) ) => p34 ) ) | #box : ( ( ( p34 & #box : ( p34 ) ) => ( p33 => #box : ( p34 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p34 ) & #box : ( #dia : ( p34 ) ) ) => p35 ) ) | #box : ( ( ( p35 & #box : ( p35 ) ) => #dia : ( p34 ) ) ) ) | ~ ( #box : ( ( ( ( p34 => #box : ( p35 ) ) & #box : ( ( p34 => #box : ( p35 ) ) ) ) => p35 ) ) | #box : ( ( ( p35 & #box : ( p35 ) ) => ( p34 => #box : ( p35 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p35 ) & #box : ( #dia : ( p35 ) ) ) => p36 ) ) | #box : ( ( ( p36 & #box : ( p36 ) ) => #dia : ( p35 ) ) ) ) | ~ ( #box : ( ( ( ( p35 => #box : ( p36 ) ) & #box : ( ( p35 => #box : ( p36 ) ) ) ) => p36 ) ) | #box : ( ( ( p36 & #box : ( p36 ) ) => ( p35 => #box : ( p36 ) ) ) ) ) | ~ ( #box : ( ( ( #dia : ( p36 ) & #box : ( #dia : ( p36 ) ) ) => p37 ) ) | #box : ( ( ( p37 & #box : ( p37 ) ) => #dia : ( p36 ) ) ) ) | ~ ( #box : ( ( ( ( p36 => #box : ( p37 ) ) & #box : ( ( p36 => #box : ( p37 ) ) ) ) => p37 ) ) | #box : ( ( ( p37 & #box : ( p37 ) ) => ( p36 => #box : ( p37 ) ) ) ) ) )).
% 0.30/0.49 %------------------------------------------------------------------------------
% 0.30/0.49 ------------ End QMF file ---------------
% 50.31/51.85
% 50.31/51.85 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.cmSSjqqhWb/theBenchmark.p.qmf : (modal (t/const))
% 50.31/51.85 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.cmSSjqqhWb/theBenchmark.p.qmf
% 50.31/51.85 ------------------------------------------------------
% 50.31/51.85 Explanations for the proof presented below:
% 50.31/51.85 - equality axioms are added if required
% 50.31/51.85 - terms and variables are represented by Prolog terms
% 50.31/51.85 and Prolog variables, negation is represented by -
% 50.31/51.85 - a prefix Pre is a list of variables and constants
% 50.31/51.85 and assigned to each literal Lit, i.e. Pre:Lit
% 50.31/51.85 - clauses and (sub-)matrices have a unique label I^K:
% 50.31/51.85 or I^K^[..]:, where I is a unique number/identifier
% 50.31/51.85 and K identifies the instance of clause/matrix I
% 50.31/51.85 - I:Lit refers to literal Lit in clause number I
% 50.31/51.85 - in the matrix, I^[t1,..,tn] may represent the atom
% 50.31/51.85 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 50.31/51.85 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 50.31/51.85 the assignments X1:=t1, .., Xn:=tn (for both term
% 50.31/51.85 and prefix variables)
% 50.31/51.85
% 50.31/51.85 Proof:
% 50.31/51.85 ------
% 50.31/51.85 Translation into a non-clausal matrix:
% 50.31/51.85 [(2 ^ _165297) ^ [] ^ [] : [4 ^ _165297 : [(5 ^ _165297) ^ [_165440] ^ [] : [-(p2) : -([_165440]), 9 ^ _165297 : [(10 ^ _165297) ^ [_165573] ^ [] : [p1 : [_165440, _165573]]], 13 ^ _165297 : [(14 ^ _165297) ^ [_165698] ^ [] : [p1 : [_165440, 11 ^ [_165440], _165698]]]]], 18 ^ _165297 : [(19 ^ _165297) ^ [_165893] ^ [] : [-(p1) : -([_165893, 27 ^ [_165893]]), p2 : [_165893], p2 : [_165893, 24 ^ [_165893]]]]], (31 ^ _165297) ^ [] ^ [] : [33 ^ _165297 : [(34 ^ _165297) ^ [_166389] ^ [] : [-(p2) : -([_166389]), 37 ^ _165297 : [(38 ^ _165297) ^ [] ^ [] : [-(p1) : -([_166389])], (41 ^ _165297) ^ [] ^ [] : [p2 : [_166389, 39 ^ [_166389]]]], 43 ^ _165297 : [(44 ^ _165297) ^ [] ^ [] : [-(p1) : -([_166389, 42 ^ [_166389]])], (47 ^ _165297) ^ [] ^ [] : [p2 : [_166389, 42 ^ [_166389], 45 ^ [_166389]]]]]], 51 ^ _165297 : [(52 ^ _165297) ^ [_167057] ^ [] : [p2 : [_167057], p2 : [_167057, 57 ^ [_167057]], p1 : [_167057], 65 ^ _165297 : [(66 ^ _165297) ^ [_167477] ^ [] : [-(p2) : -([_167057, _167477])]]]]], (68 ^ _165297) ^ [] ^ [] : [70 ^ _165297 : [(71 ^ _165297) ^ [_167663] ^ [] : [-(p3) : -([_167663]), 75 ^ _165297 : [(76 ^ _165297) ^ [_167796] ^ [] : [p2 : [_167663, _167796]]], 79 ^ _165297 : [(80 ^ _165297) ^ [_167921] ^ [] : [p2 : [_167663, 77 ^ [_167663], _167921]]]]], 84 ^ _165297 : [(85 ^ _165297) ^ [_168116] ^ [] : [-(p2) : -([_168116, 93 ^ [_168116]]), p3 : [_168116], p3 : [_168116, 90 ^ [_168116]]]]], (97 ^ _165297) ^ [] ^ [] : [99 ^ _165297 : [(100 ^ _165297) ^ [_168612] ^ [] : [-(p3) : -([_168612]), 103 ^ _165297 : [(104 ^ _165297) ^ [] ^ [] : [-(p2) : -([_168612])], (107 ^ _165297) ^ [] ^ [] : [p3 : [_168612, 105 ^ [_168612]]]], 109 ^ _165297 : [(110 ^ _165297) ^ [] ^ [] : [-(p2) : -([_168612, 108 ^ [_168612]])], (113 ^ _165297) ^ [] ^ [] : [p3 : [_168612, 108 ^ [_168612], 111 ^ [_168612]]]]]], 117 ^ _165297 : [(118 ^ _165297) ^ [_169280] ^ [] : [p3 : [_169280], p3 : [_169280, 123 ^ [_169280]], p2 : [_169280], 131 ^ _165297 : [(132 ^ _165297) ^ [_169700] ^ [] : [-(p3) : -([_169280, _169700])]]]]], (134 ^ _165297) ^ [] ^ [] : [136 ^ _165297 : [(137 ^ _165297) ^ [_169886] ^ [] : [-(p4) : -([_169886]), 141 ^ _165297 : [(142 ^ _165297) ^ [_170019] ^ [] : [p3 : [_169886, _170019]]], 145 ^ _165297 : [(146 ^ _165297) ^ [_170144] ^ [] : [p3 : [_169886, 143 ^ [_169886], _170144]]]]], 150 ^ _165297 : [(151 ^ _165297) ^ [_170339] ^ [] : [-(p3) : -([_170339, 159 ^ [_170339]]), p4 : [_170339], p4 : [_170339, 156 ^ [_170339]]]]], (163 ^ _165297) ^ [] ^ [] : [165 ^ _165297 : [(166 ^ _165297) ^ [_170835] ^ [] : [-(p4) : -([_170835]), 169 ^ _165297 : [(170 ^ _165297) ^ [] ^ [] : [-(p3) : -([_170835])], (173 ^ _165297) ^ [] ^ [] : [p4 : [_170835, 171 ^ [_170835]]]], 175 ^ _165297 : [(176 ^ _165297) ^ [] ^ [] : [-(p3) : -([_170835, 174 ^ [_170835]])], (179 ^ _165297) ^ [] ^ [] : [p4 : [_170835, 174 ^ [_170835], 177 ^ [_170835]]]]]], 183 ^ _165297 : [(184 ^ _165297) ^ [_171503] ^ [] : [p4 : [_171503], p4 : [_171503, 189 ^ [_171503]], p3 : [_171503], 197 ^ _165297 : [(198 ^ _165297) ^ [_171923] ^ [] : [-(p4) : -([_171503, _171923])]]]]], (200 ^ _165297) ^ [] ^ [] : [202 ^ _165297 : [(203 ^ _165297) ^ [_172109] ^ [] : [-(p5) : -([_172109]), 207 ^ _165297 : [(208 ^ _165297) ^ [_172242] ^ [] : [p4 : [_172109, _172242]]], 211 ^ _165297 : [(212 ^ _165297) ^ [_172367] ^ [] : [p4 : [_172109, 209 ^ [_172109], _172367]]]]], 216 ^ _165297 : [(217 ^ _165297) ^ [_172562] ^ [] : [-(p4) : -([_172562, 225 ^ [_172562]]), p5 : [_172562], p5 : [_172562, 222 ^ [_172562]]]]], (229 ^ _165297) ^ [] ^ [] : [231 ^ _165297 : [(232 ^ _165297) ^ [_173058] ^ [] : [-(p5) : -([_173058]), 235 ^ _165297 : [(236 ^ _165297) ^ [] ^ [] : [-(p4) : -([_173058])], (239 ^ _165297) ^ [] ^ [] : [p5 : [_173058, 237 ^ [_173058]]]], 241 ^ _165297 : [(242 ^ _165297) ^ [] ^ [] : [-(p4) : -([_173058, 240 ^ [_173058]])], (245 ^ _165297) ^ [] ^ [] : [p5 : [_173058, 240 ^ [_173058], 243 ^ [_173058]]]]]], 249 ^ _165297 : [(250 ^ _165297) ^ [_173726] ^ [] : [p5 : [_173726], p5 : [_173726, 255 ^ [_173726]], p4 : [_173726], 263 ^ _165297 : [(264 ^ _165297) ^ [_174146] ^ [] : [-(p5) : -([_173726, _174146])]]]]], (266 ^ _165297) ^ [] ^ [] : [268 ^ _165297 : [(269 ^ _165297) ^ [_174332] ^ [] : [-(p6) : -([_174332]), 273 ^ _165297 : [(274 ^ _165297) ^ [_174465] ^ [] : [p5 : [_174332, _174465]]], 277 ^ _165297 : [(278 ^ _165297) ^ [_174590] ^ [] : [p5 : [_174332, 275 ^ [_174332], _174590]]]]], 282 ^ _165297 : [(283 ^ _165297) ^ [_174785] ^ [] : [-(p5) : -([_174785, 291 ^ [_174785]]), p6 : [_174785], p6 : [_174785, 288 ^ [_174785]]]]], (295 ^ _165297) ^ [] ^ [] : [297 ^ _165297 : [(298 ^ _165297) ^ [_175281] ^ [] : [-(p6) : -([_175281]), 301 ^ _165297 : [(302 ^ _165297) ^ [] ^ [] : [-(p5) : -([_175281])], (305 ^ _165297) ^ [] ^ [] : [p6 : [_175281, 303 ^ [_175281]]]], 307 ^ _165297 : [(308 ^ _165297) ^ [] ^ [] : [-(p5) : -([_175281, 306 ^ [_175281]])], (311 ^ _165297) ^ [] ^ [] : [p6 : [_175281, 306 ^ [_175281], 309 ^ [_175281]]]]]], 315 ^ _165297 : [(316 ^ _165297) ^ [_175949] ^ [] : [p6 : [_175949], p6 : [_175949, 321 ^ [_175949]], p5 : [_175949], 329 ^ _165297 : [(330 ^ _165297) ^ [_176369] ^ [] : [-(p6) : -([_175949, _176369])]]]]], (332 ^ _165297) ^ [] ^ [] : [334 ^ _165297 : [(335 ^ _165297) ^ [_176555] ^ [] : [-(p7) : -([_176555]), 339 ^ _165297 : [(340 ^ _165297) ^ [_176688] ^ [] : [p6 : [_176555, _176688]]], 343 ^ _165297 : [(344 ^ _165297) ^ [_176813] ^ [] : [p6 : [_176555, 341 ^ [_176555], _176813]]]]], 348 ^ _165297 : [(349 ^ _165297) ^ [_177008] ^ [] : [-(p6) : -([_177008, 357 ^ [_177008]]), p7 : [_177008], p7 : [_177008, 354 ^ [_177008]]]]], (361 ^ _165297) ^ [] ^ [] : [363 ^ _165297 : [(364 ^ _165297) ^ [_177504] ^ [] : [-(p7) : -([_177504]), 367 ^ _165297 : [(368 ^ _165297) ^ [] ^ [] : [-(p6) : -([_177504])], (371 ^ _165297) ^ [] ^ [] : [p7 : [_177504, 369 ^ [_177504]]]], 373 ^ _165297 : [(374 ^ _165297) ^ [] ^ [] : [-(p6) : -([_177504, 372 ^ [_177504]])], (377 ^ _165297) ^ [] ^ [] : [p7 : [_177504, 372 ^ [_177504], 375 ^ [_177504]]]]]], 381 ^ _165297 : [(382 ^ _165297) ^ [_178172] ^ [] : [p7 : [_178172], p7 : [_178172, 387 ^ [_178172]], p6 : [_178172], 395 ^ _165297 : [(396 ^ _165297) ^ [_178592] ^ [] : [-(p7) : -([_178172, _178592])]]]]], (398 ^ _165297) ^ [] ^ [] : [400 ^ _165297 : [(401 ^ _165297) ^ [_178778] ^ [] : [-(p8) : -([_178778]), 405 ^ _165297 : [(406 ^ _165297) ^ [_178911] ^ [] : [p7 : [_178778, _178911]]], 409 ^ _165297 : [(410 ^ _165297) ^ [_179036] ^ [] : [p7 : [_178778, 407 ^ [_178778], _179036]]]]], 414 ^ _165297 : [(415 ^ _165297) ^ [_179231] ^ [] : [-(p7) : -([_179231, 423 ^ [_179231]]), p8 : [_179231], p8 : [_179231, 420 ^ [_179231]]]]], (427 ^ _165297) ^ [] ^ [] : [429 ^ _165297 : [(430 ^ _165297) ^ [_179727] ^ [] : [-(p8) : -([_179727]), 433 ^ _165297 : [(434 ^ _165297) ^ [] ^ [] : [-(p7) : -([_179727])], (437 ^ _165297) ^ [] ^ [] : [p8 : [_179727, 435 ^ [_179727]]]], 439 ^ _165297 : [(440 ^ _165297) ^ [] ^ [] : [-(p7) : -([_179727, 438 ^ [_179727]])], (443 ^ _165297) ^ [] ^ [] : [p8 : [_179727, 438 ^ [_179727], 441 ^ [_179727]]]]]], 447 ^ _165297 : [(448 ^ _165297) ^ [_180395] ^ [] : [p8 : [_180395], p8 : [_180395, 453 ^ [_180395]], p7 : [_180395], 461 ^ _165297 : [(462 ^ _165297) ^ [_180815] ^ [] : [-(p8) : -([_180395, _180815])]]]]], (464 ^ _165297) ^ [] ^ [] : [466 ^ _165297 : [(467 ^ _165297) ^ [_181001] ^ [] : [-(p9) : -([_181001]), 471 ^ _165297 : [(472 ^ _165297) ^ [_181134] ^ [] : [p8 : [_181001, _181134]]], 475 ^ _165297 : [(476 ^ _165297) ^ [_181259] ^ [] : [p8 : [_181001, 473 ^ [_181001], _181259]]]]], 480 ^ _165297 : [(481 ^ _165297) ^ [_181454] ^ [] : [-(p8) : -([_181454, 489 ^ [_181454]]), p9 : [_181454], p9 : [_181454, 486 ^ [_181454]]]]], (493 ^ _165297) ^ [] ^ [] : [495 ^ _165297 : [(496 ^ _165297) ^ [_181950] ^ [] : [-(p9) : -([_181950]), 499 ^ _165297 : [(500 ^ _165297) ^ [] ^ [] : [-(p8) : -([_181950])], (503 ^ _165297) ^ [] ^ [] : [p9 : [_181950, 501 ^ [_181950]]]], 505 ^ _165297 : [(506 ^ _165297) ^ [] ^ [] : [-(p8) : -([_181950, 504 ^ [_181950]])], (509 ^ _165297) ^ [] ^ [] : [p9 : [_181950, 504 ^ [_181950], 507 ^ [_181950]]]]]], 513 ^ _165297 : [(514 ^ _165297) ^ [_182618] ^ [] : [p9 : [_182618], p9 : [_182618, 519 ^ [_182618]], p8 : [_182618], 527 ^ _165297 : [(528 ^ _165297) ^ [_183038] ^ [] : [-(p9) : -([_182618, _183038])]]]]], (530 ^ _165297) ^ [] ^ [] : [532 ^ _165297 : [(533 ^ _165297) ^ [_183224] ^ [] : [-(p10) : -([_183224]), 537 ^ _165297 : [(538 ^ _165297) ^ [_183357] ^ [] : [p9 : [_183224, _183357]]], 541 ^ _165297 : [(542 ^ _165297) ^ [_183482] ^ [] : [p9 : [_183224, 539 ^ [_183224], _183482]]]]], 546 ^ _165297 : [(547 ^ _165297) ^ [_183677] ^ [] : [-(p9) : -([_183677, 555 ^ [_183677]]), p10 : [_183677], p10 : [_183677, 552 ^ [_183677]]]]], (559 ^ _165297) ^ [] ^ [] : [561 ^ _165297 : [(562 ^ _165297) ^ [_184173] ^ [] : [-(p10) : -([_184173]), 565 ^ _165297 : [(566 ^ _165297) ^ [] ^ [] : [-(p9) : -([_184173])], (569 ^ _165297) ^ [] ^ [] : [p10 : [_184173, 567 ^ [_184173]]]], 571 ^ _165297 : [(572 ^ _165297) ^ [] ^ [] : [-(p9) : -([_184173, 570 ^ [_184173]])], (575 ^ _165297) ^ [] ^ [] : [p10 : [_184173, 570 ^ [_184173], 573 ^ [_184173]]]]]], 579 ^ _165297 : [(580 ^ _165297) ^ [_184841] ^ [] : [p10 : [_184841], p10 : [_184841, 585 ^ [_184841]], p9 : [_184841], 593 ^ _165297 : [(594 ^ _165297) ^ [_185261] ^ [] : [-(p10) : -([_184841, _185261])]]]]], (596 ^ _165297) ^ [] ^ [] : [598 ^ _165297 : [(599 ^ _165297) ^ [_185447] ^ [] : [-(p11) : -([_185447]), 603 ^ _165297 : [(604 ^ _165297) ^ [_185580] ^ [] : [p10 : [_185447, _185580]]], 607 ^ _165297 : [(608 ^ _165297) ^ [_185705] ^ [] : [p10 : [_185447, 605 ^ [_185447], _185705]]]]], 612 ^ _165297 : [(613 ^ _165297) ^ [_185900] ^ [] : [-(p10) : -([_185900, 621 ^ [_185900]]), p11 : [_185900], p11 : [_185900, 618 ^ [_185900]]]]], (625 ^ _165297) ^ [] ^ [] : [627 ^ _165297 : [(628 ^ _165297) ^ [_186396] ^ [] : [-(p11) : -([_186396]), 631 ^ _165297 : [(632 ^ _165297) ^ [] ^ [] : [-(p10) : -([_186396])], (635 ^ _165297) ^ [] ^ [] : [p11 : [_186396, 633 ^ [_186396]]]], 637 ^ _165297 : [(638 ^ _165297) ^ [] ^ [] : [-(p10) : -([_186396, 636 ^ [_186396]])], (641 ^ _165297) ^ [] ^ [] : [p11 : [_186396, 636 ^ [_186396], 639 ^ [_186396]]]]]], 645 ^ _165297 : [(646 ^ _165297) ^ [_187064] ^ [] : [p11 : [_187064], p11 : [_187064, 651 ^ [_187064]], p10 : [_187064], 659 ^ _165297 : [(660 ^ _165297) ^ [_187484] ^ [] : [-(p11) : -([_187064, _187484])]]]]], (662 ^ _165297) ^ [] ^ [] : [664 ^ _165297 : [(665 ^ _165297) ^ [_187670] ^ [] : [-(p12) : -([_187670]), 669 ^ _165297 : [(670 ^ _165297) ^ [_187803] ^ [] : [p11 : [_187670, _187803]]], 673 ^ _165297 : [(674 ^ _165297) ^ [_187928] ^ [] : [p11 : [_187670, 671 ^ [_187670], _187928]]]]], 678 ^ _165297 : [(679 ^ _165297) ^ [_188123] ^ [] : [-(p11) : -([_188123, 687 ^ [_188123]]), p12 : [_188123], p12 : [_188123, 684 ^ [_188123]]]]], (691 ^ _165297) ^ [] ^ [] : [693 ^ _165297 : [(694 ^ _165297) ^ [_188619] ^ [] : [-(p12) : -([_188619]), 697 ^ _165297 : [(698 ^ _165297) ^ [] ^ [] : [-(p11) : -([_188619])], (701 ^ _165297) ^ [] ^ [] : [p12 : [_188619, 699 ^ [_188619]]]], 703 ^ _165297 : [(704 ^ _165297) ^ [] ^ [] : [-(p11) : -([_188619, 702 ^ [_188619]])], (707 ^ _165297) ^ [] ^ [] : [p12 : [_188619, 702 ^ [_188619], 705 ^ [_188619]]]]]], 711 ^ _165297 : [(712 ^ _165297) ^ [_189287] ^ [] : [p12 : [_189287], p12 : [_189287, 717 ^ [_189287]], p11 : [_189287], 725 ^ _165297 : [(726 ^ _165297) ^ [_189707] ^ [] : [-(p12) : -([_189287, _189707])]]]]], (728 ^ _165297) ^ [] ^ [] : [730 ^ _165297 : [(731 ^ _165297) ^ [_189893] ^ [] : [-(p13) : -([_189893]), 735 ^ _165297 : [(736 ^ _165297) ^ [_190026] ^ [] : [p12 : [_189893, _190026]]], 739 ^ _165297 : [(740 ^ _165297) ^ [_190151] ^ [] : [p12 : [_189893, 737 ^ [_189893], _190151]]]]], 744 ^ _165297 : [(745 ^ _165297) ^ [_190346] ^ [] : [-(p12) : -([_190346, 753 ^ [_190346]]), p13 : [_190346], p13 : [_190346, 750 ^ [_190346]]]]], (757 ^ _165297) ^ [] ^ [] : [759 ^ _165297 : [(760 ^ _165297) ^ [_190842] ^ [] : [-(p13) : -([_190842]), 763 ^ _165297 : [(764 ^ _165297) ^ [] ^ [] : [-(p12) : -([_190842])], (767 ^ _165297) ^ [] ^ [] : [p13 : [_190842, 765 ^ [_190842]]]], 769 ^ _165297 : [(770 ^ _165297) ^ [] ^ [] : [-(p12) : -([_190842, 768 ^ [_190842]])], (773 ^ _165297) ^ [] ^ [] : [p13 : [_190842, 768 ^ [_190842], 771 ^ [_190842]]]]]], 777 ^ _165297 : [(778 ^ _165297) ^ [_191510] ^ [] : [p13 : [_191510], p13 : [_191510, 783 ^ [_191510]], p12 : [_191510], 791 ^ _165297 : [(792 ^ _165297) ^ [_191930] ^ [] : [-(p13) : -([_191510, _191930])]]]]], (794 ^ _165297) ^ [] ^ [] : [796 ^ _165297 : [(797 ^ _165297) ^ [_192116] ^ [] : [-(p14) : -([_192116]), 801 ^ _165297 : [(802 ^ _165297) ^ [_192249] ^ [] : [p13 : [_192116, _192249]]], 805 ^ _165297 : [(806 ^ _165297) ^ [_192374] ^ [] : [p13 : [_192116, 803 ^ [_192116], _192374]]]]], 810 ^ _165297 : [(811 ^ _165297) ^ [_192569] ^ [] : [-(p13) : -([_192569, 819 ^ [_192569]]), p14 : [_192569], p14 : [_192569, 816 ^ [_192569]]]]], (823 ^ _165297) ^ [] ^ [] : [825 ^ _165297 : [(826 ^ _165297) ^ [_193065] ^ [] : [-(p14) : -([_193065]), 829 ^ _165297 : [(830 ^ _165297) ^ [] ^ [] : [-(p13) : -([_193065])], (833 ^ _165297) ^ [] ^ [] : [p14 : [_193065, 831 ^ [_193065]]]], 835 ^ _165297 : [(836 ^ _165297) ^ [] ^ [] : [-(p13) : -([_193065, 834 ^ [_193065]])], (839 ^ _165297) ^ [] ^ [] : [p14 : [_193065, 834 ^ [_193065], 837 ^ [_193065]]]]]], 843 ^ _165297 : [(844 ^ _165297) ^ [_193733] ^ [] : [p14 : [_193733], p14 : [_193733, 849 ^ [_193733]], p13 : [_193733], 857 ^ _165297 : [(858 ^ _165297) ^ [_194153] ^ [] : [-(p14) : -([_193733, _194153])]]]]], (860 ^ _165297) ^ [] ^ [] : [862 ^ _165297 : [(863 ^ _165297) ^ [_194339] ^ [] : [-(p15) : -([_194339]), 867 ^ _165297 : [(868 ^ _165297) ^ [_194472] ^ [] : [p14 : [_194339, _194472]]], 871 ^ _165297 : [(872 ^ _165297) ^ [_194597] ^ [] : [p14 : [_194339, 869 ^ [_194339], _194597]]]]], 876 ^ _165297 : [(877 ^ _165297) ^ [_194792] ^ [] : [-(p14) : -([_194792, 885 ^ [_194792]]), p15 : [_194792], p15 : [_194792, 882 ^ [_194792]]]]], (889 ^ _165297) ^ [] ^ [] : [891 ^ _165297 : [(892 ^ _165297) ^ [_195288] ^ [] : [-(p15) : -([_195288]), 895 ^ _165297 : [(896 ^ _165297) ^ [] ^ [] : [-(p14) : -([_195288])], (899 ^ _165297) ^ [] ^ [] : [p15 : [_195288, 897 ^ [_195288]]]], 901 ^ _165297 : [(902 ^ _165297) ^ [] ^ [] : [-(p14) : -([_195288, 900 ^ [_195288]])], (905 ^ _165297) ^ [] ^ [] : [p15 : [_195288, 900 ^ [_195288], 903 ^ [_195288]]]]]], 909 ^ _165297 : [(910 ^ _165297) ^ [_195956] ^ [] : [p15 : [_195956], p15 : [_195956, 915 ^ [_195956]], p14 : [_195956], 923 ^ _165297 : [(924 ^ _165297) ^ [_196376] ^ [] : [-(p15) : -([_195956, _196376])]]]]], (926 ^ _165297) ^ [] ^ [] : [928 ^ _165297 : [(929 ^ _165297) ^ [_196562] ^ [] : [-(p16) : -([_196562]), 933 ^ _165297 : [(934 ^ _165297) ^ [_196695] ^ [] : [p15 : [_196562, _196695]]], 937 ^ _165297 : [(938 ^ _165297) ^ [_196820] ^ [] : [p15 : [_196562, 935 ^ [_196562], _196820]]]]], 942 ^ _165297 : [(943 ^ _165297) ^ [_197015] ^ [] : [-(p15) : -([_197015, 951 ^ [_197015]]), p16 : [_197015], p16 : [_197015, 948 ^ [_197015]]]]], (955 ^ _165297) ^ [] ^ [] : [957 ^ _165297 : [(958 ^ _165297) ^ [_197511] ^ [] : [-(p16) : -([_197511]), 961 ^ _165297 : [(962 ^ _165297) ^ [] ^ [] : [-(p15) : -([_197511])], (965 ^ _165297) ^ [] ^ [] : [p16 : [_197511, 963 ^ [_197511]]]], 967 ^ _165297 : [(968 ^ _165297) ^ [] ^ [] : [-(p15) : -([_197511, 966 ^ [_197511]])], (971 ^ _165297) ^ [] ^ [] : [p16 : [_197511, 966 ^ [_197511], 969 ^ [_197511]]]]]], 975 ^ _165297 : [(976 ^ _165297) ^ [_198179] ^ [] : [p16 : [_198179], p16 : [_198179, 981 ^ [_198179]], p15 : [_198179], 989 ^ _165297 : [(990 ^ _165297) ^ [_198599] ^ [] : [-(p16) : -([_198179, _198599])]]]]], (992 ^ _165297) ^ [] ^ [] : [994 ^ _165297 : [(995 ^ _165297) ^ [_198785] ^ [] : [-(p17) : -([_198785]), 999 ^ _165297 : [(1000 ^ _165297) ^ [_198918] ^ [] : [p16 : [_198785, _198918]]], 1003 ^ _165297 : [(1004 ^ _165297) ^ [_199043] ^ [] : [p16 : [_198785, 1001 ^ [_198785], _199043]]]]], 1008 ^ _165297 : [(1009 ^ _165297) ^ [_199238] ^ [] : [-(p16) : -([_199238, 1017 ^ [_199238]]), p17 : [_199238], p17 : [_199238, 1014 ^ [_199238]]]]], (1021 ^ _165297) ^ [] ^ [] : [1023 ^ _165297 : [(1024 ^ _165297) ^ [_199734] ^ [] : [-(p17) : -([_199734]), 1027 ^ _165297 : [(1028 ^ _165297) ^ [] ^ [] : [-(p16) : -([_199734])], (1031 ^ _165297) ^ [] ^ [] : [p17 : [_199734, 1029 ^ [_199734]]]], 1033 ^ _165297 : [(1034 ^ _165297) ^ [] ^ [] : [-(p16) : -([_199734, 1032 ^ [_199734]])], (1037 ^ _165297) ^ [] ^ [] : [p17 : [_199734, 1032 ^ [_199734], 1035 ^ [_199734]]]]]], 1041 ^ _165297 : [(1042 ^ _165297) ^ [_200402] ^ [] : [p17 : [_200402], p17 : [_200402, 1047 ^ [_200402]], p16 : [_200402], 1055 ^ _165297 : [(1056 ^ _165297) ^ [_200822] ^ [] : [-(p17) : -([_200402, _200822])]]]]], (1058 ^ _165297) ^ [] ^ [] : [1060 ^ _165297 : [(1061 ^ _165297) ^ [_201008] ^ [] : [-(p18) : -([_201008]), 1065 ^ _165297 : [(1066 ^ _165297) ^ [_201141] ^ [] : [p17 : [_201008, _201141]]], 1069 ^ _165297 : [(1070 ^ _165297) ^ [_201266] ^ [] : [p17 : [_201008, 1067 ^ [_201008], _201266]]]]], 1074 ^ _165297 : [(1075 ^ _165297) ^ [_201461] ^ [] : [-(p17) : -([_201461, 1083 ^ [_201461]]), p18 : [_201461], p18 : [_201461, 1080 ^ [_201461]]]]], (1087 ^ _165297) ^ [] ^ [] : [1089 ^ _165297 : [(1090 ^ _165297) ^ [_201957] ^ [] : [-(p18) : -([_201957]), 1093 ^ _165297 : [(1094 ^ _165297) ^ [] ^ [] : [-(p17) : -([_201957])], (1097 ^ _165297) ^ [] ^ [] : [p18 : [_201957, 1095 ^ [_201957]]]], 1099 ^ _165297 : [(1100 ^ _165297) ^ [] ^ [] : [-(p17) : -([_201957, 1098 ^ [_201957]])], (1103 ^ _165297) ^ [] ^ [] : [p18 : [_201957, 1098 ^ [_201957], 1101 ^ [_201957]]]]]], 1107 ^ _165297 : [(1108 ^ _165297) ^ [_202625] ^ [] : [p18 : [_202625], p18 : [_202625, 1113 ^ [_202625]], p17 : [_202625], 1121 ^ _165297 : [(1122 ^ _165297) ^ [_203045] ^ [] : [-(p18) : -([_202625, _203045])]]]]], (1124 ^ _165297) ^ [] ^ [] : [1126 ^ _165297 : [(1127 ^ _165297) ^ [_203231] ^ [] : [-(p19) : -([_203231]), 1131 ^ _165297 : [(1132 ^ _165297) ^ [_203364] ^ [] : [p18 : [_203231, _203364]]], 1135 ^ _165297 : [(1136 ^ _165297) ^ [_203489] ^ [] : [p18 : [_203231, 1133 ^ [_203231], _203489]]]]], 1140 ^ _165297 : [(1141 ^ _165297) ^ [_203684] ^ [] : [-(p18) : -([_203684, 1149 ^ [_203684]]), p19 : [_203684], p19 : [_203684, 1146 ^ [_203684]]]]], (1153 ^ _165297) ^ [] ^ [] : [1155 ^ _165297 : [(1156 ^ _165297) ^ [_204180] ^ [] : [-(p19) : -([_204180]), 1159 ^ _165297 : [(1160 ^ _165297) ^ [] ^ [] : [-(p18) : -([_204180])], (1163 ^ _165297) ^ [] ^ [] : [p19 : [_204180, 1161 ^ [_204180]]]], 1165 ^ _165297 : [(1166 ^ _165297) ^ [] ^ [] : [-(p18) : -([_204180, 1164 ^ [_204180]])], (1169 ^ _165297) ^ [] ^ [] : [p19 : [_204180, 1164 ^ [_204180], 1167 ^ [_204180]]]]]], 1173 ^ _165297 : [(1174 ^ _165297) ^ [_204848] ^ [] : [p19 : [_204848], p19 : [_204848, 1179 ^ [_204848]], p18 : [_204848], 1187 ^ _165297 : [(1188 ^ _165297) ^ [_205268] ^ [] : [-(p19) : -([_204848, _205268])]]]]], (1192 ^ _165297) ^ [_205452] ^ [] : [-(p10) : -([1189 ^ [], _205452])], (1194 ^ _165297) ^ [] ^ [] : [p10 : [1189 ^ []]], (1198 ^ _165297) ^ [_205672] ^ [] : [-(p10) : -([1195 ^ [], _205672])], (1200 ^ _165297) ^ [] ^ [] : [p10 : [1195 ^ []]], (1202 ^ _165297) ^ [] ^ [] : [1204 ^ _165297 : [(1205 ^ _165297) ^ [_205894] ^ [] : [-(p21) : -([_205894]), 1209 ^ _165297 : [(1210 ^ _165297) ^ [_206027] ^ [] : [p20 : [_205894, _206027]]], 1213 ^ _165297 : [(1214 ^ _165297) ^ [_206152] ^ [] : [p20 : [_205894, 1211 ^ [_205894], _206152]]]]], 1218 ^ _165297 : [(1219 ^ _165297) ^ [_206347] ^ [] : [-(p20) : -([_206347, 1227 ^ [_206347]]), p21 : [_206347], p21 : [_206347, 1224 ^ [_206347]]]]], (1231 ^ _165297) ^ [] ^ [] : [1233 ^ _165297 : [(1234 ^ _165297) ^ [_206843] ^ [] : [-(p21) : -([_206843]), 1237 ^ _165297 : [(1238 ^ _165297) ^ [] ^ [] : [-(p20) : -([_206843])], (1241 ^ _165297) ^ [] ^ [] : [p21 : [_206843, 1239 ^ [_206843]]]], 1243 ^ _165297 : [(1244 ^ _165297) ^ [] ^ [] : [-(p20) : -([_206843, 1242 ^ [_206843]])], (1247 ^ _165297) ^ [] ^ [] : [p21 : [_206843, 1242 ^ [_206843], 1245 ^ [_206843]]]]]], 1251 ^ _165297 : [(1252 ^ _165297) ^ [_207511] ^ [] : [p21 : [_207511], p21 : [_207511, 1257 ^ [_207511]], p20 : [_207511], 1265 ^ _165297 : [(1266 ^ _165297) ^ [_207931] ^ [] : [-(p21) : -([_207511, _207931])]]]]], (1268 ^ _165297) ^ [] ^ [] : [1270 ^ _165297 : [(1271 ^ _165297) ^ [_208117] ^ [] : [-(p22) : -([_208117]), 1275 ^ _165297 : [(1276 ^ _165297) ^ [_208250] ^ [] : [p21 : [_208117, _208250]]], 1279 ^ _165297 : [(1280 ^ _165297) ^ [_208375] ^ [] : [p21 : [_208117, 1277 ^ [_208117], _208375]]]]], 1284 ^ _165297 : [(1285 ^ _165297) ^ [_208570] ^ [] : [-(p21) : -([_208570, 1293 ^ [_208570]]), p22 : [_208570], p22 : [_208570, 1290 ^ [_208570]]]]], (1297 ^ _165297) ^ [] ^ [] : [1299 ^ _165297 : [(1300 ^ _165297) ^ [_209066] ^ [] : [-(p22) : -([_209066]), 1303 ^ _165297 : [(1304 ^ _165297) ^ [] ^ [] : [-(p21) : -([_209066])], (1307 ^ _165297) ^ [] ^ [] : [p22 : [_209066, 1305 ^ [_209066]]]], 1309 ^ _165297 : [(1310 ^ _165297) ^ [] ^ [] : [-(p21) : -([_209066, 1308 ^ [_209066]])], (1313 ^ _165297) ^ [] ^ [] : [p22 : [_209066, 1308 ^ [_209066], 1311 ^ [_209066]]]]]], 1317 ^ _165297 : [(1318 ^ _165297) ^ [_209734] ^ [] : [p22 : [_209734], p22 : [_209734, 1323 ^ [_209734]], p21 : [_209734], 1331 ^ _165297 : [(1332 ^ _165297) ^ [_210154] ^ [] : [-(p22) : -([_209734, _210154])]]]]], (1334 ^ _165297) ^ [] ^ [] : [1336 ^ _165297 : [(1337 ^ _165297) ^ [_210340] ^ [] : [-(p23) : -([_210340]), 1341 ^ _165297 : [(1342 ^ _165297) ^ [_210473] ^ [] : [p22 : [_210340, _210473]]], 1345 ^ _165297 : [(1346 ^ _165297) ^ [_210598] ^ [] : [p22 : [_210340, 1343 ^ [_210340], _210598]]]]], 1350 ^ _165297 : [(1351 ^ _165297) ^ [_210793] ^ [] : [-(p22) : -([_210793, 1359 ^ [_210793]]), p23 : [_210793], p23 : [_210793, 1356 ^ [_210793]]]]], (1363 ^ _165297) ^ [] ^ [] : [1365 ^ _165297 : [(1366 ^ _165297) ^ [_211289] ^ [] : [-(p23) : -([_211289]), 1369 ^ _165297 : [(1370 ^ _165297) ^ [] ^ [] : [-(p22) : -([_211289])], (1373 ^ _165297) ^ [] ^ [] : [p23 : [_211289, 1371 ^ [_211289]]]], 1375 ^ _165297 : [(1376 ^ _165297) ^ [] ^ [] : [-(p22) : -([_211289, 1374 ^ [_211289]])], (1379 ^ _165297) ^ [] ^ [] : [p23 : [_211289, 1374 ^ [_211289], 1377 ^ [_211289]]]]]], 1383 ^ _165297 : [(1384 ^ _165297) ^ [_211957] ^ [] : [p23 : [_211957], p23 : [_211957, 1389 ^ [_211957]], p22 : [_211957], 1397 ^ _165297 : [(1398 ^ _165297) ^ [_212377] ^ [] : [-(p23) : -([_211957, _212377])]]]]], (1400 ^ _165297) ^ [] ^ [] : [1402 ^ _165297 : [(1403 ^ _165297) ^ [_212563] ^ [] : [-(p24) : -([_212563]), 1407 ^ _165297 : [(1408 ^ _165297) ^ [_212696] ^ [] : [p23 : [_212563, _212696]]], 1411 ^ _165297 : [(1412 ^ _165297) ^ [_212821] ^ [] : [p23 : [_212563, 1409 ^ [_212563], _212821]]]]], 1416 ^ _165297 : [(1417 ^ _165297) ^ [_213016] ^ [] : [-(p23) : -([_213016, 1425 ^ [_213016]]), p24 : [_213016], p24 : [_213016, 1422 ^ [_213016]]]]], (1429 ^ _165297) ^ [] ^ [] : [1431 ^ _165297 : [(1432 ^ _165297) ^ [_213512] ^ [] : [-(p24) : -([_213512]), 1435 ^ _165297 : [(1436 ^ _165297) ^ [] ^ [] : [-(p23) : -([_213512])], (1439 ^ _165297) ^ [] ^ [] : [p24 : [_213512, 1437 ^ [_213512]]]], 1441 ^ _165297 : [(1442 ^ _165297) ^ [] ^ [] : [-(p23) : -([_213512, 1440 ^ [_213512]])], (1445 ^ _165297) ^ [] ^ [] : [p24 : [_213512, 1440 ^ [_213512], 1443 ^ [_213512]]]]]], 1449 ^ _165297 : [(1450 ^ _165297) ^ [_214180] ^ [] : [p24 : [_214180], p24 : [_214180, 1455 ^ [_214180]], p23 : [_214180], 1463 ^ _165297 : [(1464 ^ _165297) ^ [_214600] ^ [] : [-(p24) : -([_214180, _214600])]]]]], (1466 ^ _165297) ^ [] ^ [] : [1468 ^ _165297 : [(1469 ^ _165297) ^ [_214786] ^ [] : [-(p25) : -([_214786]), 1473 ^ _165297 : [(1474 ^ _165297) ^ [_214919] ^ [] : [p24 : [_214786, _214919]]], 1477 ^ _165297 : [(1478 ^ _165297) ^ [_215044] ^ [] : [p24 : [_214786, 1475 ^ [_214786], _215044]]]]], 1482 ^ _165297 : [(1483 ^ _165297) ^ [_215239] ^ [] : [-(p24) : -([_215239, 1491 ^ [_215239]]), p25 : [_215239], p25 : [_215239, 1488 ^ [_215239]]]]], (1495 ^ _165297) ^ [] ^ [] : [1497 ^ _165297 : [(1498 ^ _165297) ^ [_215735] ^ [] : [-(p25) : -([_215735]), 1501 ^ _165297 : [(1502 ^ _165297) ^ [] ^ [] : [-(p24) : -([_215735])], (1505 ^ _165297) ^ [] ^ [] : [p25 : [_215735, 1503 ^ [_215735]]]], 1507 ^ _165297 : [(1508 ^ _165297) ^ [] ^ [] : [-(p24) : -([_215735, 1506 ^ [_215735]])], (1511 ^ _165297) ^ [] ^ [] : [p25 : [_215735, 1506 ^ [_215735], 1509 ^ [_215735]]]]]], 1515 ^ _165297 : [(1516 ^ _165297) ^ [_216403] ^ [] : [p25 : [_216403], p25 : [_216403, 1521 ^ [_216403]], p24 : [_216403], 1529 ^ _165297 : [(1530 ^ _165297) ^ [_216823] ^ [] : [-(p25) : -([_216403, _216823])]]]]], (1532 ^ _165297) ^ [] ^ [] : [1534 ^ _165297 : [(1535 ^ _165297) ^ [_217009] ^ [] : [-(p26) : -([_217009]), 1539 ^ _165297 : [(1540 ^ _165297) ^ [_217142] ^ [] : [p25 : [_217009, _217142]]], 1543 ^ _165297 : [(1544 ^ _165297) ^ [_217267] ^ [] : [p25 : [_217009, 1541 ^ [_217009], _217267]]]]], 1548 ^ _165297 : [(1549 ^ _165297) ^ [_217462] ^ [] : [-(p25) : -([_217462, 1557 ^ [_217462]]), p26 : [_217462], p26 : [_217462, 1554 ^ [_217462]]]]], (1561 ^ _165297) ^ [] ^ [] : [1563 ^ _165297 : [(1564 ^ _165297) ^ [_217958] ^ [] : [-(p26) : -([_217958]), 1567 ^ _165297 : [(1568 ^ _165297) ^ [] ^ [] : [-(p25) : -([_217958])], (1571 ^ _165297) ^ [] ^ [] : [p26 : [_217958, 1569 ^ [_217958]]]], 1573 ^ _165297 : [(1574 ^ _165297) ^ [] ^ [] : [-(p25) : -([_217958, 1572 ^ [_217958]])], (1577 ^ _165297) ^ [] ^ [] : [p26 : [_217958, 1572 ^ [_217958], 1575 ^ [_217958]]]]]], 1581 ^ _165297 : [(1582 ^ _165297) ^ [_218626] ^ [] : [p26 : [_218626], p26 : [_218626, 1587 ^ [_218626]], p25 : [_218626], 1595 ^ _165297 : [(1596 ^ _165297) ^ [_219046] ^ [] : [-(p26) : -([_218626, _219046])]]]]], (1598 ^ _165297) ^ [] ^ [] : [1600 ^ _165297 : [(1601 ^ _165297) ^ [_219232] ^ [] : [-(p27) : -([_219232]), 1605 ^ _165297 : [(1606 ^ _165297) ^ [_219365] ^ [] : [p26 : [_219232, _219365]]], 1609 ^ _165297 : [(1610 ^ _165297) ^ [_219490] ^ [] : [p26 : [_219232, 1607 ^ [_219232], _219490]]]]], 1614 ^ _165297 : [(1615 ^ _165297) ^ [_219685] ^ [] : [-(p26) : -([_219685, 1623 ^ [_219685]]), p27 : [_219685], p27 : [_219685, 1620 ^ [_219685]]]]], (1627 ^ _165297) ^ [] ^ [] : [1629 ^ _165297 : [(1630 ^ _165297) ^ [_220181] ^ [] : [-(p27) : -([_220181]), 1633 ^ _165297 : [(1634 ^ _165297) ^ [] ^ [] : [-(p26) : -([_220181])], (1637 ^ _165297) ^ [] ^ [] : [p27 : [_220181, 1635 ^ [_220181]]]], 1639 ^ _165297 : [(1640 ^ _165297) ^ [] ^ [] : [-(p26) : -([_220181, 1638 ^ [_220181]])], (1643 ^ _165297) ^ [] ^ [] : [p27 : [_220181, 1638 ^ [_220181], 1641 ^ [_220181]]]]]], 1647 ^ _165297 : [(1648 ^ _165297) ^ [_220849] ^ [] : [p27 : [_220849], p27 : [_220849, 1653 ^ [_220849]], p26 : [_220849], 1661 ^ _165297 : [(1662 ^ _165297) ^ [_221269] ^ [] : [-(p27) : -([_220849, _221269])]]]]], (1664 ^ _165297) ^ [] ^ [] : [1666 ^ _165297 : [(1667 ^ _165297) ^ [_221455] ^ [] : [-(p28) : -([_221455]), 1671 ^ _165297 : [(1672 ^ _165297) ^ [_221588] ^ [] : [p27 : [_221455, _221588]]], 1675 ^ _165297 : [(1676 ^ _165297) ^ [_221713] ^ [] : [p27 : [_221455, 1673 ^ [_221455], _221713]]]]], 1680 ^ _165297 : [(1681 ^ _165297) ^ [_221908] ^ [] : [-(p27) : -([_221908, 1689 ^ [_221908]]), p28 : [_221908], p28 : [_221908, 1686 ^ [_221908]]]]], (1693 ^ _165297) ^ [] ^ [] : [1695 ^ _165297 : [(1696 ^ _165297) ^ [_222404] ^ [] : [-(p28) : -([_222404]), 1699 ^ _165297 : [(1700 ^ _165297) ^ [] ^ [] : [-(p27) : -([_222404])], (1703 ^ _165297) ^ [] ^ [] : [p28 : [_222404, 1701 ^ [_222404]]]], 1705 ^ _165297 : [(1706 ^ _165297) ^ [] ^ [] : [-(p27) : -([_222404, 1704 ^ [_222404]])], (1709 ^ _165297) ^ [] ^ [] : [p28 : [_222404, 1704 ^ [_222404], 1707 ^ [_222404]]]]]], 1713 ^ _165297 : [(1714 ^ _165297) ^ [_223072] ^ [] : [p28 : [_223072], p28 : [_223072, 1719 ^ [_223072]], p27 : [_223072], 1727 ^ _165297 : [(1728 ^ _165297) ^ [_223492] ^ [] : [-(p28) : -([_223072, _223492])]]]]], (1730 ^ _165297) ^ [] ^ [] : [1732 ^ _165297 : [(1733 ^ _165297) ^ [_223678] ^ [] : [-(p29) : -([_223678]), 1737 ^ _165297 : [(1738 ^ _165297) ^ [_223811] ^ [] : [p28 : [_223678, _223811]]], 1741 ^ _165297 : [(1742 ^ _165297) ^ [_223936] ^ [] : [p28 : [_223678, 1739 ^ [_223678], _223936]]]]], 1746 ^ _165297 : [(1747 ^ _165297) ^ [_224131] ^ [] : [-(p28) : -([_224131, 1755 ^ [_224131]]), p29 : [_224131], p29 : [_224131, 1752 ^ [_224131]]]]], (1759 ^ _165297) ^ [] ^ [] : [1761 ^ _165297 : [(1762 ^ _165297) ^ [_224627] ^ [] : [-(p29) : -([_224627]), 1765 ^ _165297 : [(1766 ^ _165297) ^ [] ^ [] : [-(p28) : -([_224627])], (1769 ^ _165297) ^ [] ^ [] : [p29 : [_224627, 1767 ^ [_224627]]]], 1771 ^ _165297 : [(1772 ^ _165297) ^ [] ^ [] : [-(p28) : -([_224627, 1770 ^ [_224627]])], (1775 ^ _165297) ^ [] ^ [] : [p29 : [_224627, 1770 ^ [_224627], 1773 ^ [_224627]]]]]], 1779 ^ _165297 : [(1780 ^ _165297) ^ [_225295] ^ [] : [p29 : [_225295], p29 : [_225295, 1785 ^ [_225295]], p28 : [_225295], 1793 ^ _165297 : [(1794 ^ _165297) ^ [_225715] ^ [] : [-(p29) : -([_225295, _225715])]]]]], (1796 ^ _165297) ^ [] ^ [] : [1798 ^ _165297 : [(1799 ^ _165297) ^ [_225901] ^ [] : [-(p30) : -([_225901]), 1803 ^ _165297 : [(1804 ^ _165297) ^ [_226034] ^ [] : [p29 : [_225901, _226034]]], 1807 ^ _165297 : [(1808 ^ _165297) ^ [_226159] ^ [] : [p29 : [_225901, 1805 ^ [_225901], _226159]]]]], 1812 ^ _165297 : [(1813 ^ _165297) ^ [_226354] ^ [] : [-(p29) : -([_226354, 1821 ^ [_226354]]), p30 : [_226354], p30 : [_226354, 1818 ^ [_226354]]]]], (1825 ^ _165297) ^ [] ^ [] : [1827 ^ _165297 : [(1828 ^ _165297) ^ [_226850] ^ [] : [-(p30) : -([_226850]), 1831 ^ _165297 : [(1832 ^ _165297) ^ [] ^ [] : [-(p29) : -([_226850])], (1835 ^ _165297) ^ [] ^ [] : [p30 : [_226850, 1833 ^ [_226850]]]], 1837 ^ _165297 : [(1838 ^ _165297) ^ [] ^ [] : [-(p29) : -([_226850, 1836 ^ [_226850]])], (1841 ^ _165297) ^ [] ^ [] : [p30 : [_226850, 1836 ^ [_226850], 1839 ^ [_226850]]]]]], 1845 ^ _165297 : [(1846 ^ _165297) ^ [_227518] ^ [] : [p30 : [_227518], p30 : [_227518, 1851 ^ [_227518]], p29 : [_227518], 1859 ^ _165297 : [(1860 ^ _165297) ^ [_227938] ^ [] : [-(p30) : -([_227518, _227938])]]]]], (1862 ^ _165297) ^ [] ^ [] : [1864 ^ _165297 : [(1865 ^ _165297) ^ [_228124] ^ [] : [-(p31) : -([_228124]), 1869 ^ _165297 : [(1870 ^ _165297) ^ [_228257] ^ [] : [p30 : [_228124, _228257]]], 1873 ^ _165297 : [(1874 ^ _165297) ^ [_228382] ^ [] : [p30 : [_228124, 1871 ^ [_228124], _228382]]]]], 1878 ^ _165297 : [(1879 ^ _165297) ^ [_228577] ^ [] : [-(p30) : -([_228577, 1887 ^ [_228577]]), p31 : [_228577], p31 : [_228577, 1884 ^ [_228577]]]]], (1891 ^ _165297) ^ [] ^ [] : [1893 ^ _165297 : [(1894 ^ _165297) ^ [_229073] ^ [] : [-(p31) : -([_229073]), 1897 ^ _165297 : [(1898 ^ _165297) ^ [] ^ [] : [-(p30) : -([_229073])], (1901 ^ _165297) ^ [] ^ [] : [p31 : [_229073, 1899 ^ [_229073]]]], 1903 ^ _165297 : [(1904 ^ _165297) ^ [] ^ [] : [-(p30) : -([_229073, 1902 ^ [_229073]])], (1907 ^ _165297) ^ [] ^ [] : [p31 : [_229073, 1902 ^ [_229073], 1905 ^ [_229073]]]]]], 1911 ^ _165297 : [(1912 ^ _165297) ^ [_229741] ^ [] : [p31 : [_229741], p31 : [_229741, 1917 ^ [_229741]], p30 : [_229741], 1925 ^ _165297 : [(1926 ^ _165297) ^ [_230161] ^ [] : [-(p31) : -([_229741, _230161])]]]]], (1928 ^ _165297) ^ [] ^ [] : [1930 ^ _165297 : [(1931 ^ _165297) ^ [_230347] ^ [] : [-(p32) : -([_230347]), 1935 ^ _165297 : [(1936 ^ _165297) ^ [_230480] ^ [] : [p31 : [_230347, _230480]]], 1939 ^ _165297 : [(1940 ^ _165297) ^ [_230605] ^ [] : [p31 : [_230347, 1937 ^ [_230347], _230605]]]]], 1944 ^ _165297 : [(1945 ^ _165297) ^ [_230800] ^ [] : [-(p31) : -([_230800, 1953 ^ [_230800]]), p32 : [_230800], p32 : [_230800, 1950 ^ [_230800]]]]], (1957 ^ _165297) ^ [] ^ [] : [1959 ^ _165297 : [(1960 ^ _165297) ^ [_231296] ^ [] : [-(p32) : -([_231296]), 1963 ^ _165297 : [(1964 ^ _165297) ^ [] ^ [] : [-(p31) : -([_231296])], (1967 ^ _165297) ^ [] ^ [] : [p32 : [_231296, 1965 ^ [_231296]]]], 1969 ^ _165297 : [(1970 ^ _165297) ^ [] ^ [] : [-(p31) : -([_231296, 1968 ^ [_231296]])], (1973 ^ _165297) ^ [] ^ [] : [p32 : [_231296, 1968 ^ [_231296], 1971 ^ [_231296]]]]]], 1977 ^ _165297 : [(1978 ^ _165297) ^ [_231964] ^ [] : [p32 : [_231964], p32 : [_231964, 1983 ^ [_231964]], p31 : [_231964], 1991 ^ _165297 : [(1992 ^ _165297) ^ [_232384] ^ [] : [-(p32) : -([_231964, _232384])]]]]], (1994 ^ _165297) ^ [] ^ [] : [1996 ^ _165297 : [(1997 ^ _165297) ^ [_232570] ^ [] : [-(p33) : -([_232570]), 2001 ^ _165297 : [(2002 ^ _165297) ^ [_232703] ^ [] : [p32 : [_232570, _232703]]], 2005 ^ _165297 : [(2006 ^ _165297) ^ [_232828] ^ [] : [p32 : [_232570, 2003 ^ [_232570], _232828]]]]], 2010 ^ _165297 : [(2011 ^ _165297) ^ [_233023] ^ [] : [-(p32) : -([_233023, 2019 ^ [_233023]]), p33 : [_233023], p33 : [_233023, 2016 ^ [_233023]]]]], (2023 ^ _165297) ^ [] ^ [] : [2025 ^ _165297 : [(2026 ^ _165297) ^ [_233519] ^ [] : [-(p33) : -([_233519]), 2029 ^ _165297 : [(2030 ^ _165297) ^ [] ^ [] : [-(p32) : -([_233519])], (2033 ^ _165297) ^ [] ^ [] : [p33 : [_233519, 2031 ^ [_233519]]]], 2035 ^ _165297 : [(2036 ^ _165297) ^ [] ^ [] : [-(p32) : -([_233519, 2034 ^ [_233519]])], (2039 ^ _165297) ^ [] ^ [] : [p33 : [_233519, 2034 ^ [_233519], 2037 ^ [_233519]]]]]], 2043 ^ _165297 : [(2044 ^ _165297) ^ [_234187] ^ [] : [p33 : [_234187], p33 : [_234187, 2049 ^ [_234187]], p32 : [_234187], 2057 ^ _165297 : [(2058 ^ _165297) ^ [_234607] ^ [] : [-(p33) : -([_234187, _234607])]]]]], (2060 ^ _165297) ^ [] ^ [] : [2062 ^ _165297 : [(2063 ^ _165297) ^ [_234793] ^ [] : [-(p34) : -([_234793]), 2067 ^ _165297 : [(2068 ^ _165297) ^ [_234926] ^ [] : [p33 : [_234793, _234926]]], 2071 ^ _165297 : [(2072 ^ _165297) ^ [_235051] ^ [] : [p33 : [_234793, 2069 ^ [_234793], _235051]]]]], 2076 ^ _165297 : [(2077 ^ _165297) ^ [_235246] ^ [] : [-(p33) : -([_235246, 2085 ^ [_235246]]), p34 : [_235246], p34 : [_235246, 2082 ^ [_235246]]]]], (2089 ^ _165297) ^ [] ^ [] : [2091 ^ _165297 : [(2092 ^ _165297) ^ [_235742] ^ [] : [-(p34) : -([_235742]), 2095 ^ _165297 : [(2096 ^ _165297) ^ [] ^ [] : [-(p33) : -([_235742])], (2099 ^ _165297) ^ [] ^ [] : [p34 : [_235742, 2097 ^ [_235742]]]], 2101 ^ _165297 : [(2102 ^ _165297) ^ [] ^ [] : [-(p33) : -([_235742, 2100 ^ [_235742]])], (2105 ^ _165297) ^ [] ^ [] : [p34 : [_235742, 2100 ^ [_235742], 2103 ^ [_235742]]]]]], 2109 ^ _165297 : [(2110 ^ _165297) ^ [_236410] ^ [] : [p34 : [_236410], p34 : [_236410, 2115 ^ [_236410]], p33 : [_236410], 2123 ^ _165297 : [(2124 ^ _165297) ^ [_236830] ^ [] : [-(p34) : -([_236410, _236830])]]]]], (2126 ^ _165297) ^ [] ^ [] : [2128 ^ _165297 : [(2129 ^ _165297) ^ [_237016] ^ [] : [-(p35) : -([_237016]), 2133 ^ _165297 : [(2134 ^ _165297) ^ [_237149] ^ [] : [p34 : [_237016, _237149]]], 2137 ^ _165297 : [(2138 ^ _165297) ^ [_237274] ^ [] : [p34 : [_237016, 2135 ^ [_237016], _237274]]]]], 2142 ^ _165297 : [(2143 ^ _165297) ^ [_237469] ^ [] : [-(p34) : -([_237469, 2151 ^ [_237469]]), p35 : [_237469], p35 : [_237469, 2148 ^ [_237469]]]]], (2155 ^ _165297) ^ [] ^ [] : [2157 ^ _165297 : [(2158 ^ _165297) ^ [_237965] ^ [] : [-(p35) : -([_237965]), 2161 ^ _165297 : [(2162 ^ _165297) ^ [] ^ [] : [-(p34) : -([_237965])], (2165 ^ _165297) ^ [] ^ [] : [p35 : [_237965, 2163 ^ [_237965]]]], 2167 ^ _165297 : [(2168 ^ _165297) ^ [] ^ [] : [-(p34) : -([_237965, 2166 ^ [_237965]])], (2171 ^ _165297) ^ [] ^ [] : [p35 : [_237965, 2166 ^ [_237965], 2169 ^ [_237965]]]]]], 2175 ^ _165297 : [(2176 ^ _165297) ^ [_238633] ^ [] : [p35 : [_238633], p35 : [_238633, 2181 ^ [_238633]], p34 : [_238633], 2189 ^ _165297 : [(2190 ^ _165297) ^ [_239053] ^ [] : [-(p35) : -([_238633, _239053])]]]]], (2192 ^ _165297) ^ [] ^ [] : [2194 ^ _165297 : [(2195 ^ _165297) ^ [_239239] ^ [] : [-(p36) : -([_239239]), 2199 ^ _165297 : [(2200 ^ _165297) ^ [_239372] ^ [] : [p35 : [_239239, _239372]]], 2203 ^ _165297 : [(2204 ^ _165297) ^ [_239497] ^ [] : [p35 : [_239239, 2201 ^ [_239239], _239497]]]]], 2208 ^ _165297 : [(2209 ^ _165297) ^ [_239692] ^ [] : [-(p35) : -([_239692, 2217 ^ [_239692]]), p36 : [_239692], p36 : [_239692, 2214 ^ [_239692]]]]], (2221 ^ _165297) ^ [] ^ [] : [2223 ^ _165297 : [(2224 ^ _165297) ^ [_240188] ^ [] : [-(p36) : -([_240188]), 2227 ^ _165297 : [(2228 ^ _165297) ^ [] ^ [] : [-(p35) : -([_240188])], (2231 ^ _165297) ^ [] ^ [] : [p36 : [_240188, 2229 ^ [_240188]]]], 2233 ^ _165297 : [(2234 ^ _165297) ^ [] ^ [] : [-(p35) : -([_240188, 2232 ^ [_240188]])], (2237 ^ _165297) ^ [] ^ [] : [p36 : [_240188, 2232 ^ [_240188], 2235 ^ [_240188]]]]]], 2241 ^ _165297 : [(2242 ^ _165297) ^ [_240856] ^ [] : [p36 : [_240856], p36 : [_240856, 2247 ^ [_240856]], p35 : [_240856], 2255 ^ _165297 : [(2256 ^ _165297) ^ [_241276] ^ [] : [-(p36) : -([_240856, _241276])]]]]], (2258 ^ _165297) ^ [] ^ [] : [2260 ^ _165297 : [(2261 ^ _165297) ^ [_241462] ^ [] : [-(p37) : -([_241462]), 2265 ^ _165297 : [(2266 ^ _165297) ^ [_241595] ^ [] : [p36 : [_241462, _241595]]], 2269 ^ _165297 : [(2270 ^ _165297) ^ [_241720] ^ [] : [p36 : [_241462, 2267 ^ [_241462], _241720]]]]], 2274 ^ _165297 : [(2275 ^ _165297) ^ [_241915] ^ [] : [-(p36) : -([_241915, 2283 ^ [_241915]]), p37 : [_241915], p37 : [_241915, 2280 ^ [_241915]]]]], (2287 ^ _165297) ^ [] ^ [] : [2289 ^ _165297 : [(2290 ^ _165297) ^ [_242388] ^ [] : [-(p37) : -([_242388]), 2293 ^ _165297 : [(2294 ^ _165297) ^ [] ^ [] : [-(p36) : -([_242388])], (2297 ^ _165297) ^ [] ^ [] : [p37 : [_242388, 2295 ^ [_242388]]]], 2299 ^ _165297 : [(2300 ^ _165297) ^ [] ^ [] : [-(p36) : -([_242388, 2298 ^ [_242388]])], (2303 ^ _165297) ^ [] ^ [] : [p37 : [_242388, 2298 ^ [_242388], 2301 ^ [_242388]]]]]], 2307 ^ _165297 : [(2308 ^ _165297) ^ [_243056] ^ [] : [p37 : [_243056], p37 : [_243056, 2313 ^ [_243056]], p36 : [_243056], 2321 ^ _165297 : [(2322 ^ _165297) ^ [_243476] ^ [] : [-(p37) : -([_243056, _243476])]]]]]]
% 50.31/51.85
% 50.31/51.85 We prove that the given matrix is valid, i.e. for
% 50.31/51.85 a given substitution it evaluates to true for all
% 50.31/51.85 interpretations. A matrix is true iff at least one
% 50.31/51.85 of its clauses is true; a clause is true iff all of
% 50.31/51.85 its elements (literals and submatrices) are true.
% 50.31/51.85
% 50.31/51.85 The proof is by contradiction:
% 50.31/51.85 Assume there is an interpretation so that the given
% 50.31/51.85 matrix evaluates to false. Then in each clause there
% 50.31/51.85 has to be at least one element that is false.
% 50.31/51.85
% 50.31/51.85 Then clause (1194 ^ 0) is false if at least one of the following is false:
% 50.31/51.85 [p10 : [1189 ^ []]]
% 50.31/51.85 1 Assume p10 : [1189 ^ [], []] is false.
% 50.31/51.85 Then clause (1192 ^ 1) under the substitution [[_205452], [[]]]
% 50.31/51.85 is true.
% 50.31/51.85
% 50.31/51.85 Therefore there is no interpretation that makes the
% 50.31/51.85 given matrix false. Hence the given matrix is valid.
% 50.31/51.85 q.e.d.
% 50.31/51.85 ------------------------------------------------------
% 50.31/51.85 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.cmSSjqqhWb/theBenchmark.p.qmf
% 50.31/51.85 % nanoCoP-M exiting
%------------------------------------------------------------------------------