%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP108_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n016.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 62.86s 64.24s
% Output : Proof 62.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.19 % Problem : SYP108_1 : TPTP v9.3.0. Released v9.3.0.
% 0.04/0.19 % Command : run_nanocopm %s %d
% 0.12/0.41 % Computer : n016.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8042.1875MB
% 0.12/0.41 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Mon May 4 17:45:51 EDT 2026
% 0.12/0.42 % CPUTime :
% 0.22/0.62 % Logic is t
% 0.22/0.63 % Designation is rigid
% 0.22/0.63 % Terms are local
% 0.22/0.63 % Domains are const
% 0.22/0.65 ------------ Start QMF file ---------------
% 0.22/0.65 %------------------------------------------------------------------------------
% 0.22/0.65 % File : SYP108_1 : TPTP v9.3.0. Released v9.3.0.
% 0.22/0.65 % Domain : Syntactic
% 0.22/0.65 % Problem : Logic KT, problem k_path, size 10
% 0.22/0.65 % Version : Especial.
% 0.22/0.65 % English :
% 0.22/0.65 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.22/0.65 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.22/0.65 % Source : [Ste24]
% 0.22/0.65 % Names : KT/k_path_n/10.p
% 0.22/0.65 % Status : CounterSatisfiable
% 0.22/0.65 % Rating : ? v9.2.0
% 0.22/0.65 % Syntax : Number of formulae : 7 ( 0 unt; 6 typ; 0 def)
% 0.22/0.65 % Number of atoms : 394 ( 0 equ)
% 0.22/0.65 % Maximal formula atoms : 394 ( 394 avg)
% 0.22/0.65 % Number of connectives : 1653 ( 163 ~; 234 |; 159 &)
% 0.22/0.65 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.22/0.65 % (1097 {.}; 0 {#})
% 0.22/0.65 % Maximal formula depth : 247 ( 247 avg)
% 0.22/0.65 % Maximal term depth : 0 ( 0 avg)
% 0.22/0.65 % Number of types : 1 ( 0 usr)
% 0.22/0.65 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.22/0.65 % Number of predicates : 7 ( 6 usr; 7 prp; 0-0 aty)
% 0.22/0.65 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.22/0.65 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.22/0.65 % SPC : NX0_CSA_PRP_NEQ_NAR
% 0.22/0.65 % Comments :
% 0.22/0.65 %------------------------------------------------------------------------------
% 0.22/0.65 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 | $false | #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 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p1 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) ) ) | $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 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p3 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) ) ) | $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 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p1 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p3 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p5 ) & #box : ( p5 ) ) ) ) ) ) ) ) ) ) ) | $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 ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p2 ) ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p4 ) ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) & #box : ( p6 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p2 ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p4 ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p6 ) ) ) ) ) ) ) ) ) ) ) ) )).
% 0.22/0.65 %------------------------------------------------------------------------------
% 0.22/0.65 ------------ End QMF file ---------------
% 62.86/64.24
% 62.86/64.24 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.vSC3cRZDxQ/theBenchmark.p.qmf : (modal (t/const))
% 62.86/64.24 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.vSC3cRZDxQ/theBenchmark.p.qmf
% 62.86/64.24 ------------------------------------------------------
% 62.86/64.24 Explanations for the proof presented below:
% 62.86/64.24 - equality axioms are added if required
% 62.86/64.24 - terms and variables are represented by Prolog terms
% 62.86/64.24 and Prolog variables, negation is represented by -
% 62.86/64.24 - a prefix Pre is a list of variables and constants
% 62.86/64.24 and assigned to each literal Lit, i.e. Pre:Lit
% 62.86/64.24 - clauses and (sub-)matrices have a unique label I^K:
% 62.86/64.24 or I^K^[..]:, where I is a unique number/identifier
% 62.86/64.24 and K identifies the instance of clause/matrix I
% 62.86/64.24 - I:Lit refers to literal Lit in clause number I
% 62.86/64.24 - in the matrix, I^[t1,..,tn] may represent the atom
% 62.86/64.24 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 62.86/64.24 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 62.86/64.24 the assignments X1:=t1, .., Xn:=tn (for both term
% 62.86/64.24 and prefix variables)
% 62.86/64.24
% 62.86/64.24 Proof:
% 62.86/64.24 ------
% 62.86/64.24 Translation into a non-clausal matrix:
% 62.86/64.24 [(3 ^ _219113) ^ [] ^ [] : [p1 : [1 ^ []]], (6 ^ _219113) ^ [] ^ [] : [p2 : [4 ^ []]], (9 ^ _219113) ^ [] ^ [] : [p3 : [7 ^ []]], (12 ^ _219113) ^ [] ^ [] : [p5 : [10 ^ []]], (15 ^ _219113) ^ [_219611] ^ [] : [-(p1) : -([_219611]), p3 : [_219611, 18 ^ [_219611]]], (23 ^ _219113) ^ [_219921] ^ [] : [-(p1) : -([_219921]), p5 : [_219921, 26 ^ [_219921]]], (30 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (37 ^ _219113) ^ [_220407] ^ [] : [-(p2) : -([_220407]), p1 : [_220407, 40 ^ [_220407]]], (44 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (51 ^ _219113) ^ [_220893] ^ [] : [-(p3) : -([_220893]), p3 : [_220893, 54 ^ [_220893]]], (59 ^ _219113) ^ [_221203] ^ [] : [-(p3) : -([_221203]), p5 : [_221203, 62 ^ [_221203]]], (66 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (72 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (78 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (85 ^ _219113) ^ [_222041] ^ [] : [-(p5) : -([_222041]), p3 : [_222041, 88 ^ [_222041]]], (93 ^ _219113) ^ [_222351] ^ [] : [-(p5) : -([_222351]), p5 : [_222351, 96 ^ [_222351]]], (100 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (106 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (112 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (120 ^ _219113) ^ [_223210, _223212] ^ [] : [-(p1) : -([_223212, _223210]), p1 : [_223212, _223210, 123 ^ [_223210, _223212]]], (129 ^ _219113) ^ [_223559, _223561] ^ [] : [-(p1) : -([_223561, _223559]), p3 : [_223561, _223559, 132 ^ [_223559, _223561]]], (138 ^ _219113) ^ [_223908, _223910] ^ [] : [-(p1) : -([_223910, _223908]), p6 : [_223910, _223908, 141 ^ [_223908, _223910]]], (147 ^ _219113) ^ [_224257, _224259] ^ [] : [-(p1) : -([_224259, _224257]), p5 : [_224259, _224257, 150 ^ [_224257, _224259]]], (154 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (160 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (167 ^ _219113) ^ [_224937] ^ [] : [-(p4) : -([_224937]), p2 : [_224937, 170 ^ [_224937]]], (175 ^ _219113) ^ [_225247] ^ [] : [-(p6) : -([_225247]), p2 : [_225247, 178 ^ [_225247]]], (184 ^ _219113) ^ [_225578, _225580] ^ [] : [-(p3) : -([_225580, _225578]), p1 : [_225580, _225578, 187 ^ [_225578, _225580]]], (193 ^ _219113) ^ [_225927, _225929] ^ [] : [-(p3) : -([_225929, _225927]), p3 : [_225929, _225927, 196 ^ [_225927, _225929]]], (202 ^ _219113) ^ [_226276, _226278] ^ [] : [-(p3) : -([_226278, _226276]), p5 : [_226278, _226276, 205 ^ [_226276, _226278]]], (209 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (215 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (222 ^ _219113) ^ [_226956] ^ [] : [-(p4) : -([_226956]), p4 : [_226956, 225 ^ [_226956]]], (230 ^ _219113) ^ [_227266] ^ [] : [-(p6) : -([_227266]), p4 : [_227266, 233 ^ [_227266]]], (239 ^ _219113) ^ [_227597, _227599] ^ [] : [-(p5) : -([_227599, _227597]), p1 : [_227599, _227597, 242 ^ [_227597, _227599]]], (248 ^ _219113) ^ [_227946, _227948] ^ [] : [-(p5) : -([_227948, _227946]), p3 : [_227948, _227946, 251 ^ [_227946, _227948]]], (257 ^ _219113) ^ [_228295, _228297] ^ [] : [-(p5) : -([_228297, _228295]), p5 : [_228297, _228295, 260 ^ [_228295, _228297]]], (264 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (270 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (277 ^ _219113) ^ [_228975] ^ [] : [-(p4) : -([_228975]), p6 : [_228975, 280 ^ [_228975]]], (285 ^ _219113) ^ [_229285] ^ [] : [-(p6) : -([_229285]), p6 : [_229285, 288 ^ [_229285]]], (295 ^ _219113) ^ [_229639, _229641, _229643] ^ [] : [-(p1) : -([_229643, _229641, _229639]), p1 : [_229643, _229641, _229639, 298 ^ [_229639, _229641, _229643]]], (305 ^ _219113) ^ [_230029, _230031, _230033] ^ [] : [-(p1) : -([_230033, _230031, _230029]), p3 : [_230033, _230031, _230029, 308 ^ [_230029, _230031, _230033]]], (312 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (318 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (326 ^ _219113) ^ [_230748, _230750] ^ [] : [-(p2) : -([_230750, _230748]), p2 : [_230750, _230748, 329 ^ [_230748, _230750]]], (335 ^ _219113) ^ [_231097, _231099] ^ [] : [-(p4) : -([_231099, _231097]), p2 : [_231099, _231097, 338 ^ [_231097, _231099]]], (344 ^ _219113) ^ [_231446, _231448] ^ [] : [-(p6) : -([_231448, _231446]), p2 : [_231448, _231446, 347 ^ [_231446, _231448]]], (354 ^ _219113) ^ [_231818, _231820, _231822] ^ [] : [-(p3) : -([_231822, _231820, _231818]), p1 : [_231822, _231820, _231818, 357 ^ [_231818, _231820, _231822]]], (364 ^ _219113) ^ [_232208, _232210, _232212] ^ [] : [-(p3) : -([_232212, _232210, _232208]), p3 : [_232212, _232210, _232208, 367 ^ [_232208, _232210, _232212]]], (371 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (377 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (385 ^ _219113) ^ [_232927, _232929] ^ [] : [-(p2) : -([_232929, _232927]), p4 : [_232929, _232927, 388 ^ [_232927, _232929]]], (394 ^ _219113) ^ [_233276, _233278] ^ [] : [-(p4) : -([_233278, _233276]), p4 : [_233278, _233276, 397 ^ [_233276, _233278]]], (403 ^ _219113) ^ [_233625, _233627] ^ [] : [-(p6) : -([_233627, _233625]), p4 : [_233627, _233625, 406 ^ [_233625, _233627]]], (413 ^ _219113) ^ [_233997, _233999, _234001] ^ [] : [-(p5) : -([_234001, _233999, _233997]), p1 : [_234001, _233999, _233997, 416 ^ [_233997, _233999, _234001]]], (423 ^ _219113) ^ [_234387, _234389, _234391] ^ [] : [-(p5) : -([_234391, _234389, _234387]), p3 : [_234391, _234389, _234387, 426 ^ [_234387, _234389, _234391]]], (430 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (439 ^ _219113) ^ [_234953, _234955, _234957] ^ [] : [-(p6) : -([_234957, _234955, _234953]), p5 : [_234957, _234955, _234953, 442 ^ [_234953, _234955, _234957]]], (448 ^ _219113) ^ [_235320, _235322] ^ [] : [-(p2) : -([_235322, _235320]), p6 : [_235322, _235320, 451 ^ [_235320, _235322]]], (457 ^ _219113) ^ [_235669, _235671] ^ [] : [-(p4) : -([_235671, _235669]), p6 : [_235671, _235669, 460 ^ [_235669, _235671]]], (466 ^ _219113) ^ [_236018, _236020] ^ [] : [-(p6) : -([_236020, _236018]), p6 : [_236020, _236018, 469 ^ [_236018, _236020]]], (477 ^ _219113) ^ [_236415, _236417, _236419, _236421] ^ [] : [-(p1) : -([_236421, _236419, _236417, _236415]), p1 : [_236421, _236419, _236417, _236415, 480 ^ [_236415, _236417, _236419, _236421]]], (488 ^ _219113) ^ [_236848, _236850, _236852, _236854] ^ [] : [-(p1) : -([_236854, _236852, _236850, _236848]), p3 : [_236854, _236852, _236850, _236848, 491 ^ [_236848, _236850, _236852, _236854]]], (499 ^ _219113) ^ [_237281, _237283, _237285, _237287] ^ [] : [-(p1) : -([_237287, _237285, _237283, _237281]), p5 : [_237287, _237285, _237283, _237281, 502 ^ [_237281, _237283, _237285, _237287]]], (506 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (512 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (521 ^ _219113) ^ [_238041, _238043, _238045] ^ [] : [-(p2) : -([_238045, _238043, _238041]), p2 : [_238045, _238043, _238041, 524 ^ [_238041, _238043, _238045]]], (531 ^ _219113) ^ [_238431, _238433, _238435] ^ [] : [-(p4) : -([_238435, _238433, _238431]), p2 : [_238435, _238433, _238431, 534 ^ [_238431, _238433, _238435]]], (542 ^ _219113) ^ [_238846, _238848, _238850, _238852] ^ [] : [-(p3) : -([_238852, _238850, _238848, _238846]), p1 : [_238852, _238850, _238848, _238846, 545 ^ [_238846, _238848, _238850, _238852]]], (553 ^ _219113) ^ [_239279, _239281, _239283, _239285] ^ [] : [-(p3) : -([_239285, _239283, _239281, _239279]), p3 : [_239285, _239283, _239281, _239279, 556 ^ [_239279, _239281, _239283, _239285]]], (564 ^ _219113) ^ [_239712, _239714, _239716, _239718] ^ [] : [-(p3) : -([_239718, _239716, _239714, _239712]), p5 : [_239718, _239716, _239714, _239712, 567 ^ [_239712, _239714, _239716, _239718]]], (571 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (577 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (586 ^ _219113) ^ [_240472, _240474, _240476] ^ [] : [-(p2) : -([_240476, _240474, _240472]), p4 : [_240476, _240474, _240472, 589 ^ [_240472, _240474, _240476]]], (596 ^ _219113) ^ [_240862, _240864, _240866] ^ [] : [-(p4) : -([_240866, _240864, _240862]), p4 : [_240866, _240864, _240862, 599 ^ [_240862, _240864, _240866]]], (607 ^ _219113) ^ [_241277, _241279, _241281, _241283] ^ [] : [-(p5) : -([_241283, _241281, _241279, _241277]), p1 : [_241283, _241281, _241279, _241277, 610 ^ [_241277, _241279, _241281, _241283]]], (618 ^ _219113) ^ [_241710, _241712, _241714, _241716] ^ [] : [-(p5) : -([_241716, _241714, _241712, _241710]), p3 : [_241716, _241714, _241712, _241710, 621 ^ [_241710, _241712, _241714, _241716]]], (629 ^ _219113) ^ [_242143, _242145, _242147, _242149] ^ [] : [-(p5) : -([_242149, _242147, _242145, _242143]), p4 : [_242149, _242147, _242145, _242143, 632 ^ [_242143, _242145, _242147, _242149]]], (640 ^ _219113) ^ [_242576, _242578, _242580, _242582] ^ [] : [-(p5) : -([_242582, _242580, _242578, _242576]), p5 : [_242582, _242580, _242578, _242576, 643 ^ [_242576, _242578, _242580, _242582]]], (647 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (653 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (662 ^ _219113) ^ [_243336, _243338, _243340] ^ [] : [-(p2) : -([_243340, _243338, _243336]), p6 : [_243340, _243338, _243336, 665 ^ [_243336, _243338, _243340]]], (672 ^ _219113) ^ [_243726, _243728, _243730] ^ [] : [-(p4) : -([_243730, _243728, _243726]), p6 : [_243730, _243728, _243726, 675 ^ [_243726, _243728, _243730]]], (684 ^ _219113) ^ [_244168, _244170, _244172, _244174, _244176] ^ [] : [-(p1) : -([_244176, _244174, _244172, _244170, _244168]), p3 : [_244176, _244174, _244172, _244170, _244168, 687 ^ [_244168, _244170, _244172, _244174, _244176]]], (696 ^ _219113) ^ [_244646, _244648, _244650, _244652, _244654] ^ [] : [-(p1) : -([_244654, _244652, _244650, _244648, _244646]), p5 : [_244654, _244652, _244650, _244648, _244646, 699 ^ [_244646, _244648, _244650, _244652, _244654]]], (703 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (709 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (719 ^ _219113) ^ [_245449, _245451, _245453, _245455] ^ [] : [-(p2) : -([_245455, _245453, _245451, _245449]), p2 : [_245455, _245453, _245451, _245449, 722 ^ [_245449, _245451, _245453, _245455]]], (730 ^ _219113) ^ [_245882, _245884, _245886, _245888] ^ [] : [-(p4) : -([_245888, _245886, _245884, _245882]), p2 : [_245888, _245886, _245884, _245882, 733 ^ [_245882, _245884, _245886, _245888]]], (741 ^ _219113) ^ [_246315, _246317, _246319, _246321] ^ [] : [-(p6) : -([_246321, _246319, _246317, _246315]), p2 : [_246321, _246319, _246317, _246315, 744 ^ [_246315, _246317, _246319, _246321]]], (753 ^ _219113) ^ [_246775, _246777, _246779, _246781, _246783] ^ [] : [-(p3) : -([_246783, _246781, _246779, _246777, _246775]), p3 : [_246783, _246781, _246779, _246777, _246775, 756 ^ [_246775, _246777, _246779, _246781, _246783]]], (765 ^ _219113) ^ [_247253, _247255, _247257, _247259, _247261] ^ [] : [-(p3) : -([_247261, _247259, _247257, _247255, _247253]), p5 : [_247261, _247259, _247257, _247255, _247253, 768 ^ [_247253, _247255, _247257, _247259, _247261]]], (772 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (778 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (788 ^ _219113) ^ [_248056, _248058, _248060, _248062] ^ [] : [-(p2) : -([_248062, _248060, _248058, _248056]), p4 : [_248062, _248060, _248058, _248056, 791 ^ [_248056, _248058, _248060, _248062]]], (799 ^ _219113) ^ [_248489, _248491, _248493, _248495] ^ [] : [-(p4) : -([_248495, _248493, _248491, _248489]), p4 : [_248495, _248493, _248491, _248489, 802 ^ [_248489, _248491, _248493, _248495]]], (810 ^ _219113) ^ [_248922, _248924, _248926, _248928] ^ [] : [-(p6) : -([_248928, _248926, _248924, _248922]), p4 : [_248928, _248926, _248924, _248922, 813 ^ [_248922, _248924, _248926, _248928]]], (822 ^ _219113) ^ [_249382, _249384, _249386, _249388, _249390] ^ [] : [-(p5) : -([_249390, _249388, _249386, _249384, _249382]), p3 : [_249390, _249388, _249386, _249384, _249382, 825 ^ [_249382, _249384, _249386, _249388, _249390]]], (834 ^ _219113) ^ [_249860, _249862, _249864, _249866, _249868] ^ [] : [-(p5) : -([_249868, _249866, _249864, _249862, _249860]), p5 : [_249868, _249866, _249864, _249862, _249860, 837 ^ [_249860, _249862, _249864, _249866, _249868]]], (841 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (847 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (857 ^ _219113) ^ [_250663, _250665, _250667, _250669] ^ [] : [-(p2) : -([_250669, _250667, _250665, _250663]), p6 : [_250669, _250667, _250665, _250663, 860 ^ [_250663, _250665, _250667, _250669]]], (868 ^ _219113) ^ [_251096, _251098, _251100, _251102] ^ [] : [-(p4) : -([_251102, _251100, _251098, _251096]), p6 : [_251102, _251100, _251098, _251096, 871 ^ [_251096, _251098, _251100, _251102]]], (879 ^ _219113) ^ [_251529, _251531, _251533, _251535] ^ [] : [-(p6) : -([_251535, _251533, _251531, _251529]), p6 : [_251535, _251533, _251531, _251529, 882 ^ [_251529, _251531, _251533, _251535]]], (892 ^ _219113) ^ [_252018, _252020, _252022, _252024, _252026, _252028] ^ [] : [-(p1) : -([_252028, _252026, _252024, _252022, _252020, _252018]), p1 : [_252028, _252026, _252024, _252022, _252020, _252018, 895 ^ [_252018, _252020, _252022, _252024, _252026, _252028]]], (905 ^ _219113) ^ [_252543, _252545, _252547, _252549, _252551, _252553] ^ [] : [-(p1) : -([_252553, _252551, _252549, _252547, _252545, _252543]), p3 : [_252553, _252551, _252549, _252547, _252545, _252543, 908 ^ [_252543, _252545, _252547, _252549, _252551, _252553]]], (918 ^ _219113) ^ [_253068, _253070, _253072, _253074, _253076, _253078] ^ [] : [-(p1) : -([_253078, _253076, _253074, _253072, _253070, _253068]), p4 : [_253078, _253076, _253074, _253072, _253070, _253068, 921 ^ [_253068, _253070, _253072, _253074, _253076, _253078]]], (931 ^ _219113) ^ [_253593, _253595, _253597, _253599, _253601, _253603] ^ [] : [-(p1) : -([_253603, _253601, _253599, _253597, _253595, _253593]), p5 : [_253603, _253601, _253599, _253597, _253595, _253593, 934 ^ [_253593, _253595, _253597, _253599, _253601, _253603]]], (938 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (944 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (955 ^ _219113) ^ [_254441, _254443, _254445, _254447, _254449] ^ [] : [-(p2) : -([_254449, _254447, _254445, _254443, _254441]), p2 : [_254449, _254447, _254445, _254443, _254441, 958 ^ [_254441, _254443, _254445, _254447, _254449]]], (967 ^ _219113) ^ [_254919, _254921, _254923, _254925, _254927] ^ [] : [-(p6) : -([_254927, _254925, _254923, _254921, _254919]), p2 : [_254927, _254925, _254923, _254921, _254919, 970 ^ [_254919, _254921, _254923, _254925, _254927]]], (980 ^ _219113) ^ [_255426, _255428, _255430, _255432, _255434, _255436] ^ [] : [-(p3) : -([_255436, _255434, _255432, _255430, _255428, _255426]), p1 : [_255436, _255434, _255432, _255430, _255428, _255426, 983 ^ [_255426, _255428, _255430, _255432, _255434, _255436]]], (993 ^ _219113) ^ [_255951, _255953, _255955, _255957, _255959, _255961] ^ [] : [-(p3) : -([_255961, _255959, _255957, _255955, _255953, _255951]), p3 : [_255961, _255959, _255957, _255955, _255953, _255951, 996 ^ [_255951, _255953, _255955, _255957, _255959, _255961]]], (1006 ^ _219113) ^ [_256476, _256478, _256480, _256482, _256484, _256486] ^ [] : [-(p3) : -([_256486, _256484, _256482, _256480, _256478, _256476]), p5 : [_256486, _256484, _256482, _256480, _256478, _256476, 1009 ^ [_256476, _256478, _256480, _256482, _256484, _256486]]], (1013 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1019 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1030 ^ _219113) ^ [_257324, _257326, _257328, _257330, _257332] ^ [] : [-(p2) : -([_257332, _257330, _257328, _257326, _257324]), p4 : [_257332, _257330, _257328, _257326, _257324, 1033 ^ [_257324, _257326, _257328, _257330, _257332]]], (1042 ^ _219113) ^ [_257802, _257804, _257806, _257808, _257810] ^ [] : [-(p6) : -([_257810, _257808, _257806, _257804, _257802]), p4 : [_257810, _257808, _257806, _257804, _257802, 1045 ^ [_257802, _257804, _257806, _257808, _257810]]], (1055 ^ _219113) ^ [_258309, _258311, _258313, _258315, _258317, _258319] ^ [] : [-(p5) : -([_258319, _258317, _258315, _258313, _258311, _258309]), p1 : [_258319, _258317, _258315, _258313, _258311, _258309, 1058 ^ [_258309, _258311, _258313, _258315, _258317, _258319]]], (1068 ^ _219113) ^ [_258834, _258836, _258838, _258840, _258842, _258844] ^ [] : [-(p5) : -([_258844, _258842, _258840, _258838, _258836, _258834]), p3 : [_258844, _258842, _258840, _258838, _258836, _258834, 1071 ^ [_258834, _258836, _258838, _258840, _258842, _258844]]], (1081 ^ _219113) ^ [_259359, _259361, _259363, _259365, _259367, _259369] ^ [] : [-(p5) : -([_259369, _259367, _259365, _259363, _259361, _259359]), p5 : [_259369, _259367, _259365, _259363, _259361, _259359, 1084 ^ [_259359, _259361, _259363, _259365, _259367, _259369]]], (1088 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1094 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1105 ^ _219113) ^ [_260207, _260209, _260211, _260213, _260215] ^ [] : [-(p2) : -([_260215, _260213, _260211, _260209, _260207]), p6 : [_260215, _260213, _260211, _260209, _260207, 1108 ^ [_260207, _260209, _260211, _260213, _260215]]], (1117 ^ _219113) ^ [_260685, _260687, _260689, _260691, _260693] ^ [] : [-(p6) : -([_260693, _260691, _260689, _260687, _260685]), p6 : [_260693, _260691, _260689, _260687, _260685, 1120 ^ [_260685, _260687, _260689, _260691, _260693]]], (1131 ^ _219113) ^ [_261223, _261225, _261227, _261229, _261231, _261233, _261235] ^ [] : [-(p1) : -([_261235, _261233, _261231, _261229, _261227, _261225, _261223]), p3 : [_261235, _261233, _261231, _261229, _261227, _261225, _261223, 1134 ^ [_261223, _261225, _261227, _261229, _261231, _261233, _261235]]], (1145 ^ _219113) ^ [_261797, _261799, _261801, _261803, _261805, _261807, _261809] ^ [] : [-(p1) : -([_261809, _261807, _261805, _261803, _261801, _261799, _261797]), p5 : [_261809, _261807, _261805, _261803, _261801, _261799, _261797, 1148 ^ [_261797, _261799, _261801, _261803, _261805, _261807, _261809]]], (1152 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1158 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1170 ^ _219113) ^ [_262692, _262694, _262696, _262698, _262700, _262702] ^ [] : [-(p2) : -([_262702, _262700, _262698, _262696, _262694, _262692]), p2 : [_262702, _262700, _262698, _262696, _262694, _262692, 1173 ^ [_262692, _262694, _262696, _262698, _262700, _262702]]], (1183 ^ _219113) ^ [_263217, _263219, _263221, _263223, _263225, _263227] ^ [] : [-(p4) : -([_263227, _263225, _263223, _263221, _263219, _263217]), p2 : [_263227, _263225, _263223, _263221, _263219, _263217, 1186 ^ [_263217, _263219, _263221, _263223, _263225, _263227]]], (1196 ^ _219113) ^ [_263742, _263744, _263746, _263748, _263750, _263752] ^ [] : [-(p6) : -([_263752, _263750, _263748, _263746, _263744, _263742]), p2 : [_263752, _263750, _263748, _263746, _263744, _263742, 1199 ^ [_263742, _263744, _263746, _263748, _263750, _263752]]], (1210 ^ _219113) ^ [_264298, _264300, _264302, _264304, _264306, _264308, _264310] ^ [] : [-(p3) : -([_264310, _264308, _264306, _264304, _264302, _264300, _264298]), p3 : [_264310, _264308, _264306, _264304, _264302, _264300, _264298, 1213 ^ [_264298, _264300, _264302, _264304, _264306, _264308, _264310]]], (1224 ^ _219113) ^ [_264872, _264874, _264876, _264878, _264880, _264882, _264884] ^ [] : [-(p3) : -([_264884, _264882, _264880, _264878, _264876, _264874, _264872]), p5 : [_264884, _264882, _264880, _264878, _264876, _264874, _264872, 1227 ^ [_264872, _264874, _264876, _264878, _264880, _264882, _264884]]], (1231 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1244 ^ _219113) ^ [_265622, _265624, _265626, _265628, _265630, _265632, _265634] ^ [] : [-(p4) : -([_265634, _265632, _265630, _265628, _265626, _265624, _265622]), p1 : [_265634, _265632, _265630, _265628, _265626, _265624, _265622, 1247 ^ [_265622, _265624, _265626, _265628, _265630, _265632, _265634]]], (1257 ^ _219113) ^ [_266165, _266167, _266169, _266171, _266173, _266175] ^ [] : [-(p2) : -([_266175, _266173, _266171, _266169, _266167, _266165]), p4 : [_266175, _266173, _266171, _266169, _266167, _266165, 1260 ^ [_266165, _266167, _266169, _266171, _266173, _266175]]], (1270 ^ _219113) ^ [_266690, _266692, _266694, _266696, _266698, _266700] ^ [] : [-(p4) : -([_266700, _266698, _266696, _266694, _266692, _266690]), p4 : [_266700, _266698, _266696, _266694, _266692, _266690, 1273 ^ [_266690, _266692, _266694, _266696, _266698, _266700]]], (1283 ^ _219113) ^ [_267215, _267217, _267219, _267221, _267223, _267225] ^ [] : [-(p6) : -([_267225, _267223, _267221, _267219, _267217, _267215]), p4 : [_267225, _267223, _267221, _267219, _267217, _267215, 1286 ^ [_267215, _267217, _267219, _267221, _267223, _267225]]], (1297 ^ _219113) ^ [_267771, _267773, _267775, _267777, _267779, _267781, _267783] ^ [] : [-(p5) : -([_267783, _267781, _267779, _267777, _267775, _267773, _267771]), p3 : [_267783, _267781, _267779, _267777, _267775, _267773, _267771, 1300 ^ [_267771, _267773, _267775, _267777, _267779, _267781, _267783]]], (1311 ^ _219113) ^ [_268345, _268347, _268349, _268351, _268353, _268355, _268357] ^ [] : [-(p5) : -([_268357, _268355, _268353, _268351, _268349, _268347, _268345]), p5 : [_268357, _268355, _268353, _268351, _268349, _268347, _268345, 1314 ^ [_268345, _268347, _268349, _268351, _268353, _268355, _268357]]], (1318 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1324 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1336 ^ _219113) ^ [_269240, _269242, _269244, _269246, _269248, _269250] ^ [] : [-(p2) : -([_269250, _269248, _269246, _269244, _269242, _269240]), p6 : [_269250, _269248, _269246, _269244, _269242, _269240, 1339 ^ [_269240, _269242, _269244, _269246, _269248, _269250]]], (1349 ^ _219113) ^ [_269765, _269767, _269769, _269771, _269773, _269775] ^ [] : [-(p4) : -([_269775, _269773, _269771, _269769, _269767, _269765]), p6 : [_269775, _269773, _269771, _269769, _269767, _269765, 1352 ^ [_269765, _269767, _269769, _269771, _269773, _269775]]], (1362 ^ _219113) ^ [_270290, _270292, _270294, _270296, _270298, _270300] ^ [] : [-(p6) : -([_270300, _270298, _270296, _270294, _270292, _270290]), p6 : [_270300, _270298, _270296, _270294, _270292, _270290, 1365 ^ [_270290, _270292, _270294, _270296, _270298, _270300]]], (1377 ^ _219113) ^ [_270879, _270881, _270883, _270885, _270887, _270889, _270891, _270893] ^ [] : [-(p1) : -([_270893, _270891, _270889, _270887, _270885, _270883, _270881, _270879]), p1 : [_270893, _270891, _270889, _270887, _270885, _270883, _270881, _270879, 1380 ^ [_270879, _270881, _270883, _270885, _270887, _270889, _270891, _270893]]], (1392 ^ _219113) ^ [_271504, _271506, _271508, _271510, _271512, _271514, _271516, _271518] ^ [] : [-(p1) : -([_271518, _271516, _271514, _271512, _271510, _271508, _271506, _271504]), p3 : [_271518, _271516, _271514, _271512, _271510, _271508, _271506, _271504, 1395 ^ [_271504, _271506, _271508, _271510, _271512, _271514, _271516, _271518]]], (1407 ^ _219113) ^ [_272129, _272131, _272133, _272135, _272137, _272139, _272141, _272143] ^ [] : [-(p1) : -([_272143, _272141, _272139, _272137, _272135, _272133, _272131, _272129]), p4 : [_272143, _272141, _272139, _272137, _272135, _272133, _272131, _272129, 1410 ^ [_272129, _272131, _272133, _272135, _272137, _272139, _272141, _272143]]], (1422 ^ _219113) ^ [_272754, _272756, _272758, _272760, _272762, _272764, _272766, _272768] ^ [] : [-(p1) : -([_272768, _272766, _272764, _272762, _272760, _272758, _272756, _272754]), p5 : [_272768, _272766, _272764, _272762, _272760, _272758, _272756, _272754, 1425 ^ [_272754, _272756, _272758, _272760, _272762, _272764, _272766, _272768]]], (1429 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1435 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1448 ^ _219113) ^ [_273698, _273700, _273702, _273704, _273706, _273708, _273710] ^ [] : [-(p2) : -([_273710, _273708, _273706, _273704, _273702, _273700, _273698]), p2 : [_273710, _273708, _273706, _273704, _273702, _273700, _273698, 1451 ^ [_273698, _273700, _273702, _273704, _273706, _273708, _273710]]], (1462 ^ _219113) ^ [_274272, _274274, _274276, _274278, _274280, _274282, _274284] ^ [] : [-(p6) : -([_274284, _274282, _274280, _274278, _274276, _274274, _274272]), p2 : [_274284, _274282, _274280, _274278, _274276, _274274, _274272, 1465 ^ [_274272, _274274, _274276, _274278, _274280, _274282, _274284]]], (1477 ^ _219113) ^ [_274879, _274881, _274883, _274885, _274887, _274889, _274891, _274893] ^ [] : [-(p3) : -([_274893, _274891, _274889, _274887, _274885, _274883, _274881, _274879]), p1 : [_274893, _274891, _274889, _274887, _274885, _274883, _274881, _274879, 1480 ^ [_274879, _274881, _274883, _274885, _274887, _274889, _274891, _274893]]], (1492 ^ _219113) ^ [_275504, _275506, _275508, _275510, _275512, _275514, _275516, _275518] ^ [] : [-(p3) : -([_275518, _275516, _275514, _275512, _275510, _275508, _275506, _275504]), p3 : [_275518, _275516, _275514, _275512, _275510, _275508, _275506, _275504, 1495 ^ [_275504, _275506, _275508, _275510, _275512, _275514, _275516, _275518]]], (1507 ^ _219113) ^ [_276129, _276131, _276133, _276135, _276137, _276139, _276141, _276143] ^ [] : [-(p3) : -([_276143, _276141, _276139, _276137, _276135, _276133, _276131, _276129]), p5 : [_276143, _276141, _276139, _276137, _276135, _276133, _276131, _276129, 1510 ^ [_276129, _276131, _276133, _276135, _276137, _276139, _276141, _276143]]], (1514 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1520 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1533 ^ _219113) ^ [_277073, _277075, _277077, _277079, _277081, _277083, _277085] ^ [] : [-(p2) : -([_277085, _277083, _277081, _277079, _277077, _277075, _277073]), p4 : [_277085, _277083, _277081, _277079, _277077, _277075, _277073, 1536 ^ [_277073, _277075, _277077, _277079, _277081, _277083, _277085]]], (1547 ^ _219113) ^ [_277647, _277649, _277651, _277653, _277655, _277657, _277659] ^ [] : [-(p6) : -([_277659, _277657, _277655, _277653, _277651, _277649, _277647]), p4 : [_277659, _277657, _277655, _277653, _277651, _277649, _277647, 1550 ^ [_277647, _277649, _277651, _277653, _277655, _277657, _277659]]], (1562 ^ _219113) ^ [_278254, _278256, _278258, _278260, _278262, _278264, _278266, _278268] ^ [] : [-(p5) : -([_278268, _278266, _278264, _278262, _278260, _278258, _278256, _278254]), p1 : [_278268, _278266, _278264, _278262, _278260, _278258, _278256, _278254, 1565 ^ [_278254, _278256, _278258, _278260, _278262, _278264, _278266, _278268]]], (1577 ^ _219113) ^ [_278879, _278881, _278883, _278885, _278887, _278889, _278891, _278893] ^ [] : [-(p5) : -([_278893, _278891, _278889, _278887, _278885, _278883, _278881, _278879]), p3 : [_278893, _278891, _278889, _278887, _278885, _278883, _278881, _278879, 1580 ^ [_278879, _278881, _278883, _278885, _278887, _278889, _278891, _278893]]], (1592 ^ _219113) ^ [_279504, _279506, _279508, _279510, _279512, _279514, _279516, _279518] ^ [] : [-(p5) : -([_279518, _279516, _279514, _279512, _279510, _279508, _279506, _279504]), p5 : [_279518, _279516, _279514, _279512, _279510, _279508, _279506, _279504, 1595 ^ [_279504, _279506, _279508, _279510, _279512, _279514, _279516, _279518]]], (1599 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1605 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1618 ^ _219113) ^ [_280448, _280450, _280452, _280454, _280456, _280458, _280460] ^ [] : [-(p2) : -([_280460, _280458, _280456, _280454, _280452, _280450, _280448]), p6 : [_280460, _280458, _280456, _280454, _280452, _280450, _280448, 1621 ^ [_280448, _280450, _280452, _280454, _280456, _280458, _280460]]], (1632 ^ _219113) ^ [_281022, _281024, _281026, _281028, _281030, _281032, _281034] ^ [] : [-(p6) : -([_281034, _281032, _281030, _281028, _281026, _281024, _281022]), p6 : [_281034, _281032, _281030, _281028, _281026, _281024, _281022, 1635 ^ [_281022, _281024, _281026, _281028, _281030, _281032, _281034]]], (1648 ^ _219113) ^ [_281664, _281666, _281668, _281670, _281672, _281674, _281676, _281678, _281680] ^ [] : [-(p1) : -([_281680, _281678, _281676, _281674, _281672, _281670, _281668, _281666, _281664]), p3 : [_281680, _281678, _281676, _281674, _281672, _281670, _281668, _281666, _281664, 1651 ^ [_281664, _281666, _281668, _281670, _281672, _281674, _281676, _281678, _281680]]], (1664 ^ _219113) ^ [_282342, _282344, _282346, _282348, _282350, _282352, _282354, _282356, _282358] ^ [] : [-(p1) : -([_282358, _282356, _282354, _282352, _282350, _282348, _282346, _282344, _282342]), p5 : [_282358, _282356, _282354, _282352, _282350, _282348, _282346, _282344, _282342, 1667 ^ [_282342, _282344, _282346, _282348, _282350, _282352, _282354, _282356, _282358]]], (1671 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1677 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1691 ^ _219113) ^ [_283337, _283339, _283341, _283343, _283345, _283347, _283349, _283351] ^ [] : [-(p2) : -([_283351, _283349, _283347, _283345, _283343, _283341, _283339, _283337]), p2 : [_283351, _283349, _283347, _283345, _283343, _283341, _283339, _283337, 1694 ^ [_283337, _283339, _283341, _283343, _283345, _283347, _283349, _283351]]], (1706 ^ _219113) ^ [_283962, _283964, _283966, _283968, _283970, _283972, _283974, _283976] ^ [] : [-(p4) : -([_283976, _283974, _283972, _283970, _283968, _283966, _283964, _283962]), p2 : [_283976, _283974, _283972, _283970, _283968, _283966, _283964, _283962, 1709 ^ [_283962, _283964, _283966, _283968, _283970, _283972, _283974, _283976]]], (1721 ^ _219113) ^ [_284587, _284589, _284591, _284593, _284595, _284597, _284599, _284601] ^ [] : [-(p6) : -([_284601, _284599, _284597, _284595, _284593, _284591, _284589, _284587]), p2 : [_284601, _284599, _284597, _284595, _284593, _284591, _284589, _284587, 1724 ^ [_284587, _284589, _284591, _284593, _284595, _284597, _284599, _284601]]], (1737 ^ _219113) ^ [_285247, _285249, _285251, _285253, _285255, _285257, _285259, _285261, _285263] ^ [] : [-(p3) : -([_285263, _285261, _285259, _285257, _285255, _285253, _285251, _285249, _285247]), p3 : [_285263, _285261, _285259, _285257, _285255, _285253, _285251, _285249, _285247, 1740 ^ [_285247, _285249, _285251, _285253, _285255, _285257, _285259, _285261, _285263]]], (1753 ^ _219113) ^ [_285925, _285927, _285929, _285931, _285933, _285935, _285937, _285939, _285941] ^ [] : [-(p3) : -([_285941, _285939, _285937, _285935, _285933, _285931, _285929, _285927, _285925]), p5 : [_285941, _285939, _285937, _285935, _285933, _285931, _285929, _285927, _285925, 1756 ^ [_285925, _285927, _285929, _285931, _285933, _285935, _285937, _285939, _285941]]], (1760 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1775 ^ _219113) ^ [_286779, _286781, _286783, _286785, _286787, _286789, _286791, _286793, _286795] ^ [] : [-(p4) : -([_286795, _286793, _286791, _286789, _286787, _286785, _286783, _286781, _286779]), p1 : [_286795, _286793, _286791, _286789, _286787, _286785, _286783, _286781, _286779, 1778 ^ [_286779, _286781, _286783, _286785, _286787, _286789, _286791, _286793, _286795]]], (1790 ^ _219113) ^ [_287422, _287424, _287426, _287428, _287430, _287432, _287434, _287436] ^ [] : [-(p2) : -([_287436, _287434, _287432, _287430, _287428, _287426, _287424, _287422]), p4 : [_287436, _287434, _287432, _287430, _287428, _287426, _287424, _287422, 1793 ^ [_287422, _287424, _287426, _287428, _287430, _287432, _287434, _287436]]], (1805 ^ _219113) ^ [_288047, _288049, _288051, _288053, _288055, _288057, _288059, _288061] ^ [] : [-(p4) : -([_288061, _288059, _288057, _288055, _288053, _288051, _288049, _288047]), p4 : [_288061, _288059, _288057, _288055, _288053, _288051, _288049, _288047, 1808 ^ [_288047, _288049, _288051, _288053, _288055, _288057, _288059, _288061]]], (1820 ^ _219113) ^ [_288672, _288674, _288676, _288678, _288680, _288682, _288684, _288686] ^ [] : [-(p6) : -([_288686, _288684, _288682, _288680, _288678, _288676, _288674, _288672]), p4 : [_288686, _288684, _288682, _288680, _288678, _288676, _288674, _288672, 1823 ^ [_288672, _288674, _288676, _288678, _288680, _288682, _288684, _288686]]], (1836 ^ _219113) ^ [_289332, _289334, _289336, _289338, _289340, _289342, _289344, _289346, _289348] ^ [] : [-(p5) : -([_289348, _289346, _289344, _289342, _289340, _289338, _289336, _289334, _289332]), p3 : [_289348, _289346, _289344, _289342, _289340, _289338, _289336, _289334, _289332, 1839 ^ [_289332, _289334, _289336, _289338, _289340, _289342, _289344, _289346, _289348]]], (1852 ^ _219113) ^ [_290010, _290012, _290014, _290016, _290018, _290020, _290022, _290024, _290026] ^ [] : [-(p5) : -([_290026, _290024, _290022, _290020, _290018, _290016, _290014, _290012, _290010]), p5 : [_290026, _290024, _290022, _290020, _290018, _290016, _290014, _290012, _290010, 1855 ^ [_290010, _290012, _290014, _290016, _290018, _290020, _290022, _290024, _290026]]], (1859 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1865 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1879 ^ _219113) ^ [_291005, _291007, _291009, _291011, _291013, _291015, _291017, _291019] ^ [] : [-(p2) : -([_291019, _291017, _291015, _291013, _291011, _291009, _291007, _291005]), p6 : [_291019, _291017, _291015, _291013, _291011, _291009, _291007, _291005, 1882 ^ [_291005, _291007, _291009, _291011, _291013, _291015, _291017, _291019]]], (1894 ^ _219113) ^ [_291630, _291632, _291634, _291636, _291638, _291640, _291642, _291644] ^ [] : [-(p4) : -([_291644, _291642, _291640, _291638, _291636, _291634, _291632, _291630]), p6 : [_291644, _291642, _291640, _291638, _291636, _291634, _291632, _291630, 1897 ^ [_291630, _291632, _291634, _291636, _291638, _291640, _291642, _291644]]], (1909 ^ _219113) ^ [_292255, _292257, _292259, _292261, _292263, _292265, _292267, _292269] ^ [] : [-(p6) : -([_292269, _292267, _292265, _292263, _292261, _292259, _292257, _292255]), p6 : [_292269, _292267, _292265, _292263, _292261, _292259, _292257, _292255, 1912 ^ [_292255, _292257, _292259, _292261, _292263, _292265, _292267, _292269]]], (1926 ^ _219113) ^ [_292952, _292954, _292956, _292958, _292960, _292962, _292964, _292966, _292968, _292970] ^ [] : [-(p1) : -([_292970, _292968, _292966, _292964, _292962, _292960, _292958, _292956, _292954, _292952]), p1 : [_292970, _292968, _292966, _292964, _292962, _292960, _292958, _292956, _292954, _292952, 1929 ^ [_292952, _292954, _292956, _292958, _292960, _292962, _292964, _292966, _292968, _292970]]], (1943 ^ _219113) ^ [_293685, _293687, _293689, _293691, _293693, _293695, _293697, _293699, _293701, _293703] ^ [] : [-(p1) : -([_293703, _293701, _293699, _293697, _293695, _293693, _293691, _293689, _293687, _293685]), p3 : [_293703, _293701, _293699, _293697, _293695, _293693, _293691, _293689, _293687, _293685, 1946 ^ [_293685, _293687, _293689, _293691, _293693, _293695, _293697, _293699, _293701, _293703]]], (1960 ^ _219113) ^ [_294418, _294420, _294422, _294424, _294426, _294428, _294430, _294432, _294434, _294436] ^ [] : [-(p1) : -([_294436, _294434, _294432, _294430, _294428, _294426, _294424, _294422, _294420, _294418]), p4 : [_294436, _294434, _294432, _294430, _294428, _294426, _294424, _294422, _294420, _294418, 1963 ^ [_294418, _294420, _294422, _294424, _294426, _294428, _294430, _294432, _294434, _294436]]], (1977 ^ _219113) ^ [_295151, _295153, _295155, _295157, _295159, _295161, _295163, _295165, _295167, _295169] ^ [] : [-(p1) : -([_295169, _295167, _295165, _295163, _295161, _295159, _295157, _295155, _295153, _295151]), p5 : [_295169, _295167, _295165, _295163, _295161, _295159, _295157, _295155, _295153, _295151, 1980 ^ [_295151, _295153, _295155, _295157, _295159, _295161, _295163, _295165, _295167, _295169]]], (1984 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (1990 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2005 ^ _219113) ^ [_296199, _296201, _296203, _296205, _296207, _296209, _296211, _296213, _296215] ^ [] : [-(p2) : -([_296215, _296213, _296211, _296209, _296207, _296205, _296203, _296201, _296199]), p2 : [_296215, _296213, _296211, _296209, _296207, _296205, _296203, _296201, _296199, 2008 ^ [_296199, _296201, _296203, _296205, _296207, _296209, _296211, _296213, _296215]]], (2021 ^ _219113) ^ [_296877, _296879, _296881, _296883, _296885, _296887, _296889, _296891, _296893] ^ [] : [-(p6) : -([_296893, _296891, _296889, _296887, _296885, _296883, _296881, _296879, _296877]), p2 : [_296893, _296891, _296889, _296887, _296885, _296883, _296881, _296879, _296877, 2024 ^ [_296877, _296879, _296881, _296883, _296885, _296887, _296889, _296891, _296893]]], (2038 ^ _219113) ^ [_297592, _297594, _297596, _297598, _297600, _297602, _297604, _297606, _297608, _297610] ^ [] : [-(p3) : -([_297610, _297608, _297606, _297604, _297602, _297600, _297598, _297596, _297594, _297592]), p1 : [_297610, _297608, _297606, _297604, _297602, _297600, _297598, _297596, _297594, _297592, 2041 ^ [_297592, _297594, _297596, _297598, _297600, _297602, _297604, _297606, _297608, _297610]]], (2055 ^ _219113) ^ [_298325, _298327, _298329, _298331, _298333, _298335, _298337, _298339, _298341, _298343] ^ [] : [-(p3) : -([_298343, _298341, _298339, _298337, _298335, _298333, _298331, _298329, _298327, _298325]), p3 : [_298343, _298341, _298339, _298337, _298335, _298333, _298331, _298329, _298327, _298325, 2058 ^ [_298325, _298327, _298329, _298331, _298333, _298335, _298337, _298339, _298341, _298343]]], (2072 ^ _219113) ^ [_299058, _299060, _299062, _299064, _299066, _299068, _299070, _299072, _299074, _299076] ^ [] : [-(p3) : -([_299076, _299074, _299072, _299070, _299068, _299066, _299064, _299062, _299060, _299058]), p5 : [_299076, _299074, _299072, _299070, _299068, _299066, _299064, _299062, _299060, _299058, 2075 ^ [_299058, _299060, _299062, _299064, _299066, _299068, _299070, _299072, _299074, _299076]]], (2079 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2085 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2100 ^ _219113) ^ [_300106, _300108, _300110, _300112, _300114, _300116, _300118, _300120, _300122] ^ [] : [-(p2) : -([_300122, _300120, _300118, _300116, _300114, _300112, _300110, _300108, _300106]), p4 : [_300122, _300120, _300118, _300116, _300114, _300112, _300110, _300108, _300106, 2103 ^ [_300106, _300108, _300110, _300112, _300114, _300116, _300118, _300120, _300122]]], (2116 ^ _219113) ^ [_300784, _300786, _300788, _300790, _300792, _300794, _300796, _300798, _300800] ^ [] : [-(p6) : -([_300800, _300798, _300796, _300794, _300792, _300790, _300788, _300786, _300784]), p4 : [_300800, _300798, _300796, _300794, _300792, _300790, _300788, _300786, _300784, 2119 ^ [_300784, _300786, _300788, _300790, _300792, _300794, _300796, _300798, _300800]]], (2133 ^ _219113) ^ [_301499, _301501, _301503, _301505, _301507, _301509, _301511, _301513, _301515, _301517] ^ [] : [-(p5) : -([_301517, _301515, _301513, _301511, _301509, _301507, _301505, _301503, _301501, _301499]), p1 : [_301517, _301515, _301513, _301511, _301509, _301507, _301505, _301503, _301501, _301499, 2136 ^ [_301499, _301501, _301503, _301505, _301507, _301509, _301511, _301513, _301515, _301517]]], (2150 ^ _219113) ^ [_302232, _302234, _302236, _302238, _302240, _302242, _302244, _302246, _302248, _302250] ^ [] : [-(p5) : -([_302250, _302248, _302246, _302244, _302242, _302240, _302238, _302236, _302234, _302232]), p3 : [_302250, _302248, _302246, _302244, _302242, _302240, _302238, _302236, _302234, _302232, 2153 ^ [_302232, _302234, _302236, _302238, _302240, _302242, _302244, _302246, _302248, _302250]]], (2167 ^ _219113) ^ [_302965, _302967, _302969, _302971, _302973, _302975, _302977, _302979, _302981, _302983] ^ [] : [-(p5) : -([_302983, _302981, _302979, _302977, _302975, _302973, _302971, _302969, _302967, _302965]), p5 : [_302983, _302981, _302979, _302977, _302975, _302973, _302971, _302969, _302967, _302965, 2170 ^ [_302965, _302967, _302969, _302971, _302973, _302975, _302977, _302979, _302981, _302983]]], (2174 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2180 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2195 ^ _219113) ^ [_304013, _304015, _304017, _304019, _304021, _304023, _304025, _304027, _304029] ^ [] : [-(p2) : -([_304029, _304027, _304025, _304023, _304021, _304019, _304017, _304015, _304013]), p6 : [_304029, _304027, _304025, _304023, _304021, _304019, _304017, _304015, _304013, 2198 ^ [_304013, _304015, _304017, _304019, _304021, _304023, _304025, _304027, _304029]]], (2211 ^ _219113) ^ [_304691, _304693, _304695, _304697, _304699, _304701, _304703, _304705, _304707] ^ [] : [-(p6) : -([_304707, _304705, _304703, _304701, _304699, _304697, _304695, _304693, _304691]), p6 : [_304707, _304705, _304703, _304701, _304699, _304697, _304695, _304693, _304691, 2214 ^ [_304691, _304693, _304695, _304697, _304699, _304701, _304703, _304705, _304707]]], (2218 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2224 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2230 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2246 ^ _219113) ^ [_305934, _305936, _305938, _305940, _305942, _305944, _305946, _305948, _305950, _305952] ^ [] : [-(p2) : -([_305952, _305950, _305948, _305946, _305944, _305942, _305940, _305938, _305936, _305934]), p2 : [_305952, _305950, _305948, _305946, _305944, _305942, _305940, _305938, _305936, _305934, 2249 ^ [_305934, _305936, _305938, _305940, _305942, _305944, _305946, _305948, _305950, _305952]]], (2263 ^ _219113) ^ [_306667, _306669, _306671, _306673, _306675, _306677, _306679, _306681, _306683, _306685] ^ [] : [-(p4) : -([_306685, _306683, _306681, _306679, _306677, _306675, _306673, _306671, _306669, _306667]), p2 : [_306685, _306683, _306681, _306679, _306677, _306675, _306673, _306671, _306669, _306667, 2266 ^ [_306667, _306669, _306671, _306673, _306675, _306677, _306679, _306681, _306683, _306685]]], (2280 ^ _219113) ^ [_307400, _307402, _307404, _307406, _307408, _307410, _307412, _307414, _307416, _307418] ^ [] : [-(p6) : -([_307418, _307416, _307414, _307412, _307410, _307408, _307406, _307404, _307402, _307400]), p2 : [_307418, _307416, _307414, _307412, _307410, _307408, _307406, _307404, _307402, _307400, 2283 ^ [_307400, _307402, _307404, _307406, _307408, _307410, _307412, _307414, _307416, _307418]]], (2287 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2293 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2299 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2315 ^ _219113) ^ [_308661, _308663, _308665, _308667, _308669, _308671, _308673, _308675, _308677, _308679] ^ [] : [-(p2) : -([_308679, _308677, _308675, _308673, _308671, _308669, _308667, _308665, _308663, _308661]), p4 : [_308679, _308677, _308675, _308673, _308671, _308669, _308667, _308665, _308663, _308661, 2318 ^ [_308661, _308663, _308665, _308667, _308669, _308671, _308673, _308675, _308677, _308679]]], (2332 ^ _219113) ^ [_309394, _309396, _309398, _309400, _309402, _309404, _309406, _309408, _309410, _309412] ^ [] : [-(p4) : -([_309412, _309410, _309408, _309406, _309404, _309402, _309400, _309398, _309396, _309394]), p4 : [_309412, _309410, _309408, _309406, _309404, _309402, _309400, _309398, _309396, _309394, 2335 ^ [_309394, _309396, _309398, _309400, _309402, _309404, _309406, _309408, _309410, _309412]]], (2349 ^ _219113) ^ [_310127, _310129, _310131, _310133, _310135, _310137, _310139, _310141, _310143, _310145] ^ [] : [-(p6) : -([_310145, _310143, _310141, _310139, _310137, _310135, _310133, _310131, _310129, _310127]), p4 : [_310145, _310143, _310141, _310139, _310137, _310135, _310133, _310131, _310129, _310127, 2352 ^ [_310127, _310129, _310131, _310133, _310135, _310137, _310139, _310141, _310143, _310145]]], (2356 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2362 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2368 ^ _219113) ^ [] ^ [] : [false___ : [], -(false___) : -([])], (2384 ^ _219113) ^ [_311388, _311390, _311392, _311394, _311396, _311398, _311400, _311402, _311404, _311406] ^ [] : [-(p2) : -([_311406, _311404, _311402, _311400, _311398, _311396, _311394, _311392, _311390, _311388]), p6 : [_311406, _311404, _311402, _311400, _311398, _311396, _311394, _311392, _311390, _311388, 2387 ^ [_311388, _311390, _311392, _311394, _311396, _311398, _311400, _311402, _311404, _311406]]], (2401 ^ _219113) ^ [_312121, _312123, _312125, _312127, _312129, _312131, _312133, _312135, _312137, _312139] ^ [] : [-(p4) : -([_312139, _312137, _312135, _312133, _312131, _312129, _312127, _312125, _312123, _312121]), p6 : [_312139, _312137, _312135, _312133, _312131, _312129, _312127, _312125, _312123, _312121, 2404 ^ [_312121, _312123, _312125, _312127, _312129, _312131, _312133, _312135, _312137, _312139]]], (2436 ^ _219113) ^ [_313620, _313622, _313624, _313626, _313628, _313630, _313632, _313634, _313636, _313638, _313640] ^ [] : [-(p2) : -([_313640, _313638, _313636, _313634, _313632, _313630, _313628, _313626, _313624, _313622, _313620])], (2449 ^ _219113) ^ [_314078, _314080, _314082, _314084, _314086, _314088, _314090, _314092, _314094, _314096, _314098] ^ [] : [-(p4) : -([_314098, _314096, _314094, _314092, _314090, _314088, _314086, _314084, _314082, _314080, _314078])], (2462 ^ _219113) ^ [_314536, _314538, _314540, _314542, _314544, _314546, _314548, _314550, _314552, _314554, _314556] ^ [] : [-(p4) : -([_314556, _314554, _314552, _314550, _314548, _314546, _314544, _314542, _314540, _314538, _314536])], (2475 ^ _219113) ^ [_314971, _314973, _314975, _314977, _314979, _314981, _314983, _314985, _314987, _314989, _314991] ^ [] : [-(p6) : -([_314991, _314989, _314987, _314985, _314983, _314981, _314979, _314977, _314975, _314973, _314971])], (2418 ^ _219113) ^ [_312854, _312856, _312858, _312860, _312862, _312864, _312866, _312868, _312870, _312872] ^ [] : [-(p6) : -([_312872, _312870, _312868, _312866, _312864, _312862, _312860, _312858, _312856, _312854]), p6 : [_312872, _312870, _312868, _312866, _312864, _312862, _312860, _312858, _312856, _312854, 2421 ^ [_312854, _312856, _312858, _312860, _312862, _312864, _312866, _312868, _312870, _312872]]]]
% 62.86/64.25
% 62.86/64.25 We prove that the given matrix is valid, i.e. for
% 62.86/64.25 a given substitution it evaluates to true for all
% 62.86/64.25 interpretations. A matrix is true iff at least one
% 62.86/64.25 of its clauses is true; a clause is true iff all of
% 62.86/64.25 its elements (literals and submatrices) are true.
% 62.86/64.25
% 62.86/64.25 The proof is by contradiction:
% 62.86/64.25 Assume there is an interpretation so that the given
% 62.86/64.25 matrix evaluates to false. Then in each clause there
% 62.86/64.25 has to be at least one element that is false.
% 62.86/64.25
% 62.86/64.25 Then clause (6 ^ 0) is false if at least one of the following is false:
% 62.86/64.25 [p2 : [4 ^ []]]
% 62.86/64.25 1 Assume p2 : [[], [], [], [], [], [], [], [], [], [], 4 ^ []] is false.
% 62.86/64.25 Then clause (2436 ^ 1) under the substitution [[_313620, _313622, _313624, _313626, _313628, _313630, _313632, _313634, _313636, _313638, _313640], [4 ^ [], [], [], [], [], [], [], [], [], [], []]]
% 62.86/64.25 is true.
% 62.86/64.25
% 62.86/64.25 Therefore there is no interpretation that makes the
% 62.86/64.25 given matrix false. Hence the given matrix is valid.
% 62.86/64.25 q.e.d.
% 62.86/64.25 ------------------------------------------------------
% 62.86/64.25 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.vSC3cRZDxQ/theBenchmark.p.qmf
% 62.86/64.25 % nanoCoP-M exiting
%------------------------------------------------------------------------------