%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP097_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:14:06 PM UTC 2026
% Result : Theorem 9.12s 10.19s
% Output : Proof 9.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYP097_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_nanocopm %s %d
% 0.16/0.33 % Computer : n015.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 17:32:31 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.30/0.46 % Logic is d
% 0.30/0.46 % Designation is rigid
% 0.30/0.47 % Terms are local
% 0.30/0.47 % Domains are const
% 0.30/0.48 ------------ Start QMF file ---------------
% 0.30/0.48 %------------------------------------------------------------------------------
% 0.30/0.48 % File : SYP097_1 : TPTP v9.3.0. Released v9.3.0.
% 0.30/0.48 % Domain : Syntactic
% 0.30/0.48 % Problem : Logic KD, problem k_t4p, size 10
% 0.30/0.48 % Version : Especial.
% 0.30/0.48 % English :
% 0.30/0.48 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.30/0.48 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.30/0.48 % Source : [Ste24]
% 0.30/0.48 % Names : KD/k_t4p_p/10.p
% 0.30/0.48 % Status : Theorem
% 0.30/0.48 % Rating : ? v9.2.0
% 0.30/0.48 % Syntax : Number of formulae : 5 ( 0 unt; 4 typ; 0 def)
% 0.30/0.48 % Number of atoms : 97 ( 0 equ)
% 0.30/0.48 % Maximal formula atoms : 97 ( 97 avg)
% 0.30/0.48 % Number of connectives : 400 ( 75 ~; 51 |; 25 &)
% 0.30/0.48 % ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% 0.30/0.48 % ( 229 {.}; 0 {#})
% 0.30/0.48 % Maximal formula depth : 44 ( 44 avg)
% 0.30/0.48 % Maximal term depth : 0 ( 0 avg)
% 0.30/0.48 % Number of types : 1 ( 0 usr)
% 0.30/0.48 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.30/0.48 % Number of predicates : 4 ( 4 usr; 4 prp; 0-0 aty)
% 0.30/0.48 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.30/0.48 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.30/0.48 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.30/0.48 % Comments :
% 0.30/0.48 %------------------------------------------------------------------------------
% 0.30/0.48 qmf(10,conjecture,( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( ~ ( ( #box : ( ~ ( p1 ) ) => #box : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #box : ( #dia : ( #box : ( p0 ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) ) | #box : ( ( ~ ( #box : ( p1 ) ) => #box : ( ~ ( #box : ( p1 ) ) ) ) ) | #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( #dia : ( #box : ( p1 ) & #dia : ( #dia : ( ~ ( p1 ) ) ) ) | #dia : ( ( #box : ( #dia : ( p0 ) ) & #box : ( ~ ( p0 ) | #box : ( p3 ) ) ) | #dia : ( #box : ( #dia : ( #box : ( ~ ( p0 ) | #box : ( p3 ) ) ) ) & #box : ( #dia : ( p0 ) ) ) | ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) | #box : ( p3 ) ) ) ) ) | #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) ) & p0 & #dia : ( ~ ( p0 ) | #box : ( p3 ) ) ) | #dia : ( #box : ( ~ ( p0 ) | #box : ( p3 ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) ) | #dia : ( #box : ( #dia : ( p1 ) ) & #dia : ( #dia : ( #box : ( ~ ( p1 ) ) ) ) ) | #dia : ( p4 ) )).
% 0.30/0.48 %------------------------------------------------------------------------------
% 0.30/0.48 ------------ End QMF file ---------------
% 9.12/10.19
% 9.12/10.19 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.wXGt361e8E/theBenchmark.p.qmf : (modal (d/const))
% 9.12/10.19 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.wXGt361e8E/theBenchmark.p.qmf
% 9.12/10.19 ------------------------------------------------------
% 9.12/10.19 Explanations for the proof presented below:
% 9.12/10.19 - equality axioms are added if required
% 9.12/10.19 - terms and variables are represented by Prolog terms
% 9.12/10.19 and Prolog variables, negation is represented by -
% 9.12/10.19 - a prefix Pre is a list of variables and constants
% 9.12/10.19 and assigned to each literal Lit, i.e. Pre:Lit
% 9.12/10.19 - clauses and (sub-)matrices have a unique label I^K:
% 9.12/10.19 or I^K^[..]:, where I is a unique number/identifier
% 9.12/10.19 and K identifies the instance of clause/matrix I
% 9.12/10.19 - I:Lit refers to literal Lit in clause number I
% 9.12/10.19 - in the matrix, I^[t1,..,tn] may represent the atom
% 9.12/10.19 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 9.12/10.19 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 9.12/10.19 the assignments X1:=t1, .., Xn:=tn (for both term
% 9.12/10.19 and prefix variables)
% 9.12/10.19
% 9.12/10.19 Proof:
% 9.12/10.19 ------
% 9.12/10.19 Translation into a non-clausal matrix:
% 9.12/10.19 [(3 ^ _57939) ^ [_58045] ^ [] : [-(p1) : -([_58045, 4 ^ [_58045]]), 9 ^ _57939 : [(10 ^ _57939) ^ [_58281, _58283] ^ [] : [p1 : [_58045, _58283, _58281]]]], (14 ^ _57939) ^ [_58470] ^ [] : [-(p1) : -([11 ^ [], _58470, 15 ^ [_58470]]), 20 ^ _57939 : [(21 ^ _57939) ^ [_58716, _58718] ^ [] : [p1 : [11 ^ [], _58470, _58718, _58716]]]], (182 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 179 ^ [], 180 ^ []]], (186 ^ _57939) ^ [_65870] ^ [] : [-(p1) : -([11 ^ [], 179 ^ [], 183 ^ [], _65870])], (25 ^ _57939) ^ [_58911] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], _58911, 26 ^ [_58911]]), 31 ^ _57939 : [(32 ^ _57939) ^ [_59167, _59169] ^ [] : [p1 : [11 ^ [], 22 ^ [], _58911, _59169, _59167]]]], (174 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 171 ^ [], 172 ^ []]], (178 ^ _57939) ^ [_65593] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 171 ^ [], 175 ^ [], _65593])], (36 ^ _57939) ^ [_59368] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], _59368, 37 ^ [_59368]]), 42 ^ _57939 : [(43 ^ _57939) ^ [_59634, _59636] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], _59368, _59636, _59634]]]], (166 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 163 ^ [], 164 ^ []]], (170 ^ _57939) ^ [_65306] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 163 ^ [], 167 ^ [], _65306])], (47 ^ _57939) ^ [_59841] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], _59841, 48 ^ [_59841]]), 53 ^ _57939 : [(54 ^ _57939) ^ [_60117, _60119] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], _59841, _60119, _60117]]]], (158 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 155 ^ [], 156 ^ []]], (162 ^ _57939) ^ [_65009] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 155 ^ [], 159 ^ [], _65009])], (58 ^ _57939) ^ [_60330] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], _60330, 59 ^ [_60330]]), 64 ^ _57939 : [(65 ^ _57939) ^ [_60616, _60618] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], _60330, _60618, _60616]]]], (150 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 147 ^ [], 148 ^ []]], (154 ^ _57939) ^ [_64702] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 147 ^ [], 151 ^ [], _64702])], (69 ^ _57939) ^ [_60835] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], _60835, 70 ^ [_60835]]), 75 ^ _57939 : [(76 ^ _57939) ^ [_61131, _61133] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], _60835, _61133, _61131]]]], (142 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 139 ^ [], 140 ^ []]], (146 ^ _57939) ^ [_64385] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 139 ^ [], 143 ^ [], _64385])], (80 ^ _57939) ^ [_61356] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], _61356, 81 ^ [_61356]]), 86 ^ _57939 : [(87 ^ _57939) ^ [_61662, _61664] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], _61356, _61664, _61662]]]], (134 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 131 ^ [], 132 ^ []]], (138 ^ _57939) ^ [_64058] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 131 ^ [], 135 ^ [], _64058])], (91 ^ _57939) ^ [_61893] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], _61893, 92 ^ [_61893]]), 97 ^ _57939 : [(98 ^ _57939) ^ [_62209, _62211] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], _61893, _62211, _62209]]]], (126 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 123 ^ [], 124 ^ []]], (130 ^ _57939) ^ [_63721] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 123 ^ [], 127 ^ [], _63721])], (114 ^ _57939) ^ [_63020] ^ [] : [p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], _63020, 112 ^ [_63020]]], (118 ^ _57939) ^ [] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 115 ^ [], 116 ^ []]], (122 ^ _57939) ^ [_63372] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 115 ^ [], 119 ^ [], _63372])], (102 ^ _57939) ^ [_62446] ^ [] : [-(p1) : -([11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], _62446, 103 ^ [_62446]]), 108 ^ _57939 : [(109 ^ _57939) ^ [_62772, _62774] ^ [] : [p1 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], _62446, _62774, _62772]]]], (190 ^ _57939) ^ [] ^ [] : [p1 : [187 ^ [], 188 ^ []]], (194 ^ _57939) ^ [_66160] ^ [] : [-(p1) : -([187 ^ [], 191 ^ [], _66160])], (197 ^ _57939) ^ [_66290] ^ [] : [p1 : [_66290, 198 ^ [_66290]], 203 ^ _57939 : [(204 ^ _57939) ^ [_66520, _66522] ^ [] : [-(p1) : -([_66290, _66522, _66520])]]], (493 ^ _57939) ^ [_82225] ^ [] : [p4 : [_82225]], (481 ^ _57939) ^ [_81822] ^ [] : [484 ^ _57939 : [(485 ^ _57939) ^ [_81946] ^ [] : [p1 : [_81822, 482 ^ [_81822], _81946]]], 489 ^ _57939 : [(490 ^ _57939) ^ [_82112, _82114] ^ [] : [-(p1) : -([_81822, _82114, _82112, 488 ^ [_81822, _82112, _82114]])]]], (208 ^ _57939) ^ [_66701, _66703] ^ [] : [p1 : [_66703, _66701, 209 ^ [_66701, _66703]], 214 ^ _57939 : [(215 ^ _57939) ^ [_66953, _66955] ^ [] : [-(p1) : -([_66703, _66701, _66955, _66953])]]], (469 ^ _57939) ^ [_81343, _81345] ^ [] : [472 ^ _57939 : [(473 ^ _57939) ^ [_81479] ^ [] : [p1 : [_81345, _81343, 470 ^ [_81343, _81345], _81479]]], 477 ^ _57939 : [(478 ^ _57939) ^ [_81663, _81665] ^ [] : [-(p1) : -([_81345, _81343, _81665, _81663, 476 ^ [_81343, _81345, _81663, _81665]])]]], (219 ^ _57939) ^ [_67142, _67144, _67146] ^ [] : [p1 : [_67146, _67144, _67142, 220 ^ [_67142, _67144, _67146]], 225 ^ _57939 : [(226 ^ _57939) ^ [_67416, _67418] ^ [] : [-(p1) : -([_67146, _67144, _67142, _67418, _67416])]]], (457 ^ _57939) ^ [_80849, _80851, _80853] ^ [] : [460 ^ _57939 : [(461 ^ _57939) ^ [_80997] ^ [] : [p1 : [_80853, _80851, _80849, 458 ^ [_80849, _80851, _80853], _80997]]], 465 ^ _57939 : [(466 ^ _57939) ^ [_81199, _81201] ^ [] : [-(p1) : -([_80853, _80851, _80849, _81201, _81199, 464 ^ [_80849, _80851, _80853, _81199, _81201]])]]], (230 ^ _57939) ^ [_67613, _67615, _67617, _67619] ^ [] : [p1 : [_67619, _67617, _67615, _67613, 231 ^ [_67613, _67615, _67617, _67619]], 236 ^ _57939 : [(237 ^ _57939) ^ [_67909, _67911] ^ [] : [-(p1) : -([_67619, _67617, _67615, _67613, _67911, _67909])]]], (445 ^ _57939) ^ [_80317, _80319, _80321, _80323] ^ [] : [448 ^ _57939 : [(449 ^ _57939) ^ [_80477] ^ [] : [p1 : [_80323, _80321, _80319, _80317, 446 ^ [_80317, _80319, _80321, _80323], _80477]]], 453 ^ _57939 : [(454 ^ _57939) ^ [_80697, _80699] ^ [] : [-(p1) : -([_80323, _80321, _80319, _80317, _80699, _80697, 452 ^ [_80317, _80319, _80321, _80323, _80697, _80699]])]]], (241 ^ _57939) ^ [_68114, _68116, _68118, _68120, _68122] ^ [] : [p1 : [_68122, _68120, _68118, _68116, _68114, 242 ^ [_68114, _68116, _68118, _68120, _68122]], 247 ^ _57939 : [(248 ^ _57939) ^ [_68432, _68434] ^ [] : [-(p1) : -([_68122, _68120, _68118, _68116, _68114, _68434, _68432])]]], (433 ^ _57939) ^ [_79747, _79749, _79751, _79753, _79755] ^ [] : [436 ^ _57939 : [(437 ^ _57939) ^ [_79919] ^ [] : [p1 : [_79755, _79753, _79751, _79749, _79747, 434 ^ [_79747, _79749, _79751, _79753, _79755], _79919]]], 441 ^ _57939 : [(442 ^ _57939) ^ [_80157, _80159] ^ [] : [-(p1) : -([_79755, _79753, _79751, _79749, _79747, _80159, _80157, 440 ^ [_79747, _79749, _79751, _79753, _79755, _80157, _80159]])]]], (252 ^ _57939) ^ [_68645, _68647, _68649, _68651, _68653, _68655] ^ [] : [p1 : [_68655, _68653, _68651, _68649, _68647, _68645, 253 ^ [_68645, _68647, _68649, _68651, _68653, _68655]], 258 ^ _57939 : [(259 ^ _57939) ^ [_68985, _68987] ^ [] : [-(p1) : -([_68655, _68653, _68651, _68649, _68647, _68645, _68987, _68985])]]], (421 ^ _57939) ^ [_79139, _79141, _79143, _79145, _79147, _79149] ^ [] : [424 ^ _57939 : [(425 ^ _57939) ^ [_79323] ^ [] : [p1 : [_79149, _79147, _79145, _79143, _79141, _79139, 422 ^ [_79139, _79141, _79143, _79145, _79147, _79149], _79323]]], 429 ^ _57939 : [(430 ^ _57939) ^ [_79579, _79581] ^ [] : [-(p1) : -([_79149, _79147, _79145, _79143, _79141, _79139, _79581, _79579, 428 ^ [_79139, _79141, _79143, _79145, _79147, _79149, _79579, _79581]])]]], (263 ^ _57939) ^ [_69206, _69208, _69210, _69212, _69214, _69216, _69218] ^ [] : [p1 : [_69218, _69216, _69214, _69212, _69210, _69208, _69206, 264 ^ [_69206, _69208, _69210, _69212, _69214, _69216, _69218]], 269 ^ _57939 : [(270 ^ _57939) ^ [_69568, _69570] ^ [] : [-(p1) : -([_69218, _69216, _69214, _69212, _69210, _69208, _69206, _69570, _69568])]]], (409 ^ _57939) ^ [_78493, _78495, _78497, _78499, _78501, _78503, _78505] ^ [] : [412 ^ _57939 : [(413 ^ _57939) ^ [_78689] ^ [] : [p1 : [_78505, _78503, _78501, _78499, _78497, _78495, _78493, 410 ^ [_78493, _78495, _78497, _78499, _78501, _78503, _78505], _78689]]], 417 ^ _57939 : [(418 ^ _57939) ^ [_78963, _78965] ^ [] : [-(p1) : -([_78505, _78503, _78501, _78499, _78497, _78495, _78493, _78965, _78963, 416 ^ [_78493, _78495, _78497, _78499, _78501, _78503, _78505, _78963, _78965]])]]], (274 ^ _57939) ^ [_69797, _69799, _69801, _69803, _69805, _69807, _69809, _69811] ^ [] : [p1 : [_69811, _69809, _69807, _69805, _69803, _69801, _69799, _69797, 275 ^ [_69797, _69799, _69801, _69803, _69805, _69807, _69809, _69811]], 280 ^ _57939 : [(281 ^ _57939) ^ [_70181, _70183] ^ [] : [-(p1) : -([_69811, _69809, _69807, _69805, _69803, _69801, _69799, _69797, _70183, _70181])]]], (397 ^ _57939) ^ [_77809, _77811, _77813, _77815, _77817, _77819, _77821, _77823] ^ [] : [400 ^ _57939 : [(401 ^ _57939) ^ [_78017] ^ [] : [p1 : [_77823, _77821, _77819, _77817, _77815, _77813, _77811, _77809, 398 ^ [_77809, _77811, _77813, _77815, _77817, _77819, _77821, _77823], _78017]]], 405 ^ _57939 : [(406 ^ _57939) ^ [_78309, _78311] ^ [] : [-(p1) : -([_77823, _77821, _77819, _77817, _77815, _77813, _77811, _77809, _78311, _78309, 404 ^ [_77809, _77811, _77813, _77815, _77817, _77819, _77821, _77823, _78309, _78311]])]]], (285 ^ _57939) ^ [_70418, _70420, _70422, _70424, _70426, _70428, _70430, _70432, _70434] ^ [] : [p1 : [_70434, _70432, _70430, _70428, _70426, _70424, _70422, _70420, _70418, 286 ^ [_70418, _70420, _70422, _70424, _70426, _70428, _70430, _70432, _70434]], 291 ^ _57939 : [(292 ^ _57939) ^ [_70824, _70826] ^ [] : [-(p1) : -([_70434, _70432, _70430, _70428, _70426, _70424, _70422, _70420, _70418, _70826, _70824])]]], (385 ^ _57939) ^ [_77087, _77089, _77091, _77093, _77095, _77097, _77099, _77101, _77103] ^ [] : [388 ^ _57939 : [(389 ^ _57939) ^ [_77307] ^ [] : [p1 : [_77103, _77101, _77099, _77097, _77095, _77093, _77091, _77089, _77087, 386 ^ [_77087, _77089, _77091, _77093, _77095, _77097, _77099, _77101, _77103], _77307]]], 393 ^ _57939 : [(394 ^ _57939) ^ [_77617, _77619] ^ [] : [-(p1) : -([_77103, _77101, _77099, _77097, _77095, _77093, _77091, _77089, _77087, _77619, _77617, 392 ^ [_77087, _77089, _77091, _77093, _77095, _77097, _77099, _77101, _77103, _77617, _77619]])]]], (296 ^ _57939) ^ [_71069, _71071, _71073, _71075, _71077, _71079, _71081, _71083, _71085, _71087] ^ [] : [p1 : [_71087, _71085, _71083, _71081, _71079, _71077, _71075, _71073, _71071, _71069, 297 ^ [_71069, _71071, _71073, _71075, _71077, _71079, _71081, _71083, _71085, _71087]], 302 ^ _57939 : [(303 ^ _57939) ^ [_71497, _71499] ^ [] : [-(p1) : -([_71087, _71085, _71083, _71081, _71079, _71077, _71075, _71073, _71071, _71069, _71499, _71497])]]], (373 ^ _57939) ^ [_76327, _76329, _76331, _76333, _76335, _76337, _76339, _76341, _76343, _76345] ^ [] : [376 ^ _57939 : [(377 ^ _57939) ^ [_76559] ^ [] : [p1 : [_76345, _76343, _76341, _76339, _76337, _76335, _76333, _76331, _76329, _76327, 374 ^ [_76327, _76329, _76331, _76333, _76335, _76337, _76339, _76341, _76343, _76345], _76559]]], 381 ^ _57939 : [(382 ^ _57939) ^ [_76887, _76889] ^ [] : [-(p1) : -([_76345, _76343, _76341, _76339, _76337, _76335, _76333, _76331, _76329, _76327, _76889, _76887, 380 ^ [_76327, _76329, _76331, _76333, _76335, _76337, _76339, _76341, _76343, _76345, _76887, _76889]])]]], (306 ^ _57939) ^ [_71711, _71713, _71715, _71717, _71719, _71721, _71723, _71725, _71727, _71729] ^ [] : [309 ^ _57939 : [(310 ^ _57939) ^ [_71943] ^ [] : [p0 : [_71729, _71727, _71725, _71723, _71721, _71719, _71717, _71715, _71713, _71711, 307 ^ [_71711, _71713, _71715, _71717, _71719, _71721, _71723, _71725, _71727, _71729], _71943]]], 312 ^ _57939 : [(313 ^ _57939) ^ [] ^ [] : [-(p0) : -([_71729, _71727, _71725, _71723, _71721, _71719, _71717, _71715, _71713, _71711, 311 ^ [_71711, _71713, _71715, _71717, _71719, _71721, _71723, _71725, _71727, _71729]])], (316 ^ _57939) ^ [] ^ [] : [p3 : [_71729, _71727, _71725, _71723, _71721, _71719, _71717, _71715, _71713, _71711, 311 ^ [_71711, _71713, _71715, _71717, _71719, _71721, _71723, _71725, _71727, _71729], 314 ^ [_71711, _71713, _71715, _71717, _71719, _71721, _71723, _71725, _71727, _71729]]]]], (319 ^ _57939) ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623] ^ [] : [323 ^ _57939 : [(324 ^ _57939) ^ [_72948] ^ [] : [-(p0) : -([_72623, _72621, _72619, _72617, _72615, _72613, _72611, _72609, _72607, _72605, _72603, 320 ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623], _72948, 322 ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623, _72948]])], (327 ^ _57939) ^ [_73190] ^ [] : [p3 : [_72623, _72621, _72619, _72617, _72615, _72613, _72611, _72609, _72607, _72605, _72603, 320 ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623], _73190, 322 ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623, _73190], 325 ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623, _73190]]]], 330 ^ _57939 : [(331 ^ _57939) ^ [_73522] ^ [] : [p0 : [_72623, _72621, _72619, _72617, _72615, _72613, _72611, _72609, _72607, _72605, _72603, 328 ^ [_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623], _73522]]]], (333 ^ _57939) ^ [_73704, _73706, _73708, _73710, _73712, _73714, _73716, _73718, _73720, _73722] ^ [] : [336 ^ _57939 : [(337 ^ _57939) ^ [_73936] ^ [] : [p0 : [_73722, _73720, _73718, _73716, _73714, _73712, _73710, _73708, _73706, _73704, 334 ^ [_73704, _73706, _73708, _73710, _73712, _73714, _73716, _73718, _73720, _73722], _73936]]], 341 ^ _57939 : [(342 ^ _57939) ^ [_74287, _74289] ^ [] : [-(p0) : -([_73722, _73720, _73718, _73716, _73714, _73712, _73710, _73708, _73706, _73704, _74289, _74287, 340 ^ [_73704, _73706, _73708, _73710, _73712, _73714, _73716, _73718, _73720, _73722, _74287, _74289]])], (345 ^ _57939) ^ [_74498, _74500] ^ [] : [p3 : [_73722, _73720, _73718, _73716, _73714, _73712, _73710, _73708, _73706, _73704, _74500, _74498, 340 ^ [_73704, _73706, _73708, _73710, _73712, _73714, _73716, _73718, _73720, _73722, _74498, _74500], 343 ^ [_73704, _73706, _73708, _73710, _73712, _73714, _73716, _73718, _73720, _73722, _74498, _74500]]]]], (367 ^ _57939) ^ [_75919, _75921, _75923, _75925, _75927, _75929, _75931, _75933, _75935, _75937, _75939] ^ [] : [-(p0) : -([_75939, _75937, _75935, _75933, _75931, _75929, _75927, _75925, _75923, _75921, _75919, 365 ^ [_75919, _75921, _75923, _75925, _75927, _75929, _75931, _75933, _75935, _75937, _75939]])], (370 ^ _57939) ^ [_76102, _76104, _76106, _76108, _76110, _76112, _76114, _76116, _76118, _76120, _76122] ^ [] : [p3 : [_76122, _76120, _76118, _76116, _76114, _76112, _76110, _76108, _76106, _76104, _76102, 365 ^ [_76102, _76104, _76106, _76108, _76110, _76112, _76114, _76116, _76118, _76120, _76122], 368 ^ [_76102, _76104, _76106, _76108, _76110, _76112, _76114, _76116, _76118, _76120, _76122]]], (348 ^ _57939) ^ [_74752, _74754, _74756, _74758, _74760, _74762, _74764, _74766, _74768, _74770, _74772] ^ [] : [352 ^ _57939 : [(353 ^ _57939) ^ [_75063, _75065] ^ [] : [p0 : [_74772, _74770, _74768, _74766, _74764, _74762, _74760, _74758, _74756, _74754, _74752, _75065, 350 ^ [_74752, _74754, _74756, _74758, _74760, _74762, _74764, _74766, _74768, _74770, _74772, _75065], _75063]]], p0 : [_74772, _74770, _74768, _74766, _74764, _74762, _74760, _74758, _74756, _74754, _74752], 359 ^ _57939 : [(360 ^ _57939) ^ [_75469] ^ [] : [-(p0) : -([_74772, _74770, _74768, _74766, _74764, _74762, _74760, _74758, _74756, _74754, _74752, _75469])], (363 ^ _57939) ^ [_75651] ^ [] : [p3 : [_74772, _74770, _74768, _74766, _74764, _74762, _74760, _74758, _74756, _74754, _74752, _75651, 361 ^ [_74752, _74754, _74756, _74758, _74760, _74762, _74764, _74766, _74768, _74770, _74772, _75651]]]]]]
% 9.30/10.32
% 9.30/10.32 We prove that the given matrix is valid, i.e. for
% 9.30/10.32 a given substitution it evaluates to true for all
% 9.30/10.32 interpretations. A matrix is true iff at least one
% 9.30/10.32 of its clauses is true; a clause is true iff all of
% 9.30/10.32 its elements (literals and submatrices) are true.
% 9.30/10.32
% 9.30/10.32 The proof is by contradiction:
% 9.30/10.32 Assume there is an interpretation so that the given
% 9.30/10.32 matrix evaluates to false. Then in each clause there
% 9.30/10.32 has to be at least one element that is false.
% 9.30/10.32
% 9.30/10.32 Then clause (114 ^ 0) under the substitution [[_63020], [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.30/10.32 is false if at least one of the following is false:
% 9.30/10.32 [p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 112 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]]
% 9.30/10.32 1 Assume p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 112 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]] is false.
% 9.30/10.32 Then clause (348 ^ 1) under the substitution [[_74752, _74754, _74756, _74758, _74760, _74762, _74764, _74766, _74768, _74770, _74772, _75469, _75063, _75065], [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 112 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]], 322 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 350 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.30/10.32 is false if at least one of the following is false:
% 9.30/10.32 [353 : p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 350 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]], 322 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 350 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]], 353 : p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.40/10.41 1.1 Assume p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 350 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]], 322 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 350 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]] is false.
% 9.40/10.41 Then clause (319 ^ 4) under the substitution [[_72603, _72605, _72607, _72609, _72611, _72613, _72615, _72617, _72619, _72621, _72623, _72948, _73522], [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 350 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 320 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]], 340 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 328 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]]
% 9.40/10.41 is false if at least one of the following is false:
% 9.40/10.49 [331 : p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 328 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 340 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 328 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]]
% 9.40/10.49 1.1.1 Assume p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 328 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 340 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 328 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]] is false.
% 9.40/10.49 Then clause (333 ^ 7) under the substitution [[_73704, _73706, _73708, _73710, _73712, _73714, _73716, _73718, _73720, _73722, _74287, _74289, _73936], [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 328 ^ [311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 365 ^ [334 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.40/10.49 is false if at least one of the following is false:
% 9.40/10.49 [337 : p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 334 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 365 ^ [334 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.40/10.49 1.1.1.1 Assume p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 334 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 365 ^ [334 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]] is false.
% 9.40/10.49 Then clause (367 ^ 10) under the substitution [[_75919, _75921, _75923, _75925, _75927, _75929, _75931, _75933, _75935, _75937, _75939], [334 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]
% 9.40/10.49 is true.
% 9.40/10.49 1.2 Assume p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 311 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]] is false.
% 9.40/10.49 Then clause (306 ^ 2) under the substitution [[_71711, _71713, _71715, _71717, _71719, _71721, _71723, _71725, _71727, _71729, _71943], [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ [], 365 ^ [307 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.50/10.50 is false if at least one of the following is false:
% 9.50/10.50 [310 : p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 307 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 365 ^ [307 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]]
% 9.50/10.50 1.2.1 Assume p0 : [11 ^ [], 22 ^ [], 33 ^ [], 44 ^ [], 55 ^ [], 66 ^ [], 77 ^ [], 88 ^ [], 99 ^ [], 110 ^ [], 307 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 365 ^ [307 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]] is false.
% 9.50/10.50 Then clause (367 ^ 5) under the substitution [[_75919, _75921, _75923, _75925, _75927, _75929, _75931, _75933, _75935, _75937, _75939], [307 ^ [110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []], 110 ^ [], 99 ^ [], 88 ^ [], 77 ^ [], 66 ^ [], 55 ^ [], 44 ^ [], 33 ^ [], 22 ^ [], 11 ^ []]]
% 9.50/10.50 is true.
% 9.50/10.50
% 9.50/10.50 Therefore there is no interpretation that makes the
% 9.50/10.50 given matrix false. Hence the given matrix is valid.
% 9.50/10.50 q.e.d.
% 9.50/10.50 ------------------------------------------------------
% 9.50/10.50 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.wXGt361e8E/theBenchmark.p.qmf
% 9.50/10.50 % nanoCoP-M exiting
%------------------------------------------------------------------------------