%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP083_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n009.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:05 PM UTC 2026
% Result : Theorem 12.35s 13.30s
% Output : Proof 12.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYP083_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : run_nanocopm %s %d
% 0.15/0.34 % Computer : n009.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 17:20:41 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.26/0.49 % Logic is d
% 0.26/0.49 % Designation is rigid
% 0.26/0.50 % Terms are local
% 0.26/0.50 % Domains are const
% 0.26/0.51 ------------ Start QMF file ---------------
% 0.26/0.51 %------------------------------------------------------------------------------
% 0.26/0.51 % File : SYP083_1 : TPTP v9.3.0. Released v9.3.0.
% 0.26/0.51 % Domain : Syntactic
% 0.26/0.51 % Problem : Logic KD, problem k_d4, size 10
% 0.26/0.51 % Version : Especial.
% 0.26/0.51 % English :
% 0.26/0.51 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.26/0.51 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.26/0.51 % Source : [Ste24]
% 0.26/0.51 % Names : KD/k_d4_p/10.p
% 0.26/0.51 % Status : Theorem
% 0.26/0.51 % Rating : ? v9.2.0
% 0.26/0.51 % Syntax : Number of formulae : 2 ( 0 unt; 1 typ; 0 def)
% 0.26/0.51 % Number of atoms : 110 ( 0 equ)
% 0.26/0.51 % Maximal formula atoms : 110 ( 110 avg)
% 0.26/0.51 % Number of connectives : 674 ( 50 ~; 69 |; 40 &)
% 0.26/0.51 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.26/0.51 % ( 515 {.}; 0 {#})
% 0.26/0.51 % Maximal formula depth : 74 ( 74 avg)
% 0.26/0.51 % Maximal term depth : 0 ( 0 avg)
% 0.26/0.51 % Number of types : 1 ( 0 usr)
% 0.26/0.51 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.26/0.51 % Number of predicates : 2 ( 1 usr; 2 prp; 0-0 aty)
% 0.26/0.51 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.26/0.51 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.26/0.51 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.26/0.51 % Comments :
% 0.26/0.51 %------------------------------------------------------------------------------
% 0.26/0.51 qmf(10,conjecture,( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #box : ( $false ) ) | #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) | #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) | #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) | #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #box : ( $false ) ) ) | #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) | #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) | #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) | #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) | #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) ) ) ) ) ) | #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #box : ( #dia : ( ~ ( p0 ) ) | p0 ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( $false ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( p0 ) & #dia : ( #dia : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #box : ( #dia : ( p0 ) ) & #dia : ( #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( p0 & #dia : ( #box : ( ~ ( p0 ) ) ) ) ) ) ) ) ) ) ) ) ) | #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( #dia : ( ~ ( p0 ) & #dia : ( #box : ( p0 ) ) ) ) ) ) ) ) ) ) ) ) )).
% 0.26/0.51 %------------------------------------------------------------------------------
% 0.26/0.51 ------------ End QMF file ---------------
% 12.35/13.30
% 12.35/13.30 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.bETpvBy8VW/theBenchmark.p.qmf : (modal (d/const))
% 12.35/13.30 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.bETpvBy8VW/theBenchmark.p.qmf
% 12.35/13.30 ------------------------------------------------------
% 12.35/13.30 Explanations for the proof presented below:
% 12.35/13.30 - equality axioms are added if required
% 12.35/13.30 - terms and variables are represented by Prolog terms
% 12.35/13.30 and Prolog variables, negation is represented by -
% 12.35/13.30 - a prefix Pre is a list of variables and constants
% 12.35/13.30 and assigned to each literal Lit, i.e. Pre:Lit
% 12.35/13.30 - clauses and (sub-)matrices have a unique label I^K:
% 12.35/13.30 or I^K^[..]:, where I is a unique number/identifier
% 12.35/13.30 and K identifies the instance of clause/matrix I
% 12.35/13.30 - I:Lit refers to literal Lit in clause number I
% 12.35/13.30 - in the matrix, I^[t1,..,tn] may represent the atom
% 12.35/13.30 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 12.35/13.30 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 12.35/13.30 the assignments X1:=t1, .., Xn:=tn (for both term
% 12.35/13.30 and prefix variables)
% 12.35/13.30
% 12.35/13.30 Proof:
% 12.35/13.30 ------
% 12.35/13.30 Translation into a non-clausal matrix:
% 12.35/13.30 [(13 ^ _83909) ^ [_84368] ^ [] : [-(p0) : -([1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], _84368])], (15 ^ _83909) ^ [] ^ [] : [p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ []]], (19 ^ _83909) ^ [_84592] ^ [] : [false___ : [_84592, 17 ^ [_84592]], -(false___) : -([_84592, 17 ^ [_84592]])], (26 ^ _83909) ^ [_84889] ^ [] : [p0 : [_84889, 27 ^ [_84889]], 32 ^ _83909 : [(33 ^ _83909) ^ [_85119, _85121] ^ [] : [-(p0) : -([_84889, _85121, _85119])]]], (36 ^ _83909) ^ [_85256] ^ [] : [39 ^ _83909 : [(40 ^ _83909) ^ [_85380] ^ [] : [p0 : [_85256, 37 ^ [_85256], _85380]]], 44 ^ _83909 : [(45 ^ _83909) ^ [_85546, _85548] ^ [] : [-(p0) : -([_85256, _85548, _85546, 43 ^ [_85256, _85546, _85548]])]]], (48 ^ _83909) ^ [_85695] ^ [] : [p0 : [_85695], 53 ^ _83909 : [(54 ^ _83909) ^ [_85895] ^ [] : [-(p0) : -([_85695, _85895, 52 ^ [_85695, _85895]])]]], (57 ^ _83909) ^ [_86037] ^ [] : [-(p0) : -([_86037]), 62 ^ _83909 : [(63 ^ _83909) ^ [_86237] ^ [] : [p0 : [_86037, _86237, 61 ^ [_86037, _86237]]]]], (76 ^ _83909) ^ [_86736] ^ [] : [-(p0) : -([64 ^ [], 65 ^ [], 66 ^ [], 67 ^ [], 68 ^ [], 69 ^ [], 70 ^ [], 71 ^ [], 72 ^ [], 73 ^ [], _86736])], (78 ^ _83909) ^ [] ^ [] : [p0 : [64 ^ [], 65 ^ [], 66 ^ [], 67 ^ [], 68 ^ [], 69 ^ [], 70 ^ [], 71 ^ [], 72 ^ [], 73 ^ []]], (83 ^ _83909) ^ [_86983, _86985] ^ [] : [false___ : [_86985, _86983, 81 ^ [_86983, _86985]], -(false___) : -([_86985, _86983, 81 ^ [_86983, _86985]])], (91 ^ _83909) ^ [_87319, _87321] ^ [] : [p0 : [_87321, _87319, 92 ^ [_87319, _87321]], 97 ^ _83909 : [(98 ^ _83909) ^ [_87571, _87573] ^ [] : [-(p0) : -([_87321, _87319, _87573, _87571])]]], (102 ^ _83909) ^ [_87733, _87735] ^ [] : [105 ^ _83909 : [(106 ^ _83909) ^ [_87869] ^ [] : [p0 : [_87735, _87733, 103 ^ [_87733, _87735], _87869]]], 110 ^ _83909 : [(111 ^ _83909) ^ [_88053, _88055] ^ [] : [-(p0) : -([_87735, _87733, _88055, _88053, 109 ^ [_87733, _87735, _88053, _88055]])]]], (115 ^ _83909) ^ [_88229, _88231] ^ [] : [p0 : [_88231, _88229], 120 ^ _83909 : [(121 ^ _83909) ^ [_88445] ^ [] : [-(p0) : -([_88231, _88229, _88445, 119 ^ [_88229, _88231, _88445]])]]], (125 ^ _83909) ^ [_88614, _88616] ^ [] : [-(p0) : -([_88616, _88614]), 130 ^ _83909 : [(131 ^ _83909) ^ [_88830] ^ [] : [p0 : [_88616, _88614, _88830, 129 ^ [_88614, _88616, _88830]]]]], (144 ^ _83909) ^ [_89335] ^ [] : [-(p0) : -([132 ^ [], 133 ^ [], 134 ^ [], 135 ^ [], 136 ^ [], 137 ^ [], 138 ^ [], 139 ^ [], 140 ^ [], 141 ^ [], _89335])], (146 ^ _83909) ^ [] ^ [] : [p0 : [132 ^ [], 133 ^ [], 134 ^ [], 135 ^ [], 136 ^ [], 137 ^ [], 138 ^ [], 139 ^ [], 140 ^ [], 141 ^ []]], (152 ^ _83909) ^ [_89607, _89609, _89611] ^ [] : [false___ : [_89611, _89609, _89607, 150 ^ [_89607, _89609, _89611]], -(false___) : -([_89611, _89609, _89607, 150 ^ [_89607, _89609, _89611]])], (161 ^ _83909) ^ [_89984, _89986, _89988] ^ [] : [p0 : [_89988, _89986, _89984, 162 ^ [_89984, _89986, _89988]], 167 ^ _83909 : [(168 ^ _83909) ^ [_90258, _90260] ^ [] : [-(p0) : -([_89988, _89986, _89984, _90260, _90258])]]], (173 ^ _83909) ^ [_90447, _90449, _90451] ^ [] : [176 ^ _83909 : [(177 ^ _83909) ^ [_90595] ^ [] : [p0 : [_90451, _90449, _90447, 174 ^ [_90447, _90449, _90451], _90595]]], 181 ^ _83909 : [(182 ^ _83909) ^ [_90797, _90799] ^ [] : [-(p0) : -([_90451, _90449, _90447, _90799, _90797, 180 ^ [_90447, _90449, _90451, _90797, _90799]])]]], (187 ^ _83909) ^ [_91002, _91004, _91006] ^ [] : [p0 : [_91006, _91004, _91002], 192 ^ _83909 : [(193 ^ _83909) ^ [_91234] ^ [] : [-(p0) : -([_91006, _91004, _91002, _91234, 191 ^ [_91002, _91004, _91006, _91234]])]]], (198 ^ _83909) ^ [_91432, _91434, _91436] ^ [] : [-(p0) : -([_91436, _91434, _91432]), 203 ^ _83909 : [(204 ^ _83909) ^ [_91664] ^ [] : [p0 : [_91436, _91434, _91432, _91664, 202 ^ [_91432, _91434, _91436, _91664]]]]], (217 ^ _83909) ^ [_92175] ^ [] : [-(p0) : -([205 ^ [], 206 ^ [], 207 ^ [], 208 ^ [], 209 ^ [], 210 ^ [], 211 ^ [], 212 ^ [], 213 ^ [], 214 ^ [], _92175])], (219 ^ _83909) ^ [] ^ [] : [p0 : [205 ^ [], 206 ^ [], 207 ^ [], 208 ^ [], 209 ^ [], 210 ^ [], 211 ^ [], 212 ^ [], 213 ^ [], 214 ^ []]], (226 ^ _83909) ^ [_92474, _92476, _92478, _92480] ^ [] : [false___ : [_92480, _92478, _92476, _92474, 224 ^ [_92474, _92476, _92478, _92480]], -(false___) : -([_92480, _92478, _92476, _92474, 224 ^ [_92474, _92476, _92478, _92480]])], (236 ^ _83909) ^ [_92894, _92896, _92898, _92900] ^ [] : [p0 : [_92900, _92898, _92896, _92894, 237 ^ [_92894, _92896, _92898, _92900]], 242 ^ _83909 : [(243 ^ _83909) ^ [_93190, _93192] ^ [] : [-(p0) : -([_92900, _92898, _92896, _92894, _93192, _93190])]]], (249 ^ _83909) ^ [_93408, _93410, _93412, _93414] ^ [] : [252 ^ _83909 : [(253 ^ _83909) ^ [_93568] ^ [] : [p0 : [_93414, _93412, _93410, _93408, 250 ^ [_93408, _93410, _93412, _93414], _93568]]], 257 ^ _83909 : [(258 ^ _83909) ^ [_93788, _93790] ^ [] : [-(p0) : -([_93414, _93412, _93410, _93408, _93790, _93788, 256 ^ [_93408, _93410, _93412, _93414, _93788, _93790]])]]], (264 ^ _83909) ^ [_94024, _94026, _94028, _94030] ^ [] : [p0 : [_94030, _94028, _94026, _94024], 269 ^ _83909 : [(270 ^ _83909) ^ [_94272] ^ [] : [-(p0) : -([_94030, _94028, _94026, _94024, _94272, 268 ^ [_94024, _94026, _94028, _94030, _94272]])]]], (276 ^ _83909) ^ [_94501, _94503, _94505, _94507] ^ [] : [-(p0) : -([_94507, _94505, _94503, _94501]), 281 ^ _83909 : [(282 ^ _83909) ^ [_94749] ^ [] : [p0 : [_94507, _94505, _94503, _94501, _94749, 280 ^ [_94501, _94503, _94505, _94507, _94749]]]]], (295 ^ _83909) ^ [_95266] ^ [] : [-(p0) : -([283 ^ [], 284 ^ [], 285 ^ [], 286 ^ [], 287 ^ [], 288 ^ [], 289 ^ [], 290 ^ [], 291 ^ [], 292 ^ [], _95266])], (297 ^ _83909) ^ [] ^ [] : [p0 : [283 ^ [], 284 ^ [], 285 ^ [], 286 ^ [], 287 ^ [], 288 ^ [], 289 ^ [], 290 ^ [], 291 ^ [], 292 ^ []]], (305 ^ _83909) ^ [_95594, _95596, _95598, _95600, _95602] ^ [] : [false___ : [_95602, _95600, _95598, _95596, _95594, 303 ^ [_95594, _95596, _95598, _95600, _95602]], -(false___) : -([_95602, _95600, _95598, _95596, _95594, 303 ^ [_95594, _95596, _95598, _95600, _95602]])], (316 ^ _83909) ^ [_96059, _96061, _96063, _96065, _96067] ^ [] : [p0 : [_96067, _96065, _96063, _96061, _96059, 317 ^ [_96059, _96061, _96063, _96065, _96067]], 322 ^ _83909 : [(323 ^ _83909) ^ [_96377, _96379] ^ [] : [-(p0) : -([_96067, _96065, _96063, _96061, _96059, _96379, _96377])]]], (330 ^ _83909) ^ [_96626, _96628, _96630, _96632, _96634] ^ [] : [333 ^ _83909 : [(334 ^ _83909) ^ [_96798] ^ [] : [p0 : [_96634, _96632, _96630, _96628, _96626, 331 ^ [_96626, _96628, _96630, _96632, _96634], _96798]]], 338 ^ _83909 : [(339 ^ _83909) ^ [_97036, _97038] ^ [] : [-(p0) : -([_96634, _96632, _96630, _96628, _96626, _97038, _97036, 337 ^ [_96626, _96628, _96630, _96632, _96634, _97036, _97038]])]]], (346 ^ _83909) ^ [_97305, _97307, _97309, _97311, _97313] ^ [] : [p0 : [_97313, _97311, _97309, _97307, _97305], 351 ^ _83909 : [(352 ^ _83909) ^ [_97569] ^ [] : [-(p0) : -([_97313, _97311, _97309, _97307, _97305, _97569, 350 ^ [_97305, _97307, _97309, _97311, _97313, _97569]])]]], (359 ^ _83909) ^ [_97831, _97833, _97835, _97837, _97839] ^ [] : [-(p0) : -([_97839, _97837, _97835, _97833, _97831]), 364 ^ _83909 : [(365 ^ _83909) ^ [_98095] ^ [] : [p0 : [_97839, _97837, _97835, _97833, _97831, _98095, 363 ^ [_97831, _97833, _97835, _97837, _97839, _98095]]]]], (378 ^ _83909) ^ [_98618] ^ [] : [-(p0) : -([366 ^ [], 367 ^ [], 368 ^ [], 369 ^ [], 370 ^ [], 371 ^ [], 372 ^ [], 373 ^ [], 374 ^ [], 375 ^ [], _98618])], (380 ^ _83909) ^ [] ^ [] : [p0 : [366 ^ [], 367 ^ [], 368 ^ [], 369 ^ [], 370 ^ [], 371 ^ [], 372 ^ [], 373 ^ [], 374 ^ [], 375 ^ []]], (389 ^ _83909) ^ [_98977, _98979, _98981, _98983, _98985, _98987] ^ [] : [false___ : [_98987, _98985, _98983, _98981, _98979, _98977, 387 ^ [_98977, _98979, _98981, _98983, _98985, _98987]], -(false___) : -([_98987, _98985, _98983, _98981, _98979, _98977, 387 ^ [_98977, _98979, _98981, _98983, _98985, _98987]])], (401 ^ _83909) ^ [_99489, _99491, _99493, _99495, _99497, _99499] ^ [] : [p0 : [_99499, _99497, _99495, _99493, _99491, _99489, 402 ^ [_99489, _99491, _99493, _99495, _99497, _99499]], 407 ^ _83909 : [(408 ^ _83909) ^ [_99829, _99831] ^ [] : [-(p0) : -([_99499, _99497, _99495, _99493, _99491, _99489, _99831, _99829])]]], (416 ^ _83909) ^ [_100111, _100113, _100115, _100117, _100119, _100121] ^ [] : [419 ^ _83909 : [(420 ^ _83909) ^ [_100295] ^ [] : [p0 : [_100121, _100119, _100117, _100115, _100113, _100111, 417 ^ [_100111, _100113, _100115, _100117, _100119, _100121], _100295]]], 424 ^ _83909 : [(425 ^ _83909) ^ [_100551, _100553] ^ [] : [-(p0) : -([_100121, _100119, _100117, _100115, _100113, _100111, _100553, _100551, 423 ^ [_100111, _100113, _100115, _100117, _100119, _100121, _100551, _100553]])]]], (433 ^ _83909) ^ [_100855, _100857, _100859, _100861, _100863, _100865] ^ [] : [p0 : [_100865, _100863, _100861, _100859, _100857, _100855], 438 ^ _83909 : [(439 ^ _83909) ^ [_101135] ^ [] : [-(p0) : -([_100865, _100863, _100861, _100859, _100857, _100855, _101135, 437 ^ [_100855, _100857, _100859, _100861, _100863, _100865, _101135]])]]], (447 ^ _83909) ^ [_101432, _101434, _101436, _101438, _101440, _101442] ^ [] : [-(p0) : -([_101442, _101440, _101438, _101436, _101434, _101432]), 452 ^ _83909 : [(453 ^ _83909) ^ [_101712] ^ [] : [p0 : [_101442, _101440, _101438, _101436, _101434, _101432, _101712, 451 ^ [_101432, _101434, _101436, _101438, _101440, _101442, _101712]]]]], (466 ^ _83909) ^ [_102241] ^ [] : [-(p0) : -([454 ^ [], 455 ^ [], 456 ^ [], 457 ^ [], 458 ^ [], 459 ^ [], 460 ^ [], 461 ^ [], 462 ^ [], 463 ^ [], _102241])], (468 ^ _83909) ^ [] ^ [] : [p0 : [454 ^ [], 455 ^ [], 456 ^ [], 457 ^ [], 458 ^ [], 459 ^ [], 460 ^ [], 461 ^ [], 462 ^ [], 463 ^ []]], (478 ^ _83909) ^ [_102633, _102635, _102637, _102639, _102641, _102643, _102645] ^ [] : [false___ : [_102645, _102643, _102641, _102639, _102637, _102635, _102633, 476 ^ [_102633, _102635, _102637, _102639, _102641, _102643, _102645]], -(false___) : -([_102645, _102643, _102641, _102639, _102637, _102635, _102633, 476 ^ [_102633, _102635, _102637, _102639, _102641, _102643, _102645]])], (491 ^ _83909) ^ [_103194, _103196, _103198, _103200, _103202, _103204, _103206] ^ [] : [p0 : [_103206, _103204, _103202, _103200, _103198, _103196, _103194, 492 ^ [_103194, _103196, _103198, _103200, _103202, _103204, _103206]], 497 ^ _83909 : [(498 ^ _83909) ^ [_103556, _103558] ^ [] : [-(p0) : -([_103206, _103204, _103202, _103200, _103198, _103196, _103194, _103558, _103556])]]], (507 ^ _83909) ^ [_103873, _103875, _103877, _103879, _103881, _103883, _103885] ^ [] : [510 ^ _83909 : [(511 ^ _83909) ^ [_104069] ^ [] : [p0 : [_103885, _103883, _103881, _103879, _103877, _103875, _103873, 508 ^ [_103873, _103875, _103877, _103879, _103881, _103883, _103885], _104069]]], 515 ^ _83909 : [(516 ^ _83909) ^ [_104343, _104345] ^ [] : [-(p0) : -([_103885, _103883, _103881, _103879, _103877, _103875, _103873, _104345, _104343, 514 ^ [_103873, _103875, _103877, _103879, _103881, _103883, _103885, _104343, _104345]])]]], (525 ^ _83909) ^ [_104684, _104686, _104688, _104690, _104692, _104694, _104696] ^ [] : [p0 : [_104696, _104694, _104692, _104690, _104688, _104686, _104684], 530 ^ _83909 : [(531 ^ _83909) ^ [_104980] ^ [] : [-(p0) : -([_104696, _104694, _104692, _104690, _104688, _104686, _104684, _104980, 529 ^ [_104684, _104686, _104688, _104690, _104692, _104694, _104696, _104980]])]]], (540 ^ _83909) ^ [_105314, _105316, _105318, _105320, _105322, _105324, _105326] ^ [] : [-(p0) : -([_105326, _105324, _105322, _105320, _105318, _105316, _105314]), 545 ^ _83909 : [(546 ^ _83909) ^ [_105610] ^ [] : [p0 : [_105326, _105324, _105322, _105320, _105318, _105316, _105314, _105610, 544 ^ [_105314, _105316, _105318, _105320, _105322, _105324, _105326, _105610]]]]], (559 ^ _83909) ^ [_106145] ^ [] : [-(p0) : -([547 ^ [], 548 ^ [], 549 ^ [], 550 ^ [], 551 ^ [], 552 ^ [], 553 ^ [], 554 ^ [], 555 ^ [], 556 ^ [], _106145])], (561 ^ _83909) ^ [] ^ [] : [p0 : [547 ^ [], 548 ^ [], 549 ^ [], 550 ^ [], 551 ^ [], 552 ^ [], 553 ^ [], 554 ^ [], 555 ^ [], 556 ^ []]], (572 ^ _83909) ^ [_106572, _106574, _106576, _106578, _106580, _106582, _106584, _106586] ^ [] : [false___ : [_106586, _106584, _106582, _106580, _106578, _106576, _106574, _106572, 570 ^ [_106572, _106574, _106576, _106578, _106580, _106582, _106584, _106586]], -(false___) : -([_106586, _106584, _106582, _106580, _106578, _106576, _106574, _106572, 570 ^ [_106572, _106574, _106576, _106578, _106580, _106582, _106584, _106586]])], (586 ^ _83909) ^ [_107184, _107186, _107188, _107190, _107192, _107194, _107196, _107198] ^ [] : [p0 : [_107198, _107196, _107194, _107192, _107190, _107188, _107186, _107184, 587 ^ [_107184, _107186, _107188, _107190, _107192, _107194, _107196, _107198]], 592 ^ _83909 : [(593 ^ _83909) ^ [_107568, _107570] ^ [] : [-(p0) : -([_107198, _107196, _107194, _107192, _107190, _107188, _107186, _107184, _107570, _107568])]]], (603 ^ _83909) ^ [_107922, _107924, _107926, _107928, _107930, _107932, _107934, _107936] ^ [] : [606 ^ _83909 : [(607 ^ _83909) ^ [_108130] ^ [] : [p0 : [_107936, _107934, _107932, _107930, _107928, _107926, _107924, _107922, 604 ^ [_107922, _107924, _107926, _107928, _107930, _107932, _107934, _107936], _108130]]], 611 ^ _83909 : [(612 ^ _83909) ^ [_108422, _108424] ^ [] : [-(p0) : -([_107936, _107934, _107932, _107930, _107928, _107926, _107924, _107922, _108424, _108422, 610 ^ [_107922, _107924, _107926, _107928, _107930, _107932, _107934, _107936, _108422, _108424]])]]], (622 ^ _83909) ^ [_108802, _108804, _108806, _108808, _108810, _108812, _108814, _108816] ^ [] : [p0 : [_108816, _108814, _108812, _108810, _108808, _108806, _108804, _108802], 627 ^ _83909 : [(628 ^ _83909) ^ [_109114] ^ [] : [-(p0) : -([_108816, _108814, _108812, _108810, _108808, _108806, _108804, _108802, _109114, 626 ^ [_108802, _108804, _108806, _108808, _108810, _108812, _108814, _108816, _109114]])]]], (638 ^ _83909) ^ [_109487, _109489, _109491, _109493, _109495, _109497, _109499, _109501] ^ [] : [-(p0) : -([_109501, _109499, _109497, _109495, _109493, _109491, _109489, _109487]), 643 ^ _83909 : [(644 ^ _83909) ^ [_109799] ^ [] : [p0 : [_109501, _109499, _109497, _109495, _109493, _109491, _109489, _109487, _109799, 642 ^ [_109487, _109489, _109491, _109493, _109495, _109497, _109499, _109501, _109799]]]]], (657 ^ _83909) ^ [_110340] ^ [] : [-(p0) : -([645 ^ [], 646 ^ [], 647 ^ [], 648 ^ [], 649 ^ [], 650 ^ [], 651 ^ [], 652 ^ [], 653 ^ [], 654 ^ [], _110340])], (659 ^ _83909) ^ [] ^ [] : [p0 : [645 ^ [], 646 ^ [], 647 ^ [], 648 ^ [], 649 ^ [], 650 ^ [], 651 ^ [], 652 ^ [], 653 ^ [], 654 ^ []]], (671 ^ _83909) ^ [_110804, _110806, _110808, _110810, _110812, _110814, _110816, _110818, _110820] ^ [] : [false___ : [_110820, _110818, _110816, _110814, _110812, _110810, _110808, _110806, _110804, 669 ^ [_110804, _110806, _110808, _110810, _110812, _110814, _110816, _110818, _110820]], -(false___) : -([_110820, _110818, _110816, _110814, _110812, _110810, _110808, _110806, _110804, 669 ^ [_110804, _110806, _110808, _110810, _110812, _110814, _110816, _110818, _110820]])], (686 ^ _83909) ^ [_111469, _111471, _111473, _111475, _111477, _111479, _111481, _111483, _111485] ^ [] : [p0 : [_111485, _111483, _111481, _111479, _111477, _111475, _111473, _111471, _111469, 687 ^ [_111469, _111471, _111473, _111475, _111477, _111479, _111481, _111483, _111485]], 692 ^ _83909 : [(693 ^ _83909) ^ [_111875, _111877] ^ [] : [-(p0) : -([_111485, _111483, _111481, _111479, _111477, _111475, _111473, _111471, _111469, _111877, _111875])]]], (704 ^ _83909) ^ [_112268, _112270, _112272, _112274, _112276, _112278, _112280, _112282, _112284] ^ [] : [707 ^ _83909 : [(708 ^ _83909) ^ [_112488] ^ [] : [p0 : [_112284, _112282, _112280, _112278, _112276, _112274, _112272, _112270, _112268, 705 ^ [_112268, _112270, _112272, _112274, _112276, _112278, _112280, _112282, _112284], _112488]]], 712 ^ _83909 : [(713 ^ _83909) ^ [_112798, _112800] ^ [] : [-(p0) : -([_112284, _112282, _112280, _112278, _112276, _112274, _112272, _112270, _112268, _112800, _112798, 711 ^ [_112268, _112270, _112272, _112274, _112276, _112278, _112280, _112282, _112284, _112798, _112800]])]]], (724 ^ _83909) ^ [_113219, _113221, _113223, _113225, _113227, _113229, _113231, _113233, _113235] ^ [] : [p0 : [_113235, _113233, _113231, _113229, _113227, _113225, _113223, _113221, _113219], 729 ^ _83909 : [(730 ^ _83909) ^ [_113547] ^ [] : [-(p0) : -([_113235, _113233, _113231, _113229, _113227, _113225, _113223, _113221, _113219, _113547, 728 ^ [_113219, _113221, _113223, _113225, _113227, _113229, _113231, _113233, _113235, _113547]])]]], (741 ^ _83909) ^ [_113961, _113963, _113965, _113967, _113969, _113971, _113973, _113975, _113977] ^ [] : [-(p0) : -([_113977, _113975, _113973, _113971, _113969, _113967, _113965, _113963, _113961]), 746 ^ _83909 : [(747 ^ _83909) ^ [_114289] ^ [] : [p0 : [_113977, _113975, _113973, _113971, _113969, _113967, _113965, _113963, _113961, _114289, 745 ^ [_113961, _113963, _113965, _113967, _113969, _113971, _113973, _113975, _113977, _114289]]]]], (760 ^ _83909) ^ [_114836] ^ [] : [-(p0) : -([748 ^ [], 749 ^ [], 750 ^ [], 751 ^ [], 752 ^ [], 753 ^ [], 754 ^ [], 755 ^ [], 756 ^ [], 757 ^ [], _114836])], (762 ^ _83909) ^ [] ^ [] : [p0 : [748 ^ [], 749 ^ [], 750 ^ [], 751 ^ [], 752 ^ [], 753 ^ [], 754 ^ [], 755 ^ [], 756 ^ [], 757 ^ []]], (775 ^ _83909) ^ [_115339, _115341, _115343, _115345, _115347, _115349, _115351, _115353, _115355, _115357] ^ [] : [false___ : [_115357, _115355, _115353, _115351, _115349, _115347, _115345, _115343, _115341, _115339, 773 ^ [_115339, _115341, _115343, _115345, _115347, _115349, _115351, _115353, _115355, _115357]], -(false___) : -([_115357, _115355, _115353, _115351, _115349, _115347, _115345, _115343, _115341, _115339, 773 ^ [_115339, _115341, _115343, _115345, _115347, _115349, _115351, _115353, _115355, _115357]])], (791 ^ _83909) ^ [_116059, _116061, _116063, _116065, _116067, _116069, _116071, _116073, _116075, _116077] ^ [] : [p0 : [_116077, _116075, _116073, _116071, _116069, _116067, _116065, _116063, _116061, _116059, 792 ^ [_116059, _116061, _116063, _116065, _116067, _116069, _116071, _116073, _116075, _116077]], 797 ^ _83909 : [(798 ^ _83909) ^ [_116487, _116489] ^ [] : [-(p0) : -([_116077, _116075, _116073, _116071, _116069, _116067, _116065, _116063, _116061, _116059, _116489, _116487])]]], (810 ^ _83909) ^ [_116921, _116923, _116925, _116927, _116929, _116931, _116933, _116935, _116937, _116939] ^ [] : [813 ^ _83909 : [(814 ^ _83909) ^ [_117153] ^ [] : [p0 : [_116939, _116937, _116935, _116933, _116931, _116929, _116927, _116925, _116923, _116921, 811 ^ [_116921, _116923, _116925, _116927, _116929, _116931, _116933, _116935, _116937, _116939], _117153]]], 818 ^ _83909 : [(819 ^ _83909) ^ [_117481, _117483] ^ [] : [-(p0) : -([_116939, _116937, _116935, _116933, _116931, _116929, _116927, _116925, _116923, _116921, _117483, _117481, 817 ^ [_116921, _116923, _116925, _116927, _116929, _116931, _116933, _116935, _116937, _116939, _117481, _117483]])]]], (831 ^ _83909) ^ [_117945, _117947, _117949, _117951, _117953, _117955, _117957, _117959, _117961, _117963] ^ [] : [p0 : [_117963, _117961, _117959, _117957, _117955, _117953, _117951, _117949, _117947, _117945], 836 ^ _83909 : [(837 ^ _83909) ^ [_118289] ^ [] : [-(p0) : -([_117963, _117961, _117959, _117957, _117955, _117953, _117951, _117949, _117947, _117945, _118289, 835 ^ [_117945, _117947, _117949, _117951, _117953, _117955, _117957, _117959, _117961, _117963, _118289]])]]], (849 ^ _83909) ^ [_118723, _118725, _118727, _118729, _118731, _118733, _118735, _118737, _118739, _118741] ^ [] : [-(p0) : -([_118741, _118739, _118737, _118735, _118733, _118731, _118729, _118727, _118725, _118723]), 854 ^ _83909 : [(855 ^ _83909) ^ [_119067] ^ [] : [p0 : [_118741, _118739, _118737, _118735, _118733, _118731, _118729, _118727, _118725, _118723, _119067, 853 ^ [_118723, _118725, _118727, _118729, _118731, _118733, _118735, _118737, _118739, _118741, _119067]]]]]]
% 12.35/13.31
% 12.35/13.31 We prove that the given matrix is valid, i.e. for
% 12.35/13.31 a given substitution it evaluates to true for all
% 12.35/13.31 interpretations. A matrix is true iff at least one
% 12.35/13.31 of its clauses is true; a clause is true iff all of
% 12.35/13.31 its elements (literals and submatrices) are true.
% 12.35/13.31
% 12.35/13.31 The proof is by contradiction:
% 12.35/13.31 Assume there is an interpretation so that the given
% 12.35/13.31 matrix evaluates to false. Then in each clause there
% 12.35/13.31 has to be at least one element that is false.
% 12.35/13.31
% 12.35/13.31 Then clause (15 ^ 0) is false if at least one of the following is false:
% 12.35/13.31 [p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ []]]
% 12.35/13.31 1 Assume p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ []] is false.
% 12.35/13.31 Then clause (849 ^ 1) under the substitution [[_118723, _118725, _118727, _118729, _118731, _118733, _118735, _118737, _118739, _118741, _119067], [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], _68736]]
% 12.35/13.31 is false if at least one of the following is false:
% 12.35/13.31 [855 : p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], _68736, 853 ^ [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], _68736]]]
% 12.35/13.31 1.1 Assume p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], _68736, 853 ^ [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], _68736]] is false.
% 12.35/13.31 Then clause (791 ^ 4) under the substitution [[_116059, _116061, _116063, _116065, _116067, _116069, _116071, _116073, _116075, _116077, _116487, _116489], [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], 853 ^ [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], _68736], _68736]]
% 12.35/13.31 is false if at least one of the following is false:
% 12.35/13.31 [p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], 792 ^ [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]
% 12.35/13.31 1.1.1 Assume p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], 792 ^ [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]] is false.
% 12.35/13.31 Then clause (13 ^ 5) under the substitution [[_84368], [792 ^ [10 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]
% 12.35/13.31 is true.
% 12.35/13.31
% 12.35/13.31 Therefore there is no interpretation that makes the
% 12.35/13.31 given matrix false. Hence the given matrix is valid.
% 12.35/13.31 q.e.d.
% 12.35/13.31 ------------------------------------------------------
% 12.35/13.31 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.bETpvBy8VW/theBenchmark.p.qmf
% 12.35/13.31 % nanoCoP-M exiting
%------------------------------------------------------------------------------