%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP109_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n023.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:07 PM UTC 2026
% Result : Theorem 44.71s 45.76s
% Output : Proof 44.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYP109_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : run_nanocopm %s %d
% 0.15/0.34 % Computer : n023.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 17:46:08 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.30/0.48 % Logic is t
% 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.50 %------------------------------------------------------------------------------
% 0.30/0.50 % File : SYP109_1 : TPTP v9.3.0. Released v9.3.0.
% 0.30/0.50 % Domain : Syntactic
% 0.30/0.50 % Problem : Logic KT, problem kath_p, size 10
% 0.30/0.50 % Version : Especial.
% 0.30/0.50 % English :
% 0.30/0.50 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.30/0.50 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.30/0.50 % Source : [Ste24]
% 0.30/0.50 % Names : KT/k_path_p/10.p
% 0.30/0.50 % Status : Theorem
% 0.30/0.50 % Rating : ? v9.2.0
% 0.30/0.50 % Syntax : Number of formulae : 7 ( 0 unt; 6 typ; 0 def)
% 0.30/0.50 % Number of atoms : 351 ( 0 equ)
% 0.30/0.50 % Maximal formula atoms : 351 ( 351 avg)
% 0.30/0.50 % Number of connectives : 1385 ( 145 ~; 209 |; 141 &)
% 0.30/0.50 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.30/0.50 % ( 890 {.}; 0 {#})
% 0.30/0.50 % Maximal formula depth : 221 ( 221 avg)
% 0.30/0.50 % Maximal term depth : 0 ( 0 avg)
% 0.30/0.50 % Number of types : 1 ( 0 usr)
% 0.30/0.50 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.30/0.50 % Number of predicates : 7 ( 6 usr; 7 prp; 0-0 aty)
% 0.30/0.50 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.30/0.50 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.30/0.50 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.30/0.50 % Comments :
% 0.30/0.50 %------------------------------------------------------------------------------
% 0.30/0.50 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.50 %------------------------------------------------------------------------------
% 0.30/0.50 ------------ End QMF file ---------------
% 44.71/45.76
% 44.71/45.76 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.Wfs0lqheJa/theBenchmark.p.qmf : (modal (t/const))
% 44.71/45.76 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.Wfs0lqheJa/theBenchmark.p.qmf
% 44.71/45.76 ------------------------------------------------------
% 44.71/45.76 Explanations for the proof presented below:
% 44.71/45.76 - equality axioms are added if required
% 44.71/45.76 - terms and variables are represented by Prolog terms
% 44.71/45.76 and Prolog variables, negation is represented by -
% 44.71/45.76 - a prefix Pre is a list of variables and constants
% 44.71/45.76 and assigned to each literal Lit, i.e. Pre:Lit
% 44.71/45.76 - clauses and (sub-)matrices have a unique label I^K:
% 44.71/45.76 or I^K^[..]:, where I is a unique number/identifier
% 44.71/45.76 and K identifies the instance of clause/matrix I
% 44.71/45.76 - I:Lit refers to literal Lit in clause number I
% 44.71/45.76 - in the matrix, I^[t1,..,tn] may represent the atom
% 44.71/45.76 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 44.71/45.76 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 44.71/45.76 the assignments X1:=t1, .., Xn:=tn (for both term
% 44.71/45.76 and prefix variables)
% 44.71/45.76
% 44.71/45.76 Proof:
% 44.71/45.76 ------
% 44.71/45.76 Translation into a non-clausal matrix:
% 44.71/45.76 [(3 ^ _186051) ^ [] ^ [] : [p1 : [1 ^ []]], (6 ^ _186051) ^ [] ^ [] : [p2 : [4 ^ []]], (9 ^ _186051) ^ [] ^ [] : [p3 : [7 ^ []]], (12 ^ _186051) ^ [] ^ [] : [p5 : [10 ^ []]], (15 ^ _186051) ^ [_186549] ^ [] : [-(p1) : -([_186549]), p3 : [_186549, 18 ^ [_186549]]], (23 ^ _186051) ^ [_186859] ^ [] : [-(p1) : -([_186859]), p5 : [_186859, 26 ^ [_186859]]], (30 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (37 ^ _186051) ^ [_187345] ^ [] : [-(p2) : -([_187345]), p1 : [_187345, 40 ^ [_187345]]], (44 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (51 ^ _186051) ^ [_187831] ^ [] : [-(p3) : -([_187831]), p3 : [_187831, 54 ^ [_187831]]], (59 ^ _186051) ^ [_188141] ^ [] : [-(p3) : -([_188141]), p5 : [_188141, 62 ^ [_188141]]], (66 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (72 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (78 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (85 ^ _186051) ^ [_188979] ^ [] : [-(p5) : -([_188979]), p3 : [_188979, 88 ^ [_188979]]], (93 ^ _186051) ^ [_189289] ^ [] : [-(p5) : -([_189289]), p5 : [_189289, 96 ^ [_189289]]], (100 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (106 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (112 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (120 ^ _186051) ^ [_190148, _190150] ^ [] : [-(p1) : -([_190150, _190148]), p1 : [_190150, _190148, 123 ^ [_190148, _190150]]], (129 ^ _186051) ^ [_190497, _190499] ^ [] : [-(p1) : -([_190499, _190497]), p3 : [_190499, _190497, 132 ^ [_190497, _190499]]], (138 ^ _186051) ^ [_190846, _190848] ^ [] : [-(p1) : -([_190848, _190846]), p6 : [_190848, _190846, 141 ^ [_190846, _190848]]], (147 ^ _186051) ^ [_191195, _191197] ^ [] : [-(p1) : -([_191197, _191195]), p5 : [_191197, _191195, 150 ^ [_191195, _191197]]], (154 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (160 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (167 ^ _186051) ^ [_191875] ^ [] : [-(p4) : -([_191875]), p2 : [_191875, 170 ^ [_191875]]], (175 ^ _186051) ^ [_192185] ^ [] : [-(p6) : -([_192185]), p2 : [_192185, 178 ^ [_192185]]], (184 ^ _186051) ^ [_192516, _192518] ^ [] : [-(p3) : -([_192518, _192516]), p1 : [_192518, _192516, 187 ^ [_192516, _192518]]], (193 ^ _186051) ^ [_192865, _192867] ^ [] : [-(p3) : -([_192867, _192865]), p3 : [_192867, _192865, 196 ^ [_192865, _192867]]], (202 ^ _186051) ^ [_193214, _193216] ^ [] : [-(p3) : -([_193216, _193214]), p5 : [_193216, _193214, 205 ^ [_193214, _193216]]], (209 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (215 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (222 ^ _186051) ^ [_193894] ^ [] : [-(p4) : -([_193894]), p4 : [_193894, 225 ^ [_193894]]], (230 ^ _186051) ^ [_194204] ^ [] : [-(p6) : -([_194204]), p4 : [_194204, 233 ^ [_194204]]], (239 ^ _186051) ^ [_194535, _194537] ^ [] : [-(p5) : -([_194537, _194535]), p1 : [_194537, _194535, 242 ^ [_194535, _194537]]], (248 ^ _186051) ^ [_194884, _194886] ^ [] : [-(p5) : -([_194886, _194884]), p3 : [_194886, _194884, 251 ^ [_194884, _194886]]], (257 ^ _186051) ^ [_195233, _195235] ^ [] : [-(p5) : -([_195235, _195233]), p5 : [_195235, _195233, 260 ^ [_195233, _195235]]], (264 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (270 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (277 ^ _186051) ^ [_195913] ^ [] : [-(p4) : -([_195913]), p6 : [_195913, 280 ^ [_195913]]], (285 ^ _186051) ^ [_196223] ^ [] : [-(p6) : -([_196223]), p6 : [_196223, 288 ^ [_196223]]], (295 ^ _186051) ^ [_196577, _196579, _196581] ^ [] : [-(p1) : -([_196581, _196579, _196577]), p1 : [_196581, _196579, _196577, 298 ^ [_196577, _196579, _196581]]], (305 ^ _186051) ^ [_196967, _196969, _196971] ^ [] : [-(p1) : -([_196971, _196969, _196967]), p3 : [_196971, _196969, _196967, 308 ^ [_196967, _196969, _196971]]], (312 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (318 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (326 ^ _186051) ^ [_197686, _197688] ^ [] : [-(p2) : -([_197688, _197686]), p2 : [_197688, _197686, 329 ^ [_197686, _197688]]], (335 ^ _186051) ^ [_198035, _198037] ^ [] : [-(p4) : -([_198037, _198035]), p2 : [_198037, _198035, 338 ^ [_198035, _198037]]], (344 ^ _186051) ^ [_198384, _198386] ^ [] : [-(p6) : -([_198386, _198384]), p2 : [_198386, _198384, 347 ^ [_198384, _198386]]], (354 ^ _186051) ^ [_198756, _198758, _198760] ^ [] : [-(p3) : -([_198760, _198758, _198756]), p1 : [_198760, _198758, _198756, 357 ^ [_198756, _198758, _198760]]], (364 ^ _186051) ^ [_199146, _199148, _199150] ^ [] : [-(p3) : -([_199150, _199148, _199146]), p3 : [_199150, _199148, _199146, 367 ^ [_199146, _199148, _199150]]], (371 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (377 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (385 ^ _186051) ^ [_199865, _199867] ^ [] : [-(p2) : -([_199867, _199865]), p4 : [_199867, _199865, 388 ^ [_199865, _199867]]], (394 ^ _186051) ^ [_200214, _200216] ^ [] : [-(p4) : -([_200216, _200214]), p4 : [_200216, _200214, 397 ^ [_200214, _200216]]], (403 ^ _186051) ^ [_200563, _200565] ^ [] : [-(p6) : -([_200565, _200563]), p4 : [_200565, _200563, 406 ^ [_200563, _200565]]], (413 ^ _186051) ^ [_200935, _200937, _200939] ^ [] : [-(p5) : -([_200939, _200937, _200935]), p1 : [_200939, _200937, _200935, 416 ^ [_200935, _200937, _200939]]], (423 ^ _186051) ^ [_201325, _201327, _201329] ^ [] : [-(p5) : -([_201329, _201327, _201325]), p3 : [_201329, _201327, _201325, 426 ^ [_201325, _201327, _201329]]], (430 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (439 ^ _186051) ^ [_201891, _201893, _201895] ^ [] : [-(p6) : -([_201895, _201893, _201891]), p5 : [_201895, _201893, _201891, 442 ^ [_201891, _201893, _201895]]], (448 ^ _186051) ^ [_202258, _202260] ^ [] : [-(p2) : -([_202260, _202258]), p6 : [_202260, _202258, 451 ^ [_202258, _202260]]], (457 ^ _186051) ^ [_202607, _202609] ^ [] : [-(p4) : -([_202609, _202607]), p6 : [_202609, _202607, 460 ^ [_202607, _202609]]], (466 ^ _186051) ^ [_202956, _202958] ^ [] : [-(p6) : -([_202958, _202956]), p6 : [_202958, _202956, 469 ^ [_202956, _202958]]], (477 ^ _186051) ^ [_203353, _203355, _203357, _203359] ^ [] : [-(p1) : -([_203359, _203357, _203355, _203353]), p1 : [_203359, _203357, _203355, _203353, 480 ^ [_203353, _203355, _203357, _203359]]], (488 ^ _186051) ^ [_203786, _203788, _203790, _203792] ^ [] : [-(p1) : -([_203792, _203790, _203788, _203786]), p3 : [_203792, _203790, _203788, _203786, 491 ^ [_203786, _203788, _203790, _203792]]], (499 ^ _186051) ^ [_204219, _204221, _204223, _204225] ^ [] : [-(p1) : -([_204225, _204223, _204221, _204219]), p5 : [_204225, _204223, _204221, _204219, 502 ^ [_204219, _204221, _204223, _204225]]], (506 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (512 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (521 ^ _186051) ^ [_204979, _204981, _204983] ^ [] : [-(p2) : -([_204983, _204981, _204979]), p2 : [_204983, _204981, _204979, 524 ^ [_204979, _204981, _204983]]], (531 ^ _186051) ^ [_205369, _205371, _205373] ^ [] : [-(p4) : -([_205373, _205371, _205369]), p2 : [_205373, _205371, _205369, 534 ^ [_205369, _205371, _205373]]], (542 ^ _186051) ^ [_205784, _205786, _205788, _205790] ^ [] : [-(p3) : -([_205790, _205788, _205786, _205784]), p1 : [_205790, _205788, _205786, _205784, 545 ^ [_205784, _205786, _205788, _205790]]], (553 ^ _186051) ^ [_206217, _206219, _206221, _206223] ^ [] : [-(p3) : -([_206223, _206221, _206219, _206217]), p3 : [_206223, _206221, _206219, _206217, 556 ^ [_206217, _206219, _206221, _206223]]], (564 ^ _186051) ^ [_206650, _206652, _206654, _206656] ^ [] : [-(p3) : -([_206656, _206654, _206652, _206650]), p5 : [_206656, _206654, _206652, _206650, 567 ^ [_206650, _206652, _206654, _206656]]], (571 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (577 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (586 ^ _186051) ^ [_207410, _207412, _207414] ^ [] : [-(p2) : -([_207414, _207412, _207410]), p4 : [_207414, _207412, _207410, 589 ^ [_207410, _207412, _207414]]], (596 ^ _186051) ^ [_207800, _207802, _207804] ^ [] : [-(p4) : -([_207804, _207802, _207800]), p4 : [_207804, _207802, _207800, 599 ^ [_207800, _207802, _207804]]], (607 ^ _186051) ^ [_208215, _208217, _208219, _208221] ^ [] : [-(p5) : -([_208221, _208219, _208217, _208215]), p1 : [_208221, _208219, _208217, _208215, 610 ^ [_208215, _208217, _208219, _208221]]], (618 ^ _186051) ^ [_208648, _208650, _208652, _208654] ^ [] : [-(p5) : -([_208654, _208652, _208650, _208648]), p3 : [_208654, _208652, _208650, _208648, 621 ^ [_208648, _208650, _208652, _208654]]], (629 ^ _186051) ^ [_209081, _209083, _209085, _209087] ^ [] : [-(p5) : -([_209087, _209085, _209083, _209081]), p4 : [_209087, _209085, _209083, _209081, 632 ^ [_209081, _209083, _209085, _209087]]], (640 ^ _186051) ^ [_209514, _209516, _209518, _209520] ^ [] : [-(p5) : -([_209520, _209518, _209516, _209514]), p5 : [_209520, _209518, _209516, _209514, 643 ^ [_209514, _209516, _209518, _209520]]], (647 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (653 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (662 ^ _186051) ^ [_210274, _210276, _210278] ^ [] : [-(p2) : -([_210278, _210276, _210274]), p6 : [_210278, _210276, _210274, 665 ^ [_210274, _210276, _210278]]], (672 ^ _186051) ^ [_210664, _210666, _210668] ^ [] : [-(p4) : -([_210668, _210666, _210664]), p6 : [_210668, _210666, _210664, 675 ^ [_210664, _210666, _210668]]], (684 ^ _186051) ^ [_211106, _211108, _211110, _211112, _211114] ^ [] : [-(p1) : -([_211114, _211112, _211110, _211108, _211106]), p3 : [_211114, _211112, _211110, _211108, _211106, 687 ^ [_211106, _211108, _211110, _211112, _211114]]], (696 ^ _186051) ^ [_211584, _211586, _211588, _211590, _211592] ^ [] : [-(p1) : -([_211592, _211590, _211588, _211586, _211584]), p5 : [_211592, _211590, _211588, _211586, _211584, 699 ^ [_211584, _211586, _211588, _211590, _211592]]], (703 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (709 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (719 ^ _186051) ^ [_212387, _212389, _212391, _212393] ^ [] : [-(p2) : -([_212393, _212391, _212389, _212387]), p2 : [_212393, _212391, _212389, _212387, 722 ^ [_212387, _212389, _212391, _212393]]], (730 ^ _186051) ^ [_212820, _212822, _212824, _212826] ^ [] : [-(p4) : -([_212826, _212824, _212822, _212820]), p2 : [_212826, _212824, _212822, _212820, 733 ^ [_212820, _212822, _212824, _212826]]], (741 ^ _186051) ^ [_213253, _213255, _213257, _213259] ^ [] : [-(p6) : -([_213259, _213257, _213255, _213253]), p2 : [_213259, _213257, _213255, _213253, 744 ^ [_213253, _213255, _213257, _213259]]], (753 ^ _186051) ^ [_213713, _213715, _213717, _213719, _213721] ^ [] : [-(p3) : -([_213721, _213719, _213717, _213715, _213713]), p3 : [_213721, _213719, _213717, _213715, _213713, 756 ^ [_213713, _213715, _213717, _213719, _213721]]], (765 ^ _186051) ^ [_214191, _214193, _214195, _214197, _214199] ^ [] : [-(p3) : -([_214199, _214197, _214195, _214193, _214191]), p5 : [_214199, _214197, _214195, _214193, _214191, 768 ^ [_214191, _214193, _214195, _214197, _214199]]], (772 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (783 ^ _186051) ^ [_214845, _214847, _214849, _214851, _214853] ^ [] : [-(p4) : -([_214853, _214851, _214849, _214847, _214845]), p1 : [_214853, _214851, _214849, _214847, _214845, 786 ^ [_214845, _214847, _214849, _214851, _214853]]], (794 ^ _186051) ^ [_215296, _215298, _215300, _215302] ^ [] : [-(p2) : -([_215302, _215300, _215298, _215296]), p4 : [_215302, _215300, _215298, _215296, 797 ^ [_215296, _215298, _215300, _215302]]], (805 ^ _186051) ^ [_215729, _215731, _215733, _215735] ^ [] : [-(p4) : -([_215735, _215733, _215731, _215729]), p4 : [_215735, _215733, _215731, _215729, 808 ^ [_215729, _215731, _215733, _215735]]], (816 ^ _186051) ^ [_216162, _216164, _216166, _216168] ^ [] : [-(p6) : -([_216168, _216166, _216164, _216162]), p4 : [_216168, _216166, _216164, _216162, 819 ^ [_216162, _216164, _216166, _216168]]], (828 ^ _186051) ^ [_216622, _216624, _216626, _216628, _216630] ^ [] : [-(p5) : -([_216630, _216628, _216626, _216624, _216622]), p3 : [_216630, _216628, _216626, _216624, _216622, 831 ^ [_216622, _216624, _216626, _216628, _216630]]], (840 ^ _186051) ^ [_217100, _217102, _217104, _217106, _217108] ^ [] : [-(p5) : -([_217108, _217106, _217104, _217102, _217100]), p5 : [_217108, _217106, _217104, _217102, _217100, 843 ^ [_217100, _217102, _217104, _217106, _217108]]], (847 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (853 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (863 ^ _186051) ^ [_217903, _217905, _217907, _217909] ^ [] : [-(p2) : -([_217909, _217907, _217905, _217903]), p6 : [_217909, _217907, _217905, _217903, 866 ^ [_217903, _217905, _217907, _217909]]], (874 ^ _186051) ^ [_218336, _218338, _218340, _218342] ^ [] : [-(p4) : -([_218342, _218340, _218338, _218336]), p6 : [_218342, _218340, _218338, _218336, 877 ^ [_218336, _218338, _218340, _218342]]], (885 ^ _186051) ^ [_218769, _218771, _218773, _218775] ^ [] : [-(p6) : -([_218775, _218773, _218771, _218769]), p6 : [_218775, _218773, _218771, _218769, 888 ^ [_218769, _218771, _218773, _218775]]], (898 ^ _186051) ^ [_219258, _219260, _219262, _219264, _219266, _219268] ^ [] : [-(p1) : -([_219268, _219266, _219264, _219262, _219260, _219258]), p1 : [_219268, _219266, _219264, _219262, _219260, _219258, 901 ^ [_219258, _219260, _219262, _219264, _219266, _219268]]], (911 ^ _186051) ^ [_219783, _219785, _219787, _219789, _219791, _219793] ^ [] : [-(p1) : -([_219793, _219791, _219789, _219787, _219785, _219783]), p3 : [_219793, _219791, _219789, _219787, _219785, _219783, 914 ^ [_219783, _219785, _219787, _219789, _219791, _219793]]], (924 ^ _186051) ^ [_220308, _220310, _220312, _220314, _220316, _220318] ^ [] : [-(p1) : -([_220318, _220316, _220314, _220312, _220310, _220308]), p4 : [_220318, _220316, _220314, _220312, _220310, _220308, 927 ^ [_220308, _220310, _220312, _220314, _220316, _220318]]], (937 ^ _186051) ^ [_220833, _220835, _220837, _220839, _220841, _220843] ^ [] : [-(p1) : -([_220843, _220841, _220839, _220837, _220835, _220833]), p5 : [_220843, _220841, _220839, _220837, _220835, _220833, 940 ^ [_220833, _220835, _220837, _220839, _220841, _220843]]], (944 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (950 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (961 ^ _186051) ^ [_221681, _221683, _221685, _221687, _221689] ^ [] : [-(p2) : -([_221689, _221687, _221685, _221683, _221681]), p2 : [_221689, _221687, _221685, _221683, _221681, 964 ^ [_221681, _221683, _221685, _221687, _221689]]], (973 ^ _186051) ^ [_222159, _222161, _222163, _222165, _222167] ^ [] : [-(p6) : -([_222167, _222165, _222163, _222161, _222159]), p2 : [_222167, _222165, _222163, _222161, _222159, 976 ^ [_222159, _222161, _222163, _222165, _222167]]], (986 ^ _186051) ^ [_222666, _222668, _222670, _222672, _222674, _222676] ^ [] : [-(p3) : -([_222676, _222674, _222672, _222670, _222668, _222666]), p1 : [_222676, _222674, _222672, _222670, _222668, _222666, 989 ^ [_222666, _222668, _222670, _222672, _222674, _222676]]], (999 ^ _186051) ^ [_223191, _223193, _223195, _223197, _223199, _223201] ^ [] : [-(p3) : -([_223201, _223199, _223197, _223195, _223193, _223191]), p3 : [_223201, _223199, _223197, _223195, _223193, _223191, 1002 ^ [_223191, _223193, _223195, _223197, _223199, _223201]]], (1012 ^ _186051) ^ [_223716, _223718, _223720, _223722, _223724, _223726] ^ [] : [-(p3) : -([_223726, _223724, _223722, _223720, _223718, _223716]), p5 : [_223726, _223724, _223722, _223720, _223718, _223716, 1015 ^ [_223716, _223718, _223720, _223722, _223724, _223726]]], (1019 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1025 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1036 ^ _186051) ^ [_224564, _224566, _224568, _224570, _224572] ^ [] : [-(p2) : -([_224572, _224570, _224568, _224566, _224564]), p4 : [_224572, _224570, _224568, _224566, _224564, 1039 ^ [_224564, _224566, _224568, _224570, _224572]]], (1048 ^ _186051) ^ [_225042, _225044, _225046, _225048, _225050] ^ [] : [-(p6) : -([_225050, _225048, _225046, _225044, _225042]), p4 : [_225050, _225048, _225046, _225044, _225042, 1051 ^ [_225042, _225044, _225046, _225048, _225050]]], (1061 ^ _186051) ^ [_225549, _225551, _225553, _225555, _225557, _225559] ^ [] : [-(p5) : -([_225559, _225557, _225555, _225553, _225551, _225549]), p1 : [_225559, _225557, _225555, _225553, _225551, _225549, 1064 ^ [_225549, _225551, _225553, _225555, _225557, _225559]]], (1074 ^ _186051) ^ [_226074, _226076, _226078, _226080, _226082, _226084] ^ [] : [-(p5) : -([_226084, _226082, _226080, _226078, _226076, _226074]), p3 : [_226084, _226082, _226080, _226078, _226076, _226074, 1077 ^ [_226074, _226076, _226078, _226080, _226082, _226084]]], (1087 ^ _186051) ^ [_226599, _226601, _226603, _226605, _226607, _226609] ^ [] : [-(p5) : -([_226609, _226607, _226605, _226603, _226601, _226599]), p5 : [_226609, _226607, _226605, _226603, _226601, _226599, 1090 ^ [_226599, _226601, _226603, _226605, _226607, _226609]]], (1094 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1100 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1111 ^ _186051) ^ [_227447, _227449, _227451, _227453, _227455] ^ [] : [-(p2) : -([_227455, _227453, _227451, _227449, _227447]), p6 : [_227455, _227453, _227451, _227449, _227447, 1114 ^ [_227447, _227449, _227451, _227453, _227455]]], (1123 ^ _186051) ^ [_227925, _227927, _227929, _227931, _227933] ^ [] : [-(p6) : -([_227933, _227931, _227929, _227927, _227925]), p6 : [_227933, _227931, _227929, _227927, _227925, 1126 ^ [_227925, _227927, _227929, _227931, _227933]]], (1137 ^ _186051) ^ [_228463, _228465, _228467, _228469, _228471, _228473, _228475] ^ [] : [-(p1) : -([_228475, _228473, _228471, _228469, _228467, _228465, _228463]), p3 : [_228475, _228473, _228471, _228469, _228467, _228465, _228463, 1140 ^ [_228463, _228465, _228467, _228469, _228471, _228473, _228475]]], (1151 ^ _186051) ^ [_229037, _229039, _229041, _229043, _229045, _229047, _229049] ^ [] : [-(p1) : -([_229049, _229047, _229045, _229043, _229041, _229039, _229037]), p5 : [_229049, _229047, _229045, _229043, _229041, _229039, _229037, 1154 ^ [_229037, _229039, _229041, _229043, _229045, _229047, _229049]]], (1158 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1164 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1176 ^ _186051) ^ [_229932, _229934, _229936, _229938, _229940, _229942] ^ [] : [-(p2) : -([_229942, _229940, _229938, _229936, _229934, _229932]), p2 : [_229942, _229940, _229938, _229936, _229934, _229932, 1179 ^ [_229932, _229934, _229936, _229938, _229940, _229942]]], (1189 ^ _186051) ^ [_230457, _230459, _230461, _230463, _230465, _230467] ^ [] : [-(p4) : -([_230467, _230465, _230463, _230461, _230459, _230457]), p2 : [_230467, _230465, _230463, _230461, _230459, _230457, 1192 ^ [_230457, _230459, _230461, _230463, _230465, _230467]]], (1202 ^ _186051) ^ [_230982, _230984, _230986, _230988, _230990, _230992] ^ [] : [-(p6) : -([_230992, _230990, _230988, _230986, _230984, _230982]), p2 : [_230992, _230990, _230988, _230986, _230984, _230982, 1205 ^ [_230982, _230984, _230986, _230988, _230990, _230992]]], (1216 ^ _186051) ^ [_231538, _231540, _231542, _231544, _231546, _231548, _231550] ^ [] : [-(p3) : -([_231550, _231548, _231546, _231544, _231542, _231540, _231538]), p3 : [_231550, _231548, _231546, _231544, _231542, _231540, _231538, 1219 ^ [_231538, _231540, _231542, _231544, _231546, _231548, _231550]]], (1230 ^ _186051) ^ [_232112, _232114, _232116, _232118, _232120, _232122, _232124] ^ [] : [-(p3) : -([_232124, _232122, _232120, _232118, _232116, _232114, _232112]), p5 : [_232124, _232122, _232120, _232118, _232116, _232114, _232112, 1233 ^ [_232112, _232114, _232116, _232118, _232120, _232122, _232124]]], (1237 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1250 ^ _186051) ^ [_232862, _232864, _232866, _232868, _232870, _232872, _232874] ^ [] : [-(p4) : -([_232874, _232872, _232870, _232868, _232866, _232864, _232862]), p1 : [_232874, _232872, _232870, _232868, _232866, _232864, _232862, 1253 ^ [_232862, _232864, _232866, _232868, _232870, _232872, _232874]]], (1263 ^ _186051) ^ [_233405, _233407, _233409, _233411, _233413, _233415] ^ [] : [-(p2) : -([_233415, _233413, _233411, _233409, _233407, _233405]), p4 : [_233415, _233413, _233411, _233409, _233407, _233405, 1266 ^ [_233405, _233407, _233409, _233411, _233413, _233415]]], (1276 ^ _186051) ^ [_233930, _233932, _233934, _233936, _233938, _233940] ^ [] : [-(p4) : -([_233940, _233938, _233936, _233934, _233932, _233930]), p4 : [_233940, _233938, _233936, _233934, _233932, _233930, 1279 ^ [_233930, _233932, _233934, _233936, _233938, _233940]]], (1289 ^ _186051) ^ [_234455, _234457, _234459, _234461, _234463, _234465] ^ [] : [-(p6) : -([_234465, _234463, _234461, _234459, _234457, _234455]), p4 : [_234465, _234463, _234461, _234459, _234457, _234455, 1292 ^ [_234455, _234457, _234459, _234461, _234463, _234465]]], (1303 ^ _186051) ^ [_235011, _235013, _235015, _235017, _235019, _235021, _235023] ^ [] : [-(p5) : -([_235023, _235021, _235019, _235017, _235015, _235013, _235011]), p3 : [_235023, _235021, _235019, _235017, _235015, _235013, _235011, 1306 ^ [_235011, _235013, _235015, _235017, _235019, _235021, _235023]]], (1317 ^ _186051) ^ [_235585, _235587, _235589, _235591, _235593, _235595, _235597] ^ [] : [-(p5) : -([_235597, _235595, _235593, _235591, _235589, _235587, _235585]), p5 : [_235597, _235595, _235593, _235591, _235589, _235587, _235585, 1320 ^ [_235585, _235587, _235589, _235591, _235593, _235595, _235597]]], (1324 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1330 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1342 ^ _186051) ^ [_236480, _236482, _236484, _236486, _236488, _236490] ^ [] : [-(p2) : -([_236490, _236488, _236486, _236484, _236482, _236480]), p6 : [_236490, _236488, _236486, _236484, _236482, _236480, 1345 ^ [_236480, _236482, _236484, _236486, _236488, _236490]]], (1355 ^ _186051) ^ [_237005, _237007, _237009, _237011, _237013, _237015] ^ [] : [-(p4) : -([_237015, _237013, _237011, _237009, _237007, _237005]), p6 : [_237015, _237013, _237011, _237009, _237007, _237005, 1358 ^ [_237005, _237007, _237009, _237011, _237013, _237015]]], (1368 ^ _186051) ^ [_237530, _237532, _237534, _237536, _237538, _237540] ^ [] : [-(p6) : -([_237540, _237538, _237536, _237534, _237532, _237530]), p6 : [_237540, _237538, _237536, _237534, _237532, _237530, 1371 ^ [_237530, _237532, _237534, _237536, _237538, _237540]]], (1383 ^ _186051) ^ [_238119, _238121, _238123, _238125, _238127, _238129, _238131, _238133] ^ [] : [-(p1) : -([_238133, _238131, _238129, _238127, _238125, _238123, _238121, _238119]), p1 : [_238133, _238131, _238129, _238127, _238125, _238123, _238121, _238119, 1386 ^ [_238119, _238121, _238123, _238125, _238127, _238129, _238131, _238133]]], (1398 ^ _186051) ^ [_238744, _238746, _238748, _238750, _238752, _238754, _238756, _238758] ^ [] : [-(p1) : -([_238758, _238756, _238754, _238752, _238750, _238748, _238746, _238744]), p3 : [_238758, _238756, _238754, _238752, _238750, _238748, _238746, _238744, 1401 ^ [_238744, _238746, _238748, _238750, _238752, _238754, _238756, _238758]]], (1413 ^ _186051) ^ [_239369, _239371, _239373, _239375, _239377, _239379, _239381, _239383] ^ [] : [-(p1) : -([_239383, _239381, _239379, _239377, _239375, _239373, _239371, _239369]), p4 : [_239383, _239381, _239379, _239377, _239375, _239373, _239371, _239369, 1416 ^ [_239369, _239371, _239373, _239375, _239377, _239379, _239381, _239383]]], (1428 ^ _186051) ^ [_239994, _239996, _239998, _240000, _240002, _240004, _240006, _240008] ^ [] : [-(p1) : -([_240008, _240006, _240004, _240002, _240000, _239998, _239996, _239994]), p5 : [_240008, _240006, _240004, _240002, _240000, _239998, _239996, _239994, 1431 ^ [_239994, _239996, _239998, _240000, _240002, _240004, _240006, _240008]]], (1435 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1441 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1454 ^ _186051) ^ [_240938, _240940, _240942, _240944, _240946, _240948, _240950] ^ [] : [-(p2) : -([_240950, _240948, _240946, _240944, _240942, _240940, _240938]), p2 : [_240950, _240948, _240946, _240944, _240942, _240940, _240938, 1457 ^ [_240938, _240940, _240942, _240944, _240946, _240948, _240950]]], (1468 ^ _186051) ^ [_241512, _241514, _241516, _241518, _241520, _241522, _241524] ^ [] : [-(p6) : -([_241524, _241522, _241520, _241518, _241516, _241514, _241512]), p2 : [_241524, _241522, _241520, _241518, _241516, _241514, _241512, 1471 ^ [_241512, _241514, _241516, _241518, _241520, _241522, _241524]]], (1483 ^ _186051) ^ [_242119, _242121, _242123, _242125, _242127, _242129, _242131, _242133] ^ [] : [-(p3) : -([_242133, _242131, _242129, _242127, _242125, _242123, _242121, _242119]), p1 : [_242133, _242131, _242129, _242127, _242125, _242123, _242121, _242119, 1486 ^ [_242119, _242121, _242123, _242125, _242127, _242129, _242131, _242133]]], (1498 ^ _186051) ^ [_242744, _242746, _242748, _242750, _242752, _242754, _242756, _242758] ^ [] : [-(p3) : -([_242758, _242756, _242754, _242752, _242750, _242748, _242746, _242744]), p3 : [_242758, _242756, _242754, _242752, _242750, _242748, _242746, _242744, 1501 ^ [_242744, _242746, _242748, _242750, _242752, _242754, _242756, _242758]]], (1513 ^ _186051) ^ [_243369, _243371, _243373, _243375, _243377, _243379, _243381, _243383] ^ [] : [-(p3) : -([_243383, _243381, _243379, _243377, _243375, _243373, _243371, _243369]), p5 : [_243383, _243381, _243379, _243377, _243375, _243373, _243371, _243369, 1516 ^ [_243369, _243371, _243373, _243375, _243377, _243379, _243381, _243383]]], (1520 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1526 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1539 ^ _186051) ^ [_244313, _244315, _244317, _244319, _244321, _244323, _244325] ^ [] : [-(p2) : -([_244325, _244323, _244321, _244319, _244317, _244315, _244313]), p4 : [_244325, _244323, _244321, _244319, _244317, _244315, _244313, 1542 ^ [_244313, _244315, _244317, _244319, _244321, _244323, _244325]]], (1553 ^ _186051) ^ [_244887, _244889, _244891, _244893, _244895, _244897, _244899] ^ [] : [-(p6) : -([_244899, _244897, _244895, _244893, _244891, _244889, _244887]), p4 : [_244899, _244897, _244895, _244893, _244891, _244889, _244887, 1556 ^ [_244887, _244889, _244891, _244893, _244895, _244897, _244899]]], (1568 ^ _186051) ^ [_245494, _245496, _245498, _245500, _245502, _245504, _245506, _245508] ^ [] : [-(p5) : -([_245508, _245506, _245504, _245502, _245500, _245498, _245496, _245494]), p1 : [_245508, _245506, _245504, _245502, _245500, _245498, _245496, _245494, 1571 ^ [_245494, _245496, _245498, _245500, _245502, _245504, _245506, _245508]]], (1583 ^ _186051) ^ [_246119, _246121, _246123, _246125, _246127, _246129, _246131, _246133] ^ [] : [-(p5) : -([_246133, _246131, _246129, _246127, _246125, _246123, _246121, _246119]), p3 : [_246133, _246131, _246129, _246127, _246125, _246123, _246121, _246119, 1586 ^ [_246119, _246121, _246123, _246125, _246127, _246129, _246131, _246133]]], (1598 ^ _186051) ^ [_246744, _246746, _246748, _246750, _246752, _246754, _246756, _246758] ^ [] : [-(p5) : -([_246758, _246756, _246754, _246752, _246750, _246748, _246746, _246744]), p5 : [_246758, _246756, _246754, _246752, _246750, _246748, _246746, _246744, 1601 ^ [_246744, _246746, _246748, _246750, _246752, _246754, _246756, _246758]]], (1605 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1611 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1624 ^ _186051) ^ [_247688, _247690, _247692, _247694, _247696, _247698, _247700] ^ [] : [-(p2) : -([_247700, _247698, _247696, _247694, _247692, _247690, _247688]), p6 : [_247700, _247698, _247696, _247694, _247692, _247690, _247688, 1627 ^ [_247688, _247690, _247692, _247694, _247696, _247698, _247700]]], (1638 ^ _186051) ^ [_248262, _248264, _248266, _248268, _248270, _248272, _248274] ^ [] : [-(p6) : -([_248274, _248272, _248270, _248268, _248266, _248264, _248262]), p6 : [_248274, _248272, _248270, _248268, _248266, _248264, _248262, 1641 ^ [_248262, _248264, _248266, _248268, _248270, _248272, _248274]]], (1654 ^ _186051) ^ [_248904, _248906, _248908, _248910, _248912, _248914, _248916, _248918, _248920] ^ [] : [-(p1) : -([_248920, _248918, _248916, _248914, _248912, _248910, _248908, _248906, _248904]), p3 : [_248920, _248918, _248916, _248914, _248912, _248910, _248908, _248906, _248904, 1657 ^ [_248904, _248906, _248908, _248910, _248912, _248914, _248916, _248918, _248920]]], (1670 ^ _186051) ^ [_249582, _249584, _249586, _249588, _249590, _249592, _249594, _249596, _249598] ^ [] : [-(p1) : -([_249598, _249596, _249594, _249592, _249590, _249588, _249586, _249584, _249582]), p5 : [_249598, _249596, _249594, _249592, _249590, _249588, _249586, _249584, _249582, 1673 ^ [_249582, _249584, _249586, _249588, _249590, _249592, _249594, _249596, _249598]]], (1677 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1683 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1697 ^ _186051) ^ [_250577, _250579, _250581, _250583, _250585, _250587, _250589, _250591] ^ [] : [-(p2) : -([_250591, _250589, _250587, _250585, _250583, _250581, _250579, _250577]), p2 : [_250591, _250589, _250587, _250585, _250583, _250581, _250579, _250577, 1700 ^ [_250577, _250579, _250581, _250583, _250585, _250587, _250589, _250591]]], (1712 ^ _186051) ^ [_251202, _251204, _251206, _251208, _251210, _251212, _251214, _251216] ^ [] : [-(p4) : -([_251216, _251214, _251212, _251210, _251208, _251206, _251204, _251202]), p2 : [_251216, _251214, _251212, _251210, _251208, _251206, _251204, _251202, 1715 ^ [_251202, _251204, _251206, _251208, _251210, _251212, _251214, _251216]]], (1727 ^ _186051) ^ [_251827, _251829, _251831, _251833, _251835, _251837, _251839, _251841] ^ [] : [-(p6) : -([_251841, _251839, _251837, _251835, _251833, _251831, _251829, _251827]), p2 : [_251841, _251839, _251837, _251835, _251833, _251831, _251829, _251827, 1730 ^ [_251827, _251829, _251831, _251833, _251835, _251837, _251839, _251841]]], (1743 ^ _186051) ^ [_252487, _252489, _252491, _252493, _252495, _252497, _252499, _252501, _252503] ^ [] : [-(p3) : -([_252503, _252501, _252499, _252497, _252495, _252493, _252491, _252489, _252487]), p3 : [_252503, _252501, _252499, _252497, _252495, _252493, _252491, _252489, _252487, 1746 ^ [_252487, _252489, _252491, _252493, _252495, _252497, _252499, _252501, _252503]]], (1759 ^ _186051) ^ [_253165, _253167, _253169, _253171, _253173, _253175, _253177, _253179, _253181] ^ [] : [-(p3) : -([_253181, _253179, _253177, _253175, _253173, _253171, _253169, _253167, _253165]), p5 : [_253181, _253179, _253177, _253175, _253173, _253171, _253169, _253167, _253165, 1762 ^ [_253165, _253167, _253169, _253171, _253173, _253175, _253177, _253179, _253181]]], (1766 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1781 ^ _186051) ^ [_254019, _254021, _254023, _254025, _254027, _254029, _254031, _254033, _254035] ^ [] : [-(p4) : -([_254035, _254033, _254031, _254029, _254027, _254025, _254023, _254021, _254019]), p1 : [_254035, _254033, _254031, _254029, _254027, _254025, _254023, _254021, _254019, 1784 ^ [_254019, _254021, _254023, _254025, _254027, _254029, _254031, _254033, _254035]]], (1796 ^ _186051) ^ [_254662, _254664, _254666, _254668, _254670, _254672, _254674, _254676] ^ [] : [-(p2) : -([_254676, _254674, _254672, _254670, _254668, _254666, _254664, _254662]), p4 : [_254676, _254674, _254672, _254670, _254668, _254666, _254664, _254662, 1799 ^ [_254662, _254664, _254666, _254668, _254670, _254672, _254674, _254676]]], (1811 ^ _186051) ^ [_255287, _255289, _255291, _255293, _255295, _255297, _255299, _255301] ^ [] : [-(p4) : -([_255301, _255299, _255297, _255295, _255293, _255291, _255289, _255287]), p4 : [_255301, _255299, _255297, _255295, _255293, _255291, _255289, _255287, 1814 ^ [_255287, _255289, _255291, _255293, _255295, _255297, _255299, _255301]]], (1826 ^ _186051) ^ [_255912, _255914, _255916, _255918, _255920, _255922, _255924, _255926] ^ [] : [-(p6) : -([_255926, _255924, _255922, _255920, _255918, _255916, _255914, _255912]), p4 : [_255926, _255924, _255922, _255920, _255918, _255916, _255914, _255912, 1829 ^ [_255912, _255914, _255916, _255918, _255920, _255922, _255924, _255926]]], (1842 ^ _186051) ^ [_256572, _256574, _256576, _256578, _256580, _256582, _256584, _256586, _256588] ^ [] : [-(p5) : -([_256588, _256586, _256584, _256582, _256580, _256578, _256576, _256574, _256572]), p3 : [_256588, _256586, _256584, _256582, _256580, _256578, _256576, _256574, _256572, 1845 ^ [_256572, _256574, _256576, _256578, _256580, _256582, _256584, _256586, _256588]]], (1858 ^ _186051) ^ [_257250, _257252, _257254, _257256, _257258, _257260, _257262, _257264, _257266] ^ [] : [-(p5) : -([_257266, _257264, _257262, _257260, _257258, _257256, _257254, _257252, _257250]), p5 : [_257266, _257264, _257262, _257260, _257258, _257256, _257254, _257252, _257250, 1861 ^ [_257250, _257252, _257254, _257256, _257258, _257260, _257262, _257264, _257266]]], (1865 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1871 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1885 ^ _186051) ^ [_258245, _258247, _258249, _258251, _258253, _258255, _258257, _258259] ^ [] : [-(p2) : -([_258259, _258257, _258255, _258253, _258251, _258249, _258247, _258245]), p6 : [_258259, _258257, _258255, _258253, _258251, _258249, _258247, _258245, 1888 ^ [_258245, _258247, _258249, _258251, _258253, _258255, _258257, _258259]]], (1900 ^ _186051) ^ [_258870, _258872, _258874, _258876, _258878, _258880, _258882, _258884] ^ [] : [-(p4) : -([_258884, _258882, _258880, _258878, _258876, _258874, _258872, _258870]), p6 : [_258884, _258882, _258880, _258878, _258876, _258874, _258872, _258870, 1903 ^ [_258870, _258872, _258874, _258876, _258878, _258880, _258882, _258884]]], (1915 ^ _186051) ^ [_259495, _259497, _259499, _259501, _259503, _259505, _259507, _259509] ^ [] : [-(p6) : -([_259509, _259507, _259505, _259503, _259501, _259499, _259497, _259495]), p6 : [_259509, _259507, _259505, _259503, _259501, _259499, _259497, _259495, 1918 ^ [_259495, _259497, _259499, _259501, _259503, _259505, _259507, _259509]]], (1922 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1928 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1934 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1949 ^ _186051) ^ [_260683, _260685, _260687, _260689, _260691, _260693, _260695, _260697, _260699] ^ [] : [-(p2) : -([_260699, _260697, _260695, _260693, _260691, _260689, _260687, _260685, _260683]), p2 : [_260699, _260697, _260695, _260693, _260691, _260689, _260687, _260685, _260683, 1952 ^ [_260683, _260685, _260687, _260689, _260691, _260693, _260695, _260697, _260699]]], (1965 ^ _186051) ^ [_261361, _261363, _261365, _261367, _261369, _261371, _261373, _261375, _261377] ^ [] : [-(p6) : -([_261377, _261375, _261373, _261371, _261369, _261367, _261365, _261363, _261361]), p2 : [_261377, _261375, _261373, _261371, _261369, _261367, _261365, _261363, _261361, 1968 ^ [_261361, _261363, _261365, _261367, _261369, _261371, _261373, _261375, _261377]]], (1972 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1978 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1984 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1999 ^ _186051) ^ [_262567, _262569, _262571, _262573, _262575, _262577, _262579, _262581, _262583] ^ [] : [-(p2) : -([_262583, _262581, _262579, _262577, _262575, _262573, _262571, _262569, _262567]), p4 : [_262583, _262581, _262579, _262577, _262575, _262573, _262571, _262569, _262567, 2002 ^ [_262567, _262569, _262571, _262573, _262575, _262577, _262579, _262581, _262583]]], (2015 ^ _186051) ^ [_263245, _263247, _263249, _263251, _263253, _263255, _263257, _263259, _263261] ^ [] : [-(p6) : -([_263261, _263259, _263257, _263255, _263253, _263251, _263249, _263247, _263245]), p4 : [_263261, _263259, _263257, _263255, _263253, _263251, _263249, _263247, _263245, 2018 ^ [_263245, _263247, _263249, _263251, _263253, _263255, _263257, _263259, _263261]]], (2022 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2028 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2034 ^ _186051) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2049 ^ _186051) ^ [_264451, _264453, _264455, _264457, _264459, _264461, _264463, _264465, _264467] ^ [] : [-(p2) : -([_264467, _264465, _264463, _264461, _264459, _264457, _264455, _264453, _264451]), p6 : [_264467, _264465, _264463, _264461, _264459, _264457, _264455, _264453, _264451, 2052 ^ [_264451, _264453, _264455, _264457, _264459, _264461, _264463, _264465, _264467]]], (2082 ^ _186051) ^ [_265838, _265840, _265842, _265844, _265846, _265848, _265850, _265852, _265854, _265856] ^ [] : [-(p2) : -([_265856, _265854, _265852, _265850, _265848, _265846, _265844, _265842, _265840, _265838])], (2094 ^ _186051) ^ [_266253, _266255, _266257, _266259, _266261, _266263, _266265, _266267, _266269, _266271] ^ [] : [-(p4) : -([_266271, _266269, _266267, _266265, _266263, _266261, _266259, _266257, _266255, _266253])], (2106 ^ _186051) ^ [_266668, _266670, _266672, _266674, _266676, _266678, _266680, _266682, _266684, _266686] ^ [] : [-(p1) : -([_266686, _266684, _266682, _266680, _266678, _266676, _266674, _266672, _266670, _266668])], (2118 ^ _186051) ^ [_267060, _267062, _267064, _267066, _267068, _267070, _267072, _267074, _267076, _267078] ^ [] : [-(p6) : -([_267078, _267076, _267074, _267072, _267070, _267068, _267066, _267064, _267062, _267060])], (2065 ^ _186051) ^ [_265129, _265131, _265133, _265135, _265137, _265139, _265141, _265143, _265145] ^ [] : [-(p6) : -([_265145, _265143, _265141, _265139, _265137, _265135, _265133, _265131, _265129]), p6 : [_265145, _265143, _265141, _265139, _265137, _265135, _265133, _265131, _265129, 2068 ^ [_265129, _265131, _265133, _265135, _265137, _265139, _265141, _265143, _265145]]]]
% 44.71/45.76
% 44.71/45.76 We prove that the given matrix is valid, i.e. for
% 44.71/45.76 a given substitution it evaluates to true for all
% 44.71/45.76 interpretations. A matrix is true iff at least one
% 44.71/45.76 of its clauses is true; a clause is true iff all of
% 44.71/45.76 its elements (literals and submatrices) are true.
% 44.71/45.76
% 44.71/45.76 The proof is by contradiction:
% 44.71/45.76 Assume there is an interpretation so that the given
% 44.71/45.76 matrix evaluates to false. Then in each clause there
% 44.71/45.76 has to be at least one element that is false.
% 44.71/45.76
% 44.71/45.76 Then clause (3 ^ 0) is false if at least one of the following is false:
% 44.71/45.76 [p1 : [1 ^ []]]
% 44.71/45.76 1 Assume p1 : [[], [], [], [], [], [], [], [], [], 1 ^ []] is false.
% 44.71/45.76 Then clause (2106 ^ 1) under the substitution [[_266668, _266670, _266672, _266674, _266676, _266678, _266680, _266682, _266684, _266686], [1 ^ [], [], [], [], [], [], [], [], [], []]]
% 44.71/45.76 is true.
% 44.71/45.76
% 44.71/45.76 Therefore there is no interpretation that makes the
% 44.71/45.76 given matrix false. Hence the given matrix is valid.
% 44.71/45.76 q.e.d.
% 44.71/45.76 ------------------------------------------------------
% 44.71/45.76 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.Wfs0lqheJa/theBenchmark.p.qmf
% 44.71/45.76 % nanoCoP-M exiting
%------------------------------------------------------------------------------