%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP091_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n028.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 45.56s 46.09s
% Output : Proof 53.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYP091_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : run_nanocopm %s %d
% 0.14/0.34 % Computer : n028.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon May 4 17:26:45 EDT 2026
% 0.14/0.34 % CPUTime :
% 0.30/0.48 % Logic is d
% 0.30/0.48 % Designation is rigid
% 0.30/0.49 % Terms are local
% 0.30/0.49 % Domains are const
% 0.30/0.50 ------------ Start QMF file ---------------
% 0.30/0.51 %------------------------------------------------------------------------------
% 0.30/0.51 % File : SYP091_1 : TPTP v9.3.0. Released v9.3.0.
% 0.30/0.51 % Domain : Syntactic
% 0.30/0.51 % Problem : Logic KD, problem kath_p, size 10
% 0.30/0.51 % Version : Especial.
% 0.30/0.51 % English :
% 0.30/0.51 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.30/0.51 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.30/0.51 % Source : [Ste24]
% 0.30/0.51 % Names : KD/k_path_p/10.p
% 0.30/0.51 % Status : Theorem
% 0.30/0.51 % Rating : ? v9.2.0
% 0.30/0.51 % Syntax : Number of formulae : 7 ( 0 unt; 6 typ; 0 def)
% 0.30/0.51 % Number of atoms : 351 ( 0 equ)
% 0.30/0.51 % Maximal formula atoms : 351 ( 351 avg)
% 0.30/0.51 % Number of connectives : 1385 ( 145 ~; 209 |; 141 &)
% 0.30/0.51 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.30/0.51 % ( 890 {.}; 0 {#})
% 0.30/0.51 % Maximal formula depth : 221 ( 221 avg)
% 0.30/0.51 % Maximal term depth : 0 ( 0 avg)
% 0.30/0.51 % Number of types : 1 ( 0 usr)
% 0.30/0.51 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.30/0.51 % Number of predicates : 7 ( 6 usr; 7 prp; 0-0 aty)
% 0.30/0.51 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.30/0.51 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.30/0.51 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.30/0.51 % Comments :
% 0.30/0.51 %------------------------------------------------------------------------------
% 0.30/0.51 qmf(10,conjecture,( #box : ( p1 ) | #box : ( p2 ) | #box : ( p3 ) | #box : ( p5 ) | #dia : ( ~ ( p1 ) & #box : ( p3 ) ) | #dia : ( ~ ( p1 ) & #box : ( p5 ) ) | $false | #dia : ( ~ ( p2 ) & #box : ( p1 ) ) | $false | #dia : ( ~ ( p3 ) & #box : ( p3 ) ) | #dia : ( ~ ( p3 ) & #box : ( p5 ) ) | $false | $false | $false | #dia : ( ~ ( p5 ) & #box : ( p3 ) ) | #dia : ( ~ ( p5 ) & #box : ( p5 ) ) | $false | $false | $false | #dia : ( #dia : ( ~ ( p1 ) & #box : ( p1 ) ) ) | #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) | #dia : ( #dia : ( ~ ( p1 ) & #box : ( p6 ) ) ) | #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) | $false | $false | #dia : ( ~ ( p4 ) & #box : ( p2 ) ) | #dia : ( ~ ( p6 ) & #box : ( p2 ) ) | #dia : ( #dia : ( ~ ( p3 ) & #box : ( p1 ) ) ) | #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) | #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) | $false | $false | #dia : ( ~ ( p4 ) & #box : ( p4 ) ) | #dia : ( ~ ( p6 ) & #box : ( p4 ) ) | #dia : ( #dia : ( ~ ( p5 ) & #box : ( p1 ) ) ) | #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) | #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) | $false | $false | #dia : ( ~ ( p4 ) & #box : ( p6 ) ) | #dia : ( ~ ( p6 ) & #box : ( p6 ) ) | #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p1 ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) | $false | $false | #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) | #dia : ( #dia : ( ~ ( p4 ) & #box : ( p2 ) ) ) | #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p1 ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) | $false | $false | #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) | #dia : ( #dia : ( ~ ( p4 ) & #box : ( p4 ) ) ) | #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p1 ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) | $false | #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p5 ) ) ) ) | #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) | #dia : ( #dia : ( ~ ( p4 ) & #box : ( p6 ) ) ) | #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p1 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p2 ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p1 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p4 ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p1 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p4 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p6 ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p2 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) ) | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p1 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p4 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p6 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p1 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p4 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p1 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p1 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p2 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) ) ) ) | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p1 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p4 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p6 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) ) | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) ) | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) | $false | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) ) ) ) ) ) ) ) ) ) ) )).
% 0.30/0.51 %------------------------------------------------------------------------------
% 0.30/0.51 ------------ End QMF file ---------------
% 45.56/46.09
% 45.56/46.09 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.dRg0hThhdS/theBenchmark.p.qmf : (modal (d/const))
% 45.56/46.09 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.dRg0hThhdS/theBenchmark.p.qmf
% 45.56/46.09 ------------------------------------------------------
% 45.56/46.09 Explanations for the proof presented below:
% 45.56/46.09 - equality axioms are added if required
% 45.56/46.09 - terms and variables are represented by Prolog terms
% 45.56/46.09 and Prolog variables, negation is represented by -
% 45.56/46.09 - a prefix Pre is a list of variables and constants
% 45.56/46.09 and assigned to each literal Lit, i.e. Pre:Lit
% 45.56/46.09 - clauses and (sub-)matrices have a unique label I^K:
% 45.56/46.09 or I^K^[..]:, where I is a unique number/identifier
% 45.56/46.09 and K identifies the instance of clause/matrix I
% 45.56/46.09 - I:Lit refers to literal Lit in clause number I
% 45.56/46.09 - in the matrix, I^[t1,..,tn] may represent the atom
% 45.56/46.09 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 45.56/46.09 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 45.56/46.09 the assignments X1:=t1, .., Xn:=tn (for both term
% 45.56/46.09 and prefix variables)
% 45.56/46.09
% 45.56/46.09 Proof:
% 45.56/46.09 ------
% 45.56/46.09 Translation into a non-clausal matrix:
% 45.56/46.09 [(3 ^ _191559) ^ [] ^ [] : [p1 : [1 ^ []]], (6 ^ _191559) ^ [] ^ [] : [p2 : [4 ^ []]], (9 ^ _191559) ^ [] ^ [] : [p3 : [7 ^ []]], (12 ^ _191559) ^ [] ^ [] : [p5 : [10 ^ []]], (15 ^ _191559) ^ [_192057] ^ [] : [-(p1) : -([_192057]), p3 : [_192057, 18 ^ [_192057]]], (23 ^ _191559) ^ [_192367] ^ [] : [-(p1) : -([_192367]), p5 : [_192367, 26 ^ [_192367]]], (30 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (37 ^ _191559) ^ [_192853] ^ [] : [-(p2) : -([_192853]), p1 : [_192853, 40 ^ [_192853]]], (44 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (51 ^ _191559) ^ [_193339] ^ [] : [-(p3) : -([_193339]), p3 : [_193339, 54 ^ [_193339]]], (59 ^ _191559) ^ [_193649] ^ [] : [-(p3) : -([_193649]), p5 : [_193649, 62 ^ [_193649]]], (66 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (72 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (78 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (85 ^ _191559) ^ [_194487] ^ [] : [-(p5) : -([_194487]), p3 : [_194487, 88 ^ [_194487]]], (93 ^ _191559) ^ [_194797] ^ [] : [-(p5) : -([_194797]), p5 : [_194797, 96 ^ [_194797]]], (100 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (106 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (112 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (120 ^ _191559) ^ [_195656, _195658] ^ [] : [-(p1) : -([_195658, _195656]), p1 : [_195658, _195656, 123 ^ [_195656, _195658]]], (129 ^ _191559) ^ [_196005, _196007] ^ [] : [-(p1) : -([_196007, _196005]), p3 : [_196007, _196005, 132 ^ [_196005, _196007]]], (138 ^ _191559) ^ [_196354, _196356] ^ [] : [-(p1) : -([_196356, _196354]), p6 : [_196356, _196354, 141 ^ [_196354, _196356]]], (147 ^ _191559) ^ [_196703, _196705] ^ [] : [-(p1) : -([_196705, _196703]), p5 : [_196705, _196703, 150 ^ [_196703, _196705]]], (154 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (160 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (167 ^ _191559) ^ [_197383] ^ [] : [-(p4) : -([_197383]), p2 : [_197383, 170 ^ [_197383]]], (175 ^ _191559) ^ [_197693] ^ [] : [-(p6) : -([_197693]), p2 : [_197693, 178 ^ [_197693]]], (184 ^ _191559) ^ [_198024, _198026] ^ [] : [-(p3) : -([_198026, _198024]), p1 : [_198026, _198024, 187 ^ [_198024, _198026]]], (193 ^ _191559) ^ [_198373, _198375] ^ [] : [-(p3) : -([_198375, _198373]), p3 : [_198375, _198373, 196 ^ [_198373, _198375]]], (202 ^ _191559) ^ [_198722, _198724] ^ [] : [-(p3) : -([_198724, _198722]), p5 : [_198724, _198722, 205 ^ [_198722, _198724]]], (209 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (215 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (222 ^ _191559) ^ [_199402] ^ [] : [-(p4) : -([_199402]), p4 : [_199402, 225 ^ [_199402]]], (230 ^ _191559) ^ [_199712] ^ [] : [-(p6) : -([_199712]), p4 : [_199712, 233 ^ [_199712]]], (239 ^ _191559) ^ [_200043, _200045] ^ [] : [-(p5) : -([_200045, _200043]), p1 : [_200045, _200043, 242 ^ [_200043, _200045]]], (248 ^ _191559) ^ [_200392, _200394] ^ [] : [-(p5) : -([_200394, _200392]), p3 : [_200394, _200392, 251 ^ [_200392, _200394]]], (257 ^ _191559) ^ [_200741, _200743] ^ [] : [-(p5) : -([_200743, _200741]), p5 : [_200743, _200741, 260 ^ [_200741, _200743]]], (264 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (270 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (277 ^ _191559) ^ [_201421] ^ [] : [-(p4) : -([_201421]), p6 : [_201421, 280 ^ [_201421]]], (285 ^ _191559) ^ [_201731] ^ [] : [-(p6) : -([_201731]), p6 : [_201731, 288 ^ [_201731]]], (295 ^ _191559) ^ [_202085, _202087, _202089] ^ [] : [-(p1) : -([_202089, _202087, _202085]), p1 : [_202089, _202087, _202085, 298 ^ [_202085, _202087, _202089]]], (305 ^ _191559) ^ [_202475, _202477, _202479] ^ [] : [-(p1) : -([_202479, _202477, _202475]), p3 : [_202479, _202477, _202475, 308 ^ [_202475, _202477, _202479]]], (312 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (318 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (326 ^ _191559) ^ [_203194, _203196] ^ [] : [-(p2) : -([_203196, _203194]), p2 : [_203196, _203194, 329 ^ [_203194, _203196]]], (335 ^ _191559) ^ [_203543, _203545] ^ [] : [-(p4) : -([_203545, _203543]), p2 : [_203545, _203543, 338 ^ [_203543, _203545]]], (344 ^ _191559) ^ [_203892, _203894] ^ [] : [-(p6) : -([_203894, _203892]), p2 : [_203894, _203892, 347 ^ [_203892, _203894]]], (354 ^ _191559) ^ [_204264, _204266, _204268] ^ [] : [-(p3) : -([_204268, _204266, _204264]), p1 : [_204268, _204266, _204264, 357 ^ [_204264, _204266, _204268]]], (364 ^ _191559) ^ [_204654, _204656, _204658] ^ [] : [-(p3) : -([_204658, _204656, _204654]), p3 : [_204658, _204656, _204654, 367 ^ [_204654, _204656, _204658]]], (371 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (377 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (385 ^ _191559) ^ [_205373, _205375] ^ [] : [-(p2) : -([_205375, _205373]), p4 : [_205375, _205373, 388 ^ [_205373, _205375]]], (394 ^ _191559) ^ [_205722, _205724] ^ [] : [-(p4) : -([_205724, _205722]), p4 : [_205724, _205722, 397 ^ [_205722, _205724]]], (403 ^ _191559) ^ [_206071, _206073] ^ [] : [-(p6) : -([_206073, _206071]), p4 : [_206073, _206071, 406 ^ [_206071, _206073]]], (413 ^ _191559) ^ [_206443, _206445, _206447] ^ [] : [-(p5) : -([_206447, _206445, _206443]), p1 : [_206447, _206445, _206443, 416 ^ [_206443, _206445, _206447]]], (423 ^ _191559) ^ [_206833, _206835, _206837] ^ [] : [-(p5) : -([_206837, _206835, _206833]), p3 : [_206837, _206835, _206833, 426 ^ [_206833, _206835, _206837]]], (430 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (439 ^ _191559) ^ [_207399, _207401, _207403] ^ [] : [-(p6) : -([_207403, _207401, _207399]), p5 : [_207403, _207401, _207399, 442 ^ [_207399, _207401, _207403]]], (448 ^ _191559) ^ [_207766, _207768] ^ [] : [-(p2) : -([_207768, _207766]), p6 : [_207768, _207766, 451 ^ [_207766, _207768]]], (457 ^ _191559) ^ [_208115, _208117] ^ [] : [-(p4) : -([_208117, _208115]), p6 : [_208117, _208115, 460 ^ [_208115, _208117]]], (466 ^ _191559) ^ [_208464, _208466] ^ [] : [-(p6) : -([_208466, _208464]), p6 : [_208466, _208464, 469 ^ [_208464, _208466]]], (477 ^ _191559) ^ [_208861, _208863, _208865, _208867] ^ [] : [-(p1) : -([_208867, _208865, _208863, _208861]), p1 : [_208867, _208865, _208863, _208861, 480 ^ [_208861, _208863, _208865, _208867]]], (488 ^ _191559) ^ [_209294, _209296, _209298, _209300] ^ [] : [-(p1) : -([_209300, _209298, _209296, _209294]), p3 : [_209300, _209298, _209296, _209294, 491 ^ [_209294, _209296, _209298, _209300]]], (499 ^ _191559) ^ [_209727, _209729, _209731, _209733] ^ [] : [-(p1) : -([_209733, _209731, _209729, _209727]), p5 : [_209733, _209731, _209729, _209727, 502 ^ [_209727, _209729, _209731, _209733]]], (506 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (512 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (521 ^ _191559) ^ [_210487, _210489, _210491] ^ [] : [-(p2) : -([_210491, _210489, _210487]), p2 : [_210491, _210489, _210487, 524 ^ [_210487, _210489, _210491]]], (531 ^ _191559) ^ [_210877, _210879, _210881] ^ [] : [-(p4) : -([_210881, _210879, _210877]), p2 : [_210881, _210879, _210877, 534 ^ [_210877, _210879, _210881]]], (542 ^ _191559) ^ [_211292, _211294, _211296, _211298] ^ [] : [-(p3) : -([_211298, _211296, _211294, _211292]), p1 : [_211298, _211296, _211294, _211292, 545 ^ [_211292, _211294, _211296, _211298]]], (553 ^ _191559) ^ [_211725, _211727, _211729, _211731] ^ [] : [-(p3) : -([_211731, _211729, _211727, _211725]), p3 : [_211731, _211729, _211727, _211725, 556 ^ [_211725, _211727, _211729, _211731]]], (564 ^ _191559) ^ [_212158, _212160, _212162, _212164] ^ [] : [-(p3) : -([_212164, _212162, _212160, _212158]), p5 : [_212164, _212162, _212160, _212158, 567 ^ [_212158, _212160, _212162, _212164]]], (571 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (577 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (586 ^ _191559) ^ [_212918, _212920, _212922] ^ [] : [-(p2) : -([_212922, _212920, _212918]), p4 : [_212922, _212920, _212918, 589 ^ [_212918, _212920, _212922]]], (596 ^ _191559) ^ [_213308, _213310, _213312] ^ [] : [-(p4) : -([_213312, _213310, _213308]), p4 : [_213312, _213310, _213308, 599 ^ [_213308, _213310, _213312]]], (607 ^ _191559) ^ [_213723, _213725, _213727, _213729] ^ [] : [-(p5) : -([_213729, _213727, _213725, _213723]), p1 : [_213729, _213727, _213725, _213723, 610 ^ [_213723, _213725, _213727, _213729]]], (618 ^ _191559) ^ [_214156, _214158, _214160, _214162] ^ [] : [-(p5) : -([_214162, _214160, _214158, _214156]), p3 : [_214162, _214160, _214158, _214156, 621 ^ [_214156, _214158, _214160, _214162]]], (629 ^ _191559) ^ [_214589, _214591, _214593, _214595] ^ [] : [-(p5) : -([_214595, _214593, _214591, _214589]), p4 : [_214595, _214593, _214591, _214589, 632 ^ [_214589, _214591, _214593, _214595]]], (640 ^ _191559) ^ [_215022, _215024, _215026, _215028] ^ [] : [-(p5) : -([_215028, _215026, _215024, _215022]), p5 : [_215028, _215026, _215024, _215022, 643 ^ [_215022, _215024, _215026, _215028]]], (647 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (653 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (662 ^ _191559) ^ [_215782, _215784, _215786] ^ [] : [-(p2) : -([_215786, _215784, _215782]), p6 : [_215786, _215784, _215782, 665 ^ [_215782, _215784, _215786]]], (672 ^ _191559) ^ [_216172, _216174, _216176] ^ [] : [-(p4) : -([_216176, _216174, _216172]), p6 : [_216176, _216174, _216172, 675 ^ [_216172, _216174, _216176]]], (684 ^ _191559) ^ [_216614, _216616, _216618, _216620, _216622] ^ [] : [-(p1) : -([_216622, _216620, _216618, _216616, _216614]), p3 : [_216622, _216620, _216618, _216616, _216614, 687 ^ [_216614, _216616, _216618, _216620, _216622]]], (696 ^ _191559) ^ [_217092, _217094, _217096, _217098, _217100] ^ [] : [-(p1) : -([_217100, _217098, _217096, _217094, _217092]), p5 : [_217100, _217098, _217096, _217094, _217092, 699 ^ [_217092, _217094, _217096, _217098, _217100]]], (703 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (709 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (719 ^ _191559) ^ [_217895, _217897, _217899, _217901] ^ [] : [-(p2) : -([_217901, _217899, _217897, _217895]), p2 : [_217901, _217899, _217897, _217895, 722 ^ [_217895, _217897, _217899, _217901]]], (730 ^ _191559) ^ [_218328, _218330, _218332, _218334] ^ [] : [-(p4) : -([_218334, _218332, _218330, _218328]), p2 : [_218334, _218332, _218330, _218328, 733 ^ [_218328, _218330, _218332, _218334]]], (741 ^ _191559) ^ [_218761, _218763, _218765, _218767] ^ [] : [-(p6) : -([_218767, _218765, _218763, _218761]), p2 : [_218767, _218765, _218763, _218761, 744 ^ [_218761, _218763, _218765, _218767]]], (753 ^ _191559) ^ [_219221, _219223, _219225, _219227, _219229] ^ [] : [-(p3) : -([_219229, _219227, _219225, _219223, _219221]), p3 : [_219229, _219227, _219225, _219223, _219221, 756 ^ [_219221, _219223, _219225, _219227, _219229]]], (765 ^ _191559) ^ [_219699, _219701, _219703, _219705, _219707] ^ [] : [-(p3) : -([_219707, _219705, _219703, _219701, _219699]), p5 : [_219707, _219705, _219703, _219701, _219699, 768 ^ [_219699, _219701, _219703, _219705, _219707]]], (772 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (783 ^ _191559) ^ [_220353, _220355, _220357, _220359, _220361] ^ [] : [-(p4) : -([_220361, _220359, _220357, _220355, _220353]), p1 : [_220361, _220359, _220357, _220355, _220353, 786 ^ [_220353, _220355, _220357, _220359, _220361]]], (794 ^ _191559) ^ [_220804, _220806, _220808, _220810] ^ [] : [-(p2) : -([_220810, _220808, _220806, _220804]), p4 : [_220810, _220808, _220806, _220804, 797 ^ [_220804, _220806, _220808, _220810]]], (805 ^ _191559) ^ [_221237, _221239, _221241, _221243] ^ [] : [-(p4) : -([_221243, _221241, _221239, _221237]), p4 : [_221243, _221241, _221239, _221237, 808 ^ [_221237, _221239, _221241, _221243]]], (816 ^ _191559) ^ [_221670, _221672, _221674, _221676] ^ [] : [-(p6) : -([_221676, _221674, _221672, _221670]), p4 : [_221676, _221674, _221672, _221670, 819 ^ [_221670, _221672, _221674, _221676]]], (828 ^ _191559) ^ [_222130, _222132, _222134, _222136, _222138] ^ [] : [-(p5) : -([_222138, _222136, _222134, _222132, _222130]), p3 : [_222138, _222136, _222134, _222132, _222130, 831 ^ [_222130, _222132, _222134, _222136, _222138]]], (840 ^ _191559) ^ [_222608, _222610, _222612, _222614, _222616] ^ [] : [-(p5) : -([_222616, _222614, _222612, _222610, _222608]), p5 : [_222616, _222614, _222612, _222610, _222608, 843 ^ [_222608, _222610, _222612, _222614, _222616]]], (847 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (853 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (863 ^ _191559) ^ [_223411, _223413, _223415, _223417] ^ [] : [-(p2) : -([_223417, _223415, _223413, _223411]), p6 : [_223417, _223415, _223413, _223411, 866 ^ [_223411, _223413, _223415, _223417]]], (874 ^ _191559) ^ [_223844, _223846, _223848, _223850] ^ [] : [-(p4) : -([_223850, _223848, _223846, _223844]), p6 : [_223850, _223848, _223846, _223844, 877 ^ [_223844, _223846, _223848, _223850]]], (885 ^ _191559) ^ [_224277, _224279, _224281, _224283] ^ [] : [-(p6) : -([_224283, _224281, _224279, _224277]), p6 : [_224283, _224281, _224279, _224277, 888 ^ [_224277, _224279, _224281, _224283]]], (898 ^ _191559) ^ [_224766, _224768, _224770, _224772, _224774, _224776] ^ [] : [-(p1) : -([_224776, _224774, _224772, _224770, _224768, _224766]), p1 : [_224776, _224774, _224772, _224770, _224768, _224766, 901 ^ [_224766, _224768, _224770, _224772, _224774, _224776]]], (911 ^ _191559) ^ [_225291, _225293, _225295, _225297, _225299, _225301] ^ [] : [-(p1) : -([_225301, _225299, _225297, _225295, _225293, _225291]), p3 : [_225301, _225299, _225297, _225295, _225293, _225291, 914 ^ [_225291, _225293, _225295, _225297, _225299, _225301]]], (924 ^ _191559) ^ [_225816, _225818, _225820, _225822, _225824, _225826] ^ [] : [-(p1) : -([_225826, _225824, _225822, _225820, _225818, _225816]), p4 : [_225826, _225824, _225822, _225820, _225818, _225816, 927 ^ [_225816, _225818, _225820, _225822, _225824, _225826]]], (937 ^ _191559) ^ [_226341, _226343, _226345, _226347, _226349, _226351] ^ [] : [-(p1) : -([_226351, _226349, _226347, _226345, _226343, _226341]), p5 : [_226351, _226349, _226347, _226345, _226343, _226341, 940 ^ [_226341, _226343, _226345, _226347, _226349, _226351]]], (944 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (950 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (961 ^ _191559) ^ [_227189, _227191, _227193, _227195, _227197] ^ [] : [-(p2) : -([_227197, _227195, _227193, _227191, _227189]), p2 : [_227197, _227195, _227193, _227191, _227189, 964 ^ [_227189, _227191, _227193, _227195, _227197]]], (973 ^ _191559) ^ [_227667, _227669, _227671, _227673, _227675] ^ [] : [-(p6) : -([_227675, _227673, _227671, _227669, _227667]), p2 : [_227675, _227673, _227671, _227669, _227667, 976 ^ [_227667, _227669, _227671, _227673, _227675]]], (986 ^ _191559) ^ [_228174, _228176, _228178, _228180, _228182, _228184] ^ [] : [-(p3) : -([_228184, _228182, _228180, _228178, _228176, _228174]), p1 : [_228184, _228182, _228180, _228178, _228176, _228174, 989 ^ [_228174, _228176, _228178, _228180, _228182, _228184]]], (999 ^ _191559) ^ [_228699, _228701, _228703, _228705, _228707, _228709] ^ [] : [-(p3) : -([_228709, _228707, _228705, _228703, _228701, _228699]), p3 : [_228709, _228707, _228705, _228703, _228701, _228699, 1002 ^ [_228699, _228701, _228703, _228705, _228707, _228709]]], (1012 ^ _191559) ^ [_229224, _229226, _229228, _229230, _229232, _229234] ^ [] : [-(p3) : -([_229234, _229232, _229230, _229228, _229226, _229224]), p5 : [_229234, _229232, _229230, _229228, _229226, _229224, 1015 ^ [_229224, _229226, _229228, _229230, _229232, _229234]]], (1019 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1025 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1036 ^ _191559) ^ [_230072, _230074, _230076, _230078, _230080] ^ [] : [-(p2) : -([_230080, _230078, _230076, _230074, _230072]), p4 : [_230080, _230078, _230076, _230074, _230072, 1039 ^ [_230072, _230074, _230076, _230078, _230080]]], (1048 ^ _191559) ^ [_230550, _230552, _230554, _230556, _230558] ^ [] : [-(p6) : -([_230558, _230556, _230554, _230552, _230550]), p4 : [_230558, _230556, _230554, _230552, _230550, 1051 ^ [_230550, _230552, _230554, _230556, _230558]]], (1061 ^ _191559) ^ [_231057, _231059, _231061, _231063, _231065, _231067] ^ [] : [-(p5) : -([_231067, _231065, _231063, _231061, _231059, _231057]), p1 : [_231067, _231065, _231063, _231061, _231059, _231057, 1064 ^ [_231057, _231059, _231061, _231063, _231065, _231067]]], (1074 ^ _191559) ^ [_231582, _231584, _231586, _231588, _231590, _231592] ^ [] : [-(p5) : -([_231592, _231590, _231588, _231586, _231584, _231582]), p3 : [_231592, _231590, _231588, _231586, _231584, _231582, 1077 ^ [_231582, _231584, _231586, _231588, _231590, _231592]]], (1087 ^ _191559) ^ [_232107, _232109, _232111, _232113, _232115, _232117] ^ [] : [-(p5) : -([_232117, _232115, _232113, _232111, _232109, _232107]), p5 : [_232117, _232115, _232113, _232111, _232109, _232107, 1090 ^ [_232107, _232109, _232111, _232113, _232115, _232117]]], (1094 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1100 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1111 ^ _191559) ^ [_232955, _232957, _232959, _232961, _232963] ^ [] : [-(p2) : -([_232963, _232961, _232959, _232957, _232955]), p6 : [_232963, _232961, _232959, _232957, _232955, 1114 ^ [_232955, _232957, _232959, _232961, _232963]]], (1123 ^ _191559) ^ [_233433, _233435, _233437, _233439, _233441] ^ [] : [-(p6) : -([_233441, _233439, _233437, _233435, _233433]), p6 : [_233441, _233439, _233437, _233435, _233433, 1126 ^ [_233433, _233435, _233437, _233439, _233441]]], (1137 ^ _191559) ^ [_233971, _233973, _233975, _233977, _233979, _233981, _233983] ^ [] : [-(p1) : -([_233983, _233981, _233979, _233977, _233975, _233973, _233971]), p3 : [_233983, _233981, _233979, _233977, _233975, _233973, _233971, 1140 ^ [_233971, _233973, _233975, _233977, _233979, _233981, _233983]]], (1151 ^ _191559) ^ [_234545, _234547, _234549, _234551, _234553, _234555, _234557] ^ [] : [-(p1) : -([_234557, _234555, _234553, _234551, _234549, _234547, _234545]), p5 : [_234557, _234555, _234553, _234551, _234549, _234547, _234545, 1154 ^ [_234545, _234547, _234549, _234551, _234553, _234555, _234557]]], (1158 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1164 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1176 ^ _191559) ^ [_235440, _235442, _235444, _235446, _235448, _235450] ^ [] : [-(p2) : -([_235450, _235448, _235446, _235444, _235442, _235440]), p2 : [_235450, _235448, _235446, _235444, _235442, _235440, 1179 ^ [_235440, _235442, _235444, _235446, _235448, _235450]]], (1189 ^ _191559) ^ [_235965, _235967, _235969, _235971, _235973, _235975] ^ [] : [-(p4) : -([_235975, _235973, _235971, _235969, _235967, _235965]), p2 : [_235975, _235973, _235971, _235969, _235967, _235965, 1192 ^ [_235965, _235967, _235969, _235971, _235973, _235975]]], (1202 ^ _191559) ^ [_236490, _236492, _236494, _236496, _236498, _236500] ^ [] : [-(p6) : -([_236500, _236498, _236496, _236494, _236492, _236490]), p2 : [_236500, _236498, _236496, _236494, _236492, _236490, 1205 ^ [_236490, _236492, _236494, _236496, _236498, _236500]]], (1216 ^ _191559) ^ [_237046, _237048, _237050, _237052, _237054, _237056, _237058] ^ [] : [-(p3) : -([_237058, _237056, _237054, _237052, _237050, _237048, _237046]), p3 : [_237058, _237056, _237054, _237052, _237050, _237048, _237046, 1219 ^ [_237046, _237048, _237050, _237052, _237054, _237056, _237058]]], (1230 ^ _191559) ^ [_237620, _237622, _237624, _237626, _237628, _237630, _237632] ^ [] : [-(p3) : -([_237632, _237630, _237628, _237626, _237624, _237622, _237620]), p5 : [_237632, _237630, _237628, _237626, _237624, _237622, _237620, 1233 ^ [_237620, _237622, _237624, _237626, _237628, _237630, _237632]]], (1237 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1250 ^ _191559) ^ [_238370, _238372, _238374, _238376, _238378, _238380, _238382] ^ [] : [-(p4) : -([_238382, _238380, _238378, _238376, _238374, _238372, _238370]), p1 : [_238382, _238380, _238378, _238376, _238374, _238372, _238370, 1253 ^ [_238370, _238372, _238374, _238376, _238378, _238380, _238382]]], (1263 ^ _191559) ^ [_238913, _238915, _238917, _238919, _238921, _238923] ^ [] : [-(p2) : -([_238923, _238921, _238919, _238917, _238915, _238913]), p4 : [_238923, _238921, _238919, _238917, _238915, _238913, 1266 ^ [_238913, _238915, _238917, _238919, _238921, _238923]]], (1276 ^ _191559) ^ [_239438, _239440, _239442, _239444, _239446, _239448] ^ [] : [-(p4) : -([_239448, _239446, _239444, _239442, _239440, _239438]), p4 : [_239448, _239446, _239444, _239442, _239440, _239438, 1279 ^ [_239438, _239440, _239442, _239444, _239446, _239448]]], (1289 ^ _191559) ^ [_239963, _239965, _239967, _239969, _239971, _239973] ^ [] : [-(p6) : -([_239973, _239971, _239969, _239967, _239965, _239963]), p4 : [_239973, _239971, _239969, _239967, _239965, _239963, 1292 ^ [_239963, _239965, _239967, _239969, _239971, _239973]]], (1303 ^ _191559) ^ [_240519, _240521, _240523, _240525, _240527, _240529, _240531] ^ [] : [-(p5) : -([_240531, _240529, _240527, _240525, _240523, _240521, _240519]), p3 : [_240531, _240529, _240527, _240525, _240523, _240521, _240519, 1306 ^ [_240519, _240521, _240523, _240525, _240527, _240529, _240531]]], (1317 ^ _191559) ^ [_241093, _241095, _241097, _241099, _241101, _241103, _241105] ^ [] : [-(p5) : -([_241105, _241103, _241101, _241099, _241097, _241095, _241093]), p5 : [_241105, _241103, _241101, _241099, _241097, _241095, _241093, 1320 ^ [_241093, _241095, _241097, _241099, _241101, _241103, _241105]]], (1324 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1330 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1342 ^ _191559) ^ [_241988, _241990, _241992, _241994, _241996, _241998] ^ [] : [-(p2) : -([_241998, _241996, _241994, _241992, _241990, _241988]), p6 : [_241998, _241996, _241994, _241992, _241990, _241988, 1345 ^ [_241988, _241990, _241992, _241994, _241996, _241998]]], (1355 ^ _191559) ^ [_242513, _242515, _242517, _242519, _242521, _242523] ^ [] : [-(p4) : -([_242523, _242521, _242519, _242517, _242515, _242513]), p6 : [_242523, _242521, _242519, _242517, _242515, _242513, 1358 ^ [_242513, _242515, _242517, _242519, _242521, _242523]]], (1368 ^ _191559) ^ [_243038, _243040, _243042, _243044, _243046, _243048] ^ [] : [-(p6) : -([_243048, _243046, _243044, _243042, _243040, _243038]), p6 : [_243048, _243046, _243044, _243042, _243040, _243038, 1371 ^ [_243038, _243040, _243042, _243044, _243046, _243048]]], (1383 ^ _191559) ^ [_243627, _243629, _243631, _243633, _243635, _243637, _243639, _243641] ^ [] : [-(p1) : -([_243641, _243639, _243637, _243635, _243633, _243631, _243629, _243627]), p1 : [_243641, _243639, _243637, _243635, _243633, _243631, _243629, _243627, 1386 ^ [_243627, _243629, _243631, _243633, _243635, _243637, _243639, _243641]]], (1398 ^ _191559) ^ [_244252, _244254, _244256, _244258, _244260, _244262, _244264, _244266] ^ [] : [-(p1) : -([_244266, _244264, _244262, _244260, _244258, _244256, _244254, _244252]), p3 : [_244266, _244264, _244262, _244260, _244258, _244256, _244254, _244252, 1401 ^ [_244252, _244254, _244256, _244258, _244260, _244262, _244264, _244266]]], (1413 ^ _191559) ^ [_244877, _244879, _244881, _244883, _244885, _244887, _244889, _244891] ^ [] : [-(p1) : -([_244891, _244889, _244887, _244885, _244883, _244881, _244879, _244877]), p4 : [_244891, _244889, _244887, _244885, _244883, _244881, _244879, _244877, 1416 ^ [_244877, _244879, _244881, _244883, _244885, _244887, _244889, _244891]]], (1428 ^ _191559) ^ [_245502, _245504, _245506, _245508, _245510, _245512, _245514, _245516] ^ [] : [-(p1) : -([_245516, _245514, _245512, _245510, _245508, _245506, _245504, _245502]), p5 : [_245516, _245514, _245512, _245510, _245508, _245506, _245504, _245502, 1431 ^ [_245502, _245504, _245506, _245508, _245510, _245512, _245514, _245516]]], (1435 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1441 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1454 ^ _191559) ^ [_246446, _246448, _246450, _246452, _246454, _246456, _246458] ^ [] : [-(p2) : -([_246458, _246456, _246454, _246452, _246450, _246448, _246446]), p2 : [_246458, _246456, _246454, _246452, _246450, _246448, _246446, 1457 ^ [_246446, _246448, _246450, _246452, _246454, _246456, _246458]]], (1468 ^ _191559) ^ [_247020, _247022, _247024, _247026, _247028, _247030, _247032] ^ [] : [-(p6) : -([_247032, _247030, _247028, _247026, _247024, _247022, _247020]), p2 : [_247032, _247030, _247028, _247026, _247024, _247022, _247020, 1471 ^ [_247020, _247022, _247024, _247026, _247028, _247030, _247032]]], (1483 ^ _191559) ^ [_247627, _247629, _247631, _247633, _247635, _247637, _247639, _247641] ^ [] : [-(p3) : -([_247641, _247639, _247637, _247635, _247633, _247631, _247629, _247627]), p1 : [_247641, _247639, _247637, _247635, _247633, _247631, _247629, _247627, 1486 ^ [_247627, _247629, _247631, _247633, _247635, _247637, _247639, _247641]]], (1498 ^ _191559) ^ [_248252, _248254, _248256, _248258, _248260, _248262, _248264, _248266] ^ [] : [-(p3) : -([_248266, _248264, _248262, _248260, _248258, _248256, _248254, _248252]), p3 : [_248266, _248264, _248262, _248260, _248258, _248256, _248254, _248252, 1501 ^ [_248252, _248254, _248256, _248258, _248260, _248262, _248264, _248266]]], (1513 ^ _191559) ^ [_248877, _248879, _248881, _248883, _248885, _248887, _248889, _248891] ^ [] : [-(p3) : -([_248891, _248889, _248887, _248885, _248883, _248881, _248879, _248877]), p5 : [_248891, _248889, _248887, _248885, _248883, _248881, _248879, _248877, 1516 ^ [_248877, _248879, _248881, _248883, _248885, _248887, _248889, _248891]]], (1520 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1526 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1539 ^ _191559) ^ [_249821, _249823, _249825, _249827, _249829, _249831, _249833] ^ [] : [-(p2) : -([_249833, _249831, _249829, _249827, _249825, _249823, _249821]), p4 : [_249833, _249831, _249829, _249827, _249825, _249823, _249821, 1542 ^ [_249821, _249823, _249825, _249827, _249829, _249831, _249833]]], (1553 ^ _191559) ^ [_250395, _250397, _250399, _250401, _250403, _250405, _250407] ^ [] : [-(p6) : -([_250407, _250405, _250403, _250401, _250399, _250397, _250395]), p4 : [_250407, _250405, _250403, _250401, _250399, _250397, _250395, 1556 ^ [_250395, _250397, _250399, _250401, _250403, _250405, _250407]]], (1568 ^ _191559) ^ [_251002, _251004, _251006, _251008, _251010, _251012, _251014, _251016] ^ [] : [-(p5) : -([_251016, _251014, _251012, _251010, _251008, _251006, _251004, _251002]), p1 : [_251016, _251014, _251012, _251010, _251008, _251006, _251004, _251002, 1571 ^ [_251002, _251004, _251006, _251008, _251010, _251012, _251014, _251016]]], (1583 ^ _191559) ^ [_251627, _251629, _251631, _251633, _251635, _251637, _251639, _251641] ^ [] : [-(p5) : -([_251641, _251639, _251637, _251635, _251633, _251631, _251629, _251627]), p3 : [_251641, _251639, _251637, _251635, _251633, _251631, _251629, _251627, 1586 ^ [_251627, _251629, _251631, _251633, _251635, _251637, _251639, _251641]]], (1598 ^ _191559) ^ [_252252, _252254, _252256, _252258, _252260, _252262, _252264, _252266] ^ [] : [-(p5) : -([_252266, _252264, _252262, _252260, _252258, _252256, _252254, _252252]), p5 : [_252266, _252264, _252262, _252260, _252258, _252256, _252254, _252252, 1601 ^ [_252252, _252254, _252256, _252258, _252260, _252262, _252264, _252266]]], (1605 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1611 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1624 ^ _191559) ^ [_253196, _253198, _253200, _253202, _253204, _253206, _253208] ^ [] : [-(p2) : -([_253208, _253206, _253204, _253202, _253200, _253198, _253196]), p6 : [_253208, _253206, _253204, _253202, _253200, _253198, _253196, 1627 ^ [_253196, _253198, _253200, _253202, _253204, _253206, _253208]]], (1638 ^ _191559) ^ [_253770, _253772, _253774, _253776, _253778, _253780, _253782] ^ [] : [-(p6) : -([_253782, _253780, _253778, _253776, _253774, _253772, _253770]), p6 : [_253782, _253780, _253778, _253776, _253774, _253772, _253770, 1641 ^ [_253770, _253772, _253774, _253776, _253778, _253780, _253782]]], (1654 ^ _191559) ^ [_254412, _254414, _254416, _254418, _254420, _254422, _254424, _254426, _254428] ^ [] : [-(p1) : -([_254428, _254426, _254424, _254422, _254420, _254418, _254416, _254414, _254412]), p3 : [_254428, _254426, _254424, _254422, _254420, _254418, _254416, _254414, _254412, 1657 ^ [_254412, _254414, _254416, _254418, _254420, _254422, _254424, _254426, _254428]]], (1670 ^ _191559) ^ [_255090, _255092, _255094, _255096, _255098, _255100, _255102, _255104, _255106] ^ [] : [-(p1) : -([_255106, _255104, _255102, _255100, _255098, _255096, _255094, _255092, _255090]), p5 : [_255106, _255104, _255102, _255100, _255098, _255096, _255094, _255092, _255090, 1673 ^ [_255090, _255092, _255094, _255096, _255098, _255100, _255102, _255104, _255106]]], (1677 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1683 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1697 ^ _191559) ^ [_256085, _256087, _256089, _256091, _256093, _256095, _256097, _256099] ^ [] : [-(p2) : -([_256099, _256097, _256095, _256093, _256091, _256089, _256087, _256085]), p2 : [_256099, _256097, _256095, _256093, _256091, _256089, _256087, _256085, 1700 ^ [_256085, _256087, _256089, _256091, _256093, _256095, _256097, _256099]]], (1712 ^ _191559) ^ [_256710, _256712, _256714, _256716, _256718, _256720, _256722, _256724] ^ [] : [-(p4) : -([_256724, _256722, _256720, _256718, _256716, _256714, _256712, _256710]), p2 : [_256724, _256722, _256720, _256718, _256716, _256714, _256712, _256710, 1715 ^ [_256710, _256712, _256714, _256716, _256718, _256720, _256722, _256724]]], (1727 ^ _191559) ^ [_257335, _257337, _257339, _257341, _257343, _257345, _257347, _257349] ^ [] : [-(p6) : -([_257349, _257347, _257345, _257343, _257341, _257339, _257337, _257335]), p2 : [_257349, _257347, _257345, _257343, _257341, _257339, _257337, _257335, 1730 ^ [_257335, _257337, _257339, _257341, _257343, _257345, _257347, _257349]]], (1743 ^ _191559) ^ [_257995, _257997, _257999, _258001, _258003, _258005, _258007, _258009, _258011] ^ [] : [-(p3) : -([_258011, _258009, _258007, _258005, _258003, _258001, _257999, _257997, _257995]), p3 : [_258011, _258009, _258007, _258005, _258003, _258001, _257999, _257997, _257995, 1746 ^ [_257995, _257997, _257999, _258001, _258003, _258005, _258007, _258009, _258011]]], (1759 ^ _191559) ^ [_258673, _258675, _258677, _258679, _258681, _258683, _258685, _258687, _258689] ^ [] : [-(p3) : -([_258689, _258687, _258685, _258683, _258681, _258679, _258677, _258675, _258673]), p5 : [_258689, _258687, _258685, _258683, _258681, _258679, _258677, _258675, _258673, 1762 ^ [_258673, _258675, _258677, _258679, _258681, _258683, _258685, _258687, _258689]]], (1766 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1781 ^ _191559) ^ [_259527, _259529, _259531, _259533, _259535, _259537, _259539, _259541, _259543] ^ [] : [-(p4) : -([_259543, _259541, _259539, _259537, _259535, _259533, _259531, _259529, _259527]), p1 : [_259543, _259541, _259539, _259537, _259535, _259533, _259531, _259529, _259527, 1784 ^ [_259527, _259529, _259531, _259533, _259535, _259537, _259539, _259541, _259543]]], (1796 ^ _191559) ^ [_260170, _260172, _260174, _260176, _260178, _260180, _260182, _260184] ^ [] : [-(p2) : -([_260184, _260182, _260180, _260178, _260176, _260174, _260172, _260170]), p4 : [_260184, _260182, _260180, _260178, _260176, _260174, _260172, _260170, 1799 ^ [_260170, _260172, _260174, _260176, _260178, _260180, _260182, _260184]]], (1811 ^ _191559) ^ [_260795, _260797, _260799, _260801, _260803, _260805, _260807, _260809] ^ [] : [-(p4) : -([_260809, _260807, _260805, _260803, _260801, _260799, _260797, _260795]), p4 : [_260809, _260807, _260805, _260803, _260801, _260799, _260797, _260795, 1814 ^ [_260795, _260797, _260799, _260801, _260803, _260805, _260807, _260809]]], (1826 ^ _191559) ^ [_261420, _261422, _261424, _261426, _261428, _261430, _261432, _261434] ^ [] : [-(p6) : -([_261434, _261432, _261430, _261428, _261426, _261424, _261422, _261420]), p4 : [_261434, _261432, _261430, _261428, _261426, _261424, _261422, _261420, 1829 ^ [_261420, _261422, _261424, _261426, _261428, _261430, _261432, _261434]]], (1842 ^ _191559) ^ [_262080, _262082, _262084, _262086, _262088, _262090, _262092, _262094, _262096] ^ [] : [-(p5) : -([_262096, _262094, _262092, _262090, _262088, _262086, _262084, _262082, _262080]), p3 : [_262096, _262094, _262092, _262090, _262088, _262086, _262084, _262082, _262080, 1845 ^ [_262080, _262082, _262084, _262086, _262088, _262090, _262092, _262094, _262096]]], (1858 ^ _191559) ^ [_262758, _262760, _262762, _262764, _262766, _262768, _262770, _262772, _262774] ^ [] : [-(p5) : -([_262774, _262772, _262770, _262768, _262766, _262764, _262762, _262760, _262758]), p5 : [_262774, _262772, _262770, _262768, _262766, _262764, _262762, _262760, _262758, 1861 ^ [_262758, _262760, _262762, _262764, _262766, _262768, _262770, _262772, _262774]]], (1865 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1871 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1885 ^ _191559) ^ [_263753, _263755, _263757, _263759, _263761, _263763, _263765, _263767] ^ [] : [-(p2) : -([_263767, _263765, _263763, _263761, _263759, _263757, _263755, _263753]), p6 : [_263767, _263765, _263763, _263761, _263759, _263757, _263755, _263753, 1888 ^ [_263753, _263755, _263757, _263759, _263761, _263763, _263765, _263767]]], (1900 ^ _191559) ^ [_264378, _264380, _264382, _264384, _264386, _264388, _264390, _264392] ^ [] : [-(p4) : -([_264392, _264390, _264388, _264386, _264384, _264382, _264380, _264378]), p6 : [_264392, _264390, _264388, _264386, _264384, _264382, _264380, _264378, 1903 ^ [_264378, _264380, _264382, _264384, _264386, _264388, _264390, _264392]]], (1915 ^ _191559) ^ [_265003, _265005, _265007, _265009, _265011, _265013, _265015, _265017] ^ [] : [-(p6) : -([_265017, _265015, _265013, _265011, _265009, _265007, _265005, _265003]), p6 : [_265017, _265015, _265013, _265011, _265009, _265007, _265005, _265003, 1918 ^ [_265003, _265005, _265007, _265009, _265011, _265013, _265015, _265017]]], (1922 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1928 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1934 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1949 ^ _191559) ^ [_266191, _266193, _266195, _266197, _266199, _266201, _266203, _266205, _266207] ^ [] : [-(p2) : -([_266207, _266205, _266203, _266201, _266199, _266197, _266195, _266193, _266191]), p2 : [_266207, _266205, _266203, _266201, _266199, _266197, _266195, _266193, _266191, 1952 ^ [_266191, _266193, _266195, _266197, _266199, _266201, _266203, _266205, _266207]]], (1965 ^ _191559) ^ [_266869, _266871, _266873, _266875, _266877, _266879, _266881, _266883, _266885] ^ [] : [-(p6) : -([_266885, _266883, _266881, _266879, _266877, _266875, _266873, _266871, _266869]), p2 : [_266885, _266883, _266881, _266879, _266877, _266875, _266873, _266871, _266869, 1968 ^ [_266869, _266871, _266873, _266875, _266877, _266879, _266881, _266883, _266885]]], (1972 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1978 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1984 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1999 ^ _191559) ^ [_268075, _268077, _268079, _268081, _268083, _268085, _268087, _268089, _268091] ^ [] : [-(p2) : -([_268091, _268089, _268087, _268085, _268083, _268081, _268079, _268077, _268075]), p4 : [_268091, _268089, _268087, _268085, _268083, _268081, _268079, _268077, _268075, 2002 ^ [_268075, _268077, _268079, _268081, _268083, _268085, _268087, _268089, _268091]]], (2015 ^ _191559) ^ [_268753, _268755, _268757, _268759, _268761, _268763, _268765, _268767, _268769] ^ [] : [-(p6) : -([_268769, _268767, _268765, _268763, _268761, _268759, _268757, _268755, _268753]), p4 : [_268769, _268767, _268765, _268763, _268761, _268759, _268757, _268755, _268753, 2018 ^ [_268753, _268755, _268757, _268759, _268761, _268763, _268765, _268767, _268769]]], (2022 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2028 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2034 ^ _191559) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2049 ^ _191559) ^ [_269959, _269961, _269963, _269965, _269967, _269969, _269971, _269973, _269975] ^ [] : [-(p2) : -([_269975, _269973, _269971, _269969, _269967, _269965, _269963, _269961, _269959]), p6 : [_269975, _269973, _269971, _269969, _269967, _269965, _269963, _269961, _269959, 2052 ^ [_269959, _269961, _269963, _269965, _269967, _269969, _269971, _269973, _269975]]], (2082 ^ _191559) ^ [_271346, _271348, _271350, _271352, _271354, _271356, _271358, _271360, _271362, _271364] ^ [] : [-(p2) : -([_271364, _271362, _271360, _271358, _271356, _271354, _271352, _271350, _271348, _271346])], (2094 ^ _191559) ^ [_271761, _271763, _271765, _271767, _271769, _271771, _271773, _271775, _271777, _271779] ^ [] : [-(p4) : -([_271779, _271777, _271775, _271773, _271771, _271769, _271767, _271765, _271763, _271761])], (2106 ^ _191559) ^ [_272176, _272178, _272180, _272182, _272184, _272186, _272188, _272190, _272192, _272194] ^ [] : [-(p1) : -([_272194, _272192, _272190, _272188, _272186, _272184, _272182, _272180, _272178, _272176])], (2118 ^ _191559) ^ [_272568, _272570, _272572, _272574, _272576, _272578, _272580, _272582, _272584, _272586] ^ [] : [-(p6) : -([_272586, _272584, _272582, _272580, _272578, _272576, _272574, _272572, _272570, _272568])], (2065 ^ _191559) ^ [_270637, _270639, _270641, _270643, _270645, _270647, _270649, _270651, _270653] ^ [] : [-(p6) : -([_270653, _270651, _270649, _270647, _270645, _270643, _270641, _270639, _270637]), p6 : [_270653, _270651, _270649, _270647, _270645, _270643, _270641, _270639, _270637, 2068 ^ [_270637, _270639, _270641, _270643, _270645, _270647, _270649, _270651, _270653]]]]
% 45.56/46.10
% 45.56/46.10 We prove that the given matrix is valid, i.e. for
% 45.56/46.10 a given substitution it evaluates to true for all
% 45.56/46.10 interpretations. A matrix is true iff at least one
% 45.56/46.10 of its clauses is true; a clause is true iff all of
% 45.56/46.10 its elements (literals and submatrices) are true.
% 45.56/46.10
% 45.56/46.10 The proof is by contradiction:
% 45.56/46.10 Assume there is an interpretation so that the given
% 45.56/46.10 matrix evaluates to false. Then in each clause there
% 45.56/46.10 has to be at least one element that is false.
% 45.56/46.10
% 45.56/46.10 Then clause (6 ^ 0) is false if at least one of the following is false:
% 45.56/46.10 [p2 : [4 ^ []]]
% 45.56/46.10 1 Assume p2 : [4 ^ []] is false.
% 45.56/46.10 Then clause (37 ^ 1) under the substitution [[_192853], [4 ^ []]]
% 45.56/46.10 is false if at least one of the following is false:
% 45.56/46.10 [p1 : [4 ^ [], 40 ^ [4 ^ []]]]
% 45.56/46.10 1.1 Assume p1 : [4 ^ [], 40 ^ [4 ^ []]] is false.
% 45.56/46.10 Then clause (138 ^ 2) under the substitution [[_196354, _196356], [40 ^ [4 ^ []], 4 ^ []]]
% 45.56/46.10 is false if at least one of the following is false:
% 45.56/46.10 [p6 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []]]]
% 45.56/46.10 1.1.1 Assume p6 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []]] is false.
% 45.56/46.10 Then clause (439 ^ 3) under the substitution [[_207399, _207401, _207403], [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 45.56/46.10 is false if at least one of the following is false:
% 45.56/46.10 [p5 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 45.56/46.10 1.1.1.1 Assume p5 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 45.66/46.19 Then clause (629 ^ 4) under the substitution [[_214589, _214591, _214593, _214595], [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 45.66/46.19 is false if at least one of the following is false:
% 45.66/46.19 [p4 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 45.66/46.19 1.1.1.1.1 Assume p4 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 45.66/46.19 Then clause (783 ^ 5) under the substitution [[_220353, _220355, _220357, _220359, _220361], [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 45.66/46.19 is false if at least one of the following is false:
% 45.66/46.19 [p1 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 45.66/46.19 1.1.1.1.1.1 Assume p1 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 45.66/46.19 Then clause (924 ^ 6) under the substitution [[_225816, _225818, _225820, _225822, _225824, _225826], [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 45.66/46.19 is false if at least one of the following is false:
% 45.66/46.19 [p4 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 45.66/46.19 1.1.1.1.1.1.1 Assume p4 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 45.84/46.35 Then clause (1250 ^ 7) under the substitution [[_238370, _238372, _238374, _238376, _238378, _238380, _238382], [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 45.84/46.35 is false if at least one of the following is false:
% 45.84/46.35 [p1 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 46.14/46.60 1.1.1.1.1.1.1.1 Assume p1 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 46.14/46.60 Then clause (1413 ^ 8) under the substitution [[_244877, _244879, _244881, _244883, _244885, _244887, _244889, _244891], [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 46.56/47.07 is false if at least one of the following is false:
% 46.56/47.07 [p4 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 47.56/48.03 1.1.1.1.1.1.1.1.1 Assume p4 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 47.56/48.03 Then clause (1781 ^ 9) under the substitution [[_259527, _259529, _259531, _259533, _259535, _259537, _259539, _259541, _259543], [1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 47.56/48.03 is false if at least one of the following is false:
% 49.34/49.88 [p1 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1784 ^ [1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]]
% 51.24/51.74 1.1.1.1.1.1.1.1.1.1 Assume p1 : [4 ^ [], 40 ^ [4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1784 ^ [1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]] is false.
% 53.14/53.66 Then clause (2106 ^ 10) under the substitution [[_272176, _272178, _272180, _272182, _272184, _272186, _272188, _272190, _272192, _272194], [1784 ^ [1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1416 ^ [1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 1253 ^ [927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 927 ^ [786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 786 ^ [632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 632 ^ [442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 442 ^ [141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []], 141 ^ [40 ^ [4 ^ []], 4 ^ []], 40 ^ [4 ^ []], 4 ^ []]]
% 53.14/53.66 is true.
% 53.14/53.66
% 53.14/53.66 Therefore there is no interpretation that makes the
% 53.14/53.66 given matrix false. Hence the given matrix is valid.
% 53.14/53.66 q.e.d.
% 53.14/53.66 ------------------------------------------------------
% 53.14/53.66 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.dRg0hThhdS/theBenchmark.p.qmf
% 53.14/53.66 % nanoCoP-M exiting
%------------------------------------------------------------------------------