%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP101_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n027.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 12.11s 13.15s
% Output : Proof 12.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYP101_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_nanocopm %s %d
% 0.18/0.33 % Computer : n027.cluster.edu
% 0.18/0.33 % Model : x86_64 x86_64
% 0.18/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.33 % Memory : 8042.1875MB
% 0.18/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.33 % CPULimit : 300
% 0.18/0.33 % WCLimit : 300
% 0.18/0.33 % DateTime : Mon May 4 17:37:05 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.30/0.47 % Logic is t
% 0.30/0.48 % Designation is rigid
% 0.30/0.48 % Terms are local
% 0.30/0.49 % Domains are const
% 0.30/0.50 ------------ Start QMF file ---------------
% 0.30/0.50 %------------------------------------------------------------------------------
% 0.30/0.50 % File : SYP101_1 : TPTP v9.3.0. Released v9.3.0.
% 0.30/0.50 % Domain : Syntactic
% 0.30/0.50 % Problem : Logic KT, problem k_d4, size 10
% 0.30/0.50 % Version : Especial.
% 0.30/0.50 % English :
% 0.30/0.50 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.30/0.50 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.30/0.50 % Source : [Ste24]
% 0.30/0.50 % Names : KT/k_d4_p/10.p
% 0.30/0.50 % Status : Theorem
% 0.30/0.50 % Rating : ? v9.2.0
% 0.30/0.50 % Syntax : Number of formulae : 2 ( 0 unt; 1 typ; 0 def)
% 0.30/0.50 % Number of atoms : 110 ( 0 equ)
% 0.30/0.50 % Maximal formula atoms : 110 ( 110 avg)
% 0.30/0.50 % Number of connectives : 674 ( 50 ~; 69 |; 40 &)
% 0.30/0.50 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.30/0.50 % ( 515 {.}; 0 {#})
% 0.30/0.50 % Maximal formula depth : 74 ( 74 avg)
% 0.30/0.50 % Maximal term depth : 0 ( 0 avg)
% 0.30/0.50 % Number of types : 1 ( 0 usr)
% 0.30/0.50 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.30/0.50 % Number of predicates : 2 ( 1 usr; 2 prp; 0-0 aty)
% 0.30/0.50 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.30/0.50 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.30/0.50 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.30/0.50 % Comments :
% 0.30/0.50 %------------------------------------------------------------------------------
% 0.30/0.50 qmf(10,conjecture,( #box : ( #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.30/0.50 %------------------------------------------------------------------------------
% 0.30/0.50 ------------ End QMF file ---------------
% 12.11/13.15
% 12.11/13.15 % SZS status Theorem for $/export/starexec/sandbox2/tmp/tmp.IsDEBWvIBH/theBenchmark.p.qmf : (modal (t/const))
% 12.11/13.15 % SZS output start Proof for /export/starexec/sandbox2/tmp/tmp.IsDEBWvIBH/theBenchmark.p.qmf
% 12.11/13.15 ------------------------------------------------------
% 12.11/13.15 Explanations for the proof presented below:
% 12.11/13.15 - equality axioms are added if required
% 12.11/13.15 - terms and variables are represented by Prolog terms
% 12.11/13.15 and Prolog variables, negation is represented by -
% 12.11/13.15 - a prefix Pre is a list of variables and constants
% 12.11/13.15 and assigned to each literal Lit, i.e. Pre:Lit
% 12.11/13.15 - clauses and (sub-)matrices have a unique label I^K:
% 12.11/13.15 or I^K^[..]:, where I is a unique number/identifier
% 12.11/13.15 and K identifies the instance of clause/matrix I
% 12.11/13.15 - I:Lit refers to literal Lit in clause number I
% 12.11/13.15 - in the matrix, I^[t1,..,tn] may represent the atom
% 12.11/13.15 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 12.11/13.15 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 12.11/13.15 the assignments X1:=t1, .., Xn:=tn (for both term
% 12.11/13.15 and prefix variables)
% 12.11/13.15
% 12.11/13.15 Proof:
% 12.11/13.15 ------
% 12.11/13.15 Translation into a non-clausal matrix:
% 12.11/13.15 [(13 ^ _82546) ^ [_83005] ^ [] : [-(p0) : -([1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], _83005])], (15 ^ _82546) ^ [] ^ [] : [p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ []]], (19 ^ _82546) ^ [_83229] ^ [] : [false___ : [_83229, 17 ^ [_83229]], -(false___) : -([_83229, 17 ^ [_83229]])], (26 ^ _82546) ^ [_83526] ^ [] : [p0 : [_83526, 27 ^ [_83526]], 32 ^ _82546 : [(33 ^ _82546) ^ [_83756, _83758] ^ [] : [-(p0) : -([_83526, _83758, _83756])]]], (36 ^ _82546) ^ [_83893] ^ [] : [39 ^ _82546 : [(40 ^ _82546) ^ [_84017] ^ [] : [p0 : [_83893, 37 ^ [_83893], _84017]]], 44 ^ _82546 : [(45 ^ _82546) ^ [_84183, _84185] ^ [] : [-(p0) : -([_83893, _84185, _84183, 43 ^ [_83893, _84183, _84185]])]]], (48 ^ _82546) ^ [_84332] ^ [] : [p0 : [_84332], 53 ^ _82546 : [(54 ^ _82546) ^ [_84532] ^ [] : [-(p0) : -([_84332, _84532, 52 ^ [_84332, _84532]])]]], (57 ^ _82546) ^ [_84674] ^ [] : [-(p0) : -([_84674]), 62 ^ _82546 : [(63 ^ _82546) ^ [_84874] ^ [] : [p0 : [_84674, _84874, 61 ^ [_84674, _84874]]]]], (76 ^ _82546) ^ [_85373] ^ [] : [-(p0) : -([64 ^ [], 65 ^ [], 66 ^ [], 67 ^ [], 68 ^ [], 69 ^ [], 70 ^ [], 71 ^ [], 72 ^ [], 73 ^ [], _85373])], (78 ^ _82546) ^ [] ^ [] : [p0 : [64 ^ [], 65 ^ [], 66 ^ [], 67 ^ [], 68 ^ [], 69 ^ [], 70 ^ [], 71 ^ [], 72 ^ [], 73 ^ []]], (83 ^ _82546) ^ [_85620, _85622] ^ [] : [false___ : [_85622, _85620, 81 ^ [_85620, _85622]], -(false___) : -([_85622, _85620, 81 ^ [_85620, _85622]])], (91 ^ _82546) ^ [_85956, _85958] ^ [] : [p0 : [_85958, _85956, 92 ^ [_85956, _85958]], 97 ^ _82546 : [(98 ^ _82546) ^ [_86208, _86210] ^ [] : [-(p0) : -([_85958, _85956, _86210, _86208])]]], (102 ^ _82546) ^ [_86370, _86372] ^ [] : [105 ^ _82546 : [(106 ^ _82546) ^ [_86506] ^ [] : [p0 : [_86372, _86370, 103 ^ [_86370, _86372], _86506]]], 110 ^ _82546 : [(111 ^ _82546) ^ [_86690, _86692] ^ [] : [-(p0) : -([_86372, _86370, _86692, _86690, 109 ^ [_86370, _86372, _86690, _86692]])]]], (115 ^ _82546) ^ [_86866, _86868] ^ [] : [p0 : [_86868, _86866], 120 ^ _82546 : [(121 ^ _82546) ^ [_87082] ^ [] : [-(p0) : -([_86868, _86866, _87082, 119 ^ [_86866, _86868, _87082]])]]], (125 ^ _82546) ^ [_87251, _87253] ^ [] : [-(p0) : -([_87253, _87251]), 130 ^ _82546 : [(131 ^ _82546) ^ [_87467] ^ [] : [p0 : [_87253, _87251, _87467, 129 ^ [_87251, _87253, _87467]]]]], (144 ^ _82546) ^ [_87972] ^ [] : [-(p0) : -([132 ^ [], 133 ^ [], 134 ^ [], 135 ^ [], 136 ^ [], 137 ^ [], 138 ^ [], 139 ^ [], 140 ^ [], 141 ^ [], _87972])], (146 ^ _82546) ^ [] ^ [] : [p0 : [132 ^ [], 133 ^ [], 134 ^ [], 135 ^ [], 136 ^ [], 137 ^ [], 138 ^ [], 139 ^ [], 140 ^ [], 141 ^ []]], (152 ^ _82546) ^ [_88244, _88246, _88248] ^ [] : [false___ : [_88248, _88246, _88244, 150 ^ [_88244, _88246, _88248]], -(false___) : -([_88248, _88246, _88244, 150 ^ [_88244, _88246, _88248]])], (161 ^ _82546) ^ [_88621, _88623, _88625] ^ [] : [p0 : [_88625, _88623, _88621, 162 ^ [_88621, _88623, _88625]], 167 ^ _82546 : [(168 ^ _82546) ^ [_88895, _88897] ^ [] : [-(p0) : -([_88625, _88623, _88621, _88897, _88895])]]], (173 ^ _82546) ^ [_89084, _89086, _89088] ^ [] : [176 ^ _82546 : [(177 ^ _82546) ^ [_89232] ^ [] : [p0 : [_89088, _89086, _89084, 174 ^ [_89084, _89086, _89088], _89232]]], 181 ^ _82546 : [(182 ^ _82546) ^ [_89434, _89436] ^ [] : [-(p0) : -([_89088, _89086, _89084, _89436, _89434, 180 ^ [_89084, _89086, _89088, _89434, _89436]])]]], (187 ^ _82546) ^ [_89639, _89641, _89643] ^ [] : [p0 : [_89643, _89641, _89639], 192 ^ _82546 : [(193 ^ _82546) ^ [_89871] ^ [] : [-(p0) : -([_89643, _89641, _89639, _89871, 191 ^ [_89639, _89641, _89643, _89871]])]]], (198 ^ _82546) ^ [_90069, _90071, _90073] ^ [] : [-(p0) : -([_90073, _90071, _90069]), 203 ^ _82546 : [(204 ^ _82546) ^ [_90301] ^ [] : [p0 : [_90073, _90071, _90069, _90301, 202 ^ [_90069, _90071, _90073, _90301]]]]], (217 ^ _82546) ^ [_90812] ^ [] : [-(p0) : -([205 ^ [], 206 ^ [], 207 ^ [], 208 ^ [], 209 ^ [], 210 ^ [], 211 ^ [], 212 ^ [], 213 ^ [], 214 ^ [], _90812])], (219 ^ _82546) ^ [] ^ [] : [p0 : [205 ^ [], 206 ^ [], 207 ^ [], 208 ^ [], 209 ^ [], 210 ^ [], 211 ^ [], 212 ^ [], 213 ^ [], 214 ^ []]], (226 ^ _82546) ^ [_91111, _91113, _91115, _91117] ^ [] : [false___ : [_91117, _91115, _91113, _91111, 224 ^ [_91111, _91113, _91115, _91117]], -(false___) : -([_91117, _91115, _91113, _91111, 224 ^ [_91111, _91113, _91115, _91117]])], (236 ^ _82546) ^ [_91531, _91533, _91535, _91537] ^ [] : [p0 : [_91537, _91535, _91533, _91531, 237 ^ [_91531, _91533, _91535, _91537]], 242 ^ _82546 : [(243 ^ _82546) ^ [_91827, _91829] ^ [] : [-(p0) : -([_91537, _91535, _91533, _91531, _91829, _91827])]]], (249 ^ _82546) ^ [_92045, _92047, _92049, _92051] ^ [] : [252 ^ _82546 : [(253 ^ _82546) ^ [_92205] ^ [] : [p0 : [_92051, _92049, _92047, _92045, 250 ^ [_92045, _92047, _92049, _92051], _92205]]], 257 ^ _82546 : [(258 ^ _82546) ^ [_92425, _92427] ^ [] : [-(p0) : -([_92051, _92049, _92047, _92045, _92427, _92425, 256 ^ [_92045, _92047, _92049, _92051, _92425, _92427]])]]], (264 ^ _82546) ^ [_92661, _92663, _92665, _92667] ^ [] : [p0 : [_92667, _92665, _92663, _92661], 269 ^ _82546 : [(270 ^ _82546) ^ [_92909] ^ [] : [-(p0) : -([_92667, _92665, _92663, _92661, _92909, 268 ^ [_92661, _92663, _92665, _92667, _92909]])]]], (276 ^ _82546) ^ [_93138, _93140, _93142, _93144] ^ [] : [-(p0) : -([_93144, _93142, _93140, _93138]), 281 ^ _82546 : [(282 ^ _82546) ^ [_93386] ^ [] : [p0 : [_93144, _93142, _93140, _93138, _93386, 280 ^ [_93138, _93140, _93142, _93144, _93386]]]]], (295 ^ _82546) ^ [_93903] ^ [] : [-(p0) : -([283 ^ [], 284 ^ [], 285 ^ [], 286 ^ [], 287 ^ [], 288 ^ [], 289 ^ [], 290 ^ [], 291 ^ [], 292 ^ [], _93903])], (297 ^ _82546) ^ [] ^ [] : [p0 : [283 ^ [], 284 ^ [], 285 ^ [], 286 ^ [], 287 ^ [], 288 ^ [], 289 ^ [], 290 ^ [], 291 ^ [], 292 ^ []]], (305 ^ _82546) ^ [_94231, _94233, _94235, _94237, _94239] ^ [] : [false___ : [_94239, _94237, _94235, _94233, _94231, 303 ^ [_94231, _94233, _94235, _94237, _94239]], -(false___) : -([_94239, _94237, _94235, _94233, _94231, 303 ^ [_94231, _94233, _94235, _94237, _94239]])], (316 ^ _82546) ^ [_94696, _94698, _94700, _94702, _94704] ^ [] : [p0 : [_94704, _94702, _94700, _94698, _94696, 317 ^ [_94696, _94698, _94700, _94702, _94704]], 322 ^ _82546 : [(323 ^ _82546) ^ [_95014, _95016] ^ [] : [-(p0) : -([_94704, _94702, _94700, _94698, _94696, _95016, _95014])]]], (330 ^ _82546) ^ [_95263, _95265, _95267, _95269, _95271] ^ [] : [333 ^ _82546 : [(334 ^ _82546) ^ [_95435] ^ [] : [p0 : [_95271, _95269, _95267, _95265, _95263, 331 ^ [_95263, _95265, _95267, _95269, _95271], _95435]]], 338 ^ _82546 : [(339 ^ _82546) ^ [_95673, _95675] ^ [] : [-(p0) : -([_95271, _95269, _95267, _95265, _95263, _95675, _95673, 337 ^ [_95263, _95265, _95267, _95269, _95271, _95673, _95675]])]]], (346 ^ _82546) ^ [_95942, _95944, _95946, _95948, _95950] ^ [] : [p0 : [_95950, _95948, _95946, _95944, _95942], 351 ^ _82546 : [(352 ^ _82546) ^ [_96206] ^ [] : [-(p0) : -([_95950, _95948, _95946, _95944, _95942, _96206, 350 ^ [_95942, _95944, _95946, _95948, _95950, _96206]])]]], (359 ^ _82546) ^ [_96468, _96470, _96472, _96474, _96476] ^ [] : [-(p0) : -([_96476, _96474, _96472, _96470, _96468]), 364 ^ _82546 : [(365 ^ _82546) ^ [_96732] ^ [] : [p0 : [_96476, _96474, _96472, _96470, _96468, _96732, 363 ^ [_96468, _96470, _96472, _96474, _96476, _96732]]]]], (378 ^ _82546) ^ [_97255] ^ [] : [-(p0) : -([366 ^ [], 367 ^ [], 368 ^ [], 369 ^ [], 370 ^ [], 371 ^ [], 372 ^ [], 373 ^ [], 374 ^ [], 375 ^ [], _97255])], (380 ^ _82546) ^ [] ^ [] : [p0 : [366 ^ [], 367 ^ [], 368 ^ [], 369 ^ [], 370 ^ [], 371 ^ [], 372 ^ [], 373 ^ [], 374 ^ [], 375 ^ []]], (389 ^ _82546) ^ [_97614, _97616, _97618, _97620, _97622, _97624] ^ [] : [false___ : [_97624, _97622, _97620, _97618, _97616, _97614, 387 ^ [_97614, _97616, _97618, _97620, _97622, _97624]], -(false___) : -([_97624, _97622, _97620, _97618, _97616, _97614, 387 ^ [_97614, _97616, _97618, _97620, _97622, _97624]])], (401 ^ _82546) ^ [_98126, _98128, _98130, _98132, _98134, _98136] ^ [] : [p0 : [_98136, _98134, _98132, _98130, _98128, _98126, 402 ^ [_98126, _98128, _98130, _98132, _98134, _98136]], 407 ^ _82546 : [(408 ^ _82546) ^ [_98466, _98468] ^ [] : [-(p0) : -([_98136, _98134, _98132, _98130, _98128, _98126, _98468, _98466])]]], (416 ^ _82546) ^ [_98748, _98750, _98752, _98754, _98756, _98758] ^ [] : [419 ^ _82546 : [(420 ^ _82546) ^ [_98932] ^ [] : [p0 : [_98758, _98756, _98754, _98752, _98750, _98748, 417 ^ [_98748, _98750, _98752, _98754, _98756, _98758], _98932]]], 424 ^ _82546 : [(425 ^ _82546) ^ [_99188, _99190] ^ [] : [-(p0) : -([_98758, _98756, _98754, _98752, _98750, _98748, _99190, _99188, 423 ^ [_98748, _98750, _98752, _98754, _98756, _98758, _99188, _99190]])]]], (433 ^ _82546) ^ [_99492, _99494, _99496, _99498, _99500, _99502] ^ [] : [p0 : [_99502, _99500, _99498, _99496, _99494, _99492], 438 ^ _82546 : [(439 ^ _82546) ^ [_99772] ^ [] : [-(p0) : -([_99502, _99500, _99498, _99496, _99494, _99492, _99772, 437 ^ [_99492, _99494, _99496, _99498, _99500, _99502, _99772]])]]], (447 ^ _82546) ^ [_100069, _100071, _100073, _100075, _100077, _100079] ^ [] : [-(p0) : -([_100079, _100077, _100075, _100073, _100071, _100069]), 452 ^ _82546 : [(453 ^ _82546) ^ [_100349] ^ [] : [p0 : [_100079, _100077, _100075, _100073, _100071, _100069, _100349, 451 ^ [_100069, _100071, _100073, _100075, _100077, _100079, _100349]]]]], (466 ^ _82546) ^ [_100878] ^ [] : [-(p0) : -([454 ^ [], 455 ^ [], 456 ^ [], 457 ^ [], 458 ^ [], 459 ^ [], 460 ^ [], 461 ^ [], 462 ^ [], 463 ^ [], _100878])], (468 ^ _82546) ^ [] ^ [] : [p0 : [454 ^ [], 455 ^ [], 456 ^ [], 457 ^ [], 458 ^ [], 459 ^ [], 460 ^ [], 461 ^ [], 462 ^ [], 463 ^ []]], (478 ^ _82546) ^ [_101270, _101272, _101274, _101276, _101278, _101280, _101282] ^ [] : [false___ : [_101282, _101280, _101278, _101276, _101274, _101272, _101270, 476 ^ [_101270, _101272, _101274, _101276, _101278, _101280, _101282]], -(false___) : -([_101282, _101280, _101278, _101276, _101274, _101272, _101270, 476 ^ [_101270, _101272, _101274, _101276, _101278, _101280, _101282]])], (491 ^ _82546) ^ [_101831, _101833, _101835, _101837, _101839, _101841, _101843] ^ [] : [p0 : [_101843, _101841, _101839, _101837, _101835, _101833, _101831, 492 ^ [_101831, _101833, _101835, _101837, _101839, _101841, _101843]], 497 ^ _82546 : [(498 ^ _82546) ^ [_102193, _102195] ^ [] : [-(p0) : -([_101843, _101841, _101839, _101837, _101835, _101833, _101831, _102195, _102193])]]], (507 ^ _82546) ^ [_102510, _102512, _102514, _102516, _102518, _102520, _102522] ^ [] : [510 ^ _82546 : [(511 ^ _82546) ^ [_102706] ^ [] : [p0 : [_102522, _102520, _102518, _102516, _102514, _102512, _102510, 508 ^ [_102510, _102512, _102514, _102516, _102518, _102520, _102522], _102706]]], 515 ^ _82546 : [(516 ^ _82546) ^ [_102980, _102982] ^ [] : [-(p0) : -([_102522, _102520, _102518, _102516, _102514, _102512, _102510, _102982, _102980, 514 ^ [_102510, _102512, _102514, _102516, _102518, _102520, _102522, _102980, _102982]])]]], (525 ^ _82546) ^ [_103321, _103323, _103325, _103327, _103329, _103331, _103333] ^ [] : [p0 : [_103333, _103331, _103329, _103327, _103325, _103323, _103321], 530 ^ _82546 : [(531 ^ _82546) ^ [_103617] ^ [] : [-(p0) : -([_103333, _103331, _103329, _103327, _103325, _103323, _103321, _103617, 529 ^ [_103321, _103323, _103325, _103327, _103329, _103331, _103333, _103617]])]]], (540 ^ _82546) ^ [_103951, _103953, _103955, _103957, _103959, _103961, _103963] ^ [] : [-(p0) : -([_103963, _103961, _103959, _103957, _103955, _103953, _103951]), 545 ^ _82546 : [(546 ^ _82546) ^ [_104247] ^ [] : [p0 : [_103963, _103961, _103959, _103957, _103955, _103953, _103951, _104247, 544 ^ [_103951, _103953, _103955, _103957, _103959, _103961, _103963, _104247]]]]], (559 ^ _82546) ^ [_104782] ^ [] : [-(p0) : -([547 ^ [], 548 ^ [], 549 ^ [], 550 ^ [], 551 ^ [], 552 ^ [], 553 ^ [], 554 ^ [], 555 ^ [], 556 ^ [], _104782])], (561 ^ _82546) ^ [] ^ [] : [p0 : [547 ^ [], 548 ^ [], 549 ^ [], 550 ^ [], 551 ^ [], 552 ^ [], 553 ^ [], 554 ^ [], 555 ^ [], 556 ^ []]], (572 ^ _82546) ^ [_105209, _105211, _105213, _105215, _105217, _105219, _105221, _105223] ^ [] : [false___ : [_105223, _105221, _105219, _105217, _105215, _105213, _105211, _105209, 570 ^ [_105209, _105211, _105213, _105215, _105217, _105219, _105221, _105223]], -(false___) : -([_105223, _105221, _105219, _105217, _105215, _105213, _105211, _105209, 570 ^ [_105209, _105211, _105213, _105215, _105217, _105219, _105221, _105223]])], (586 ^ _82546) ^ [_105821, _105823, _105825, _105827, _105829, _105831, _105833, _105835] ^ [] : [p0 : [_105835, _105833, _105831, _105829, _105827, _105825, _105823, _105821, 587 ^ [_105821, _105823, _105825, _105827, _105829, _105831, _105833, _105835]], 592 ^ _82546 : [(593 ^ _82546) ^ [_106205, _106207] ^ [] : [-(p0) : -([_105835, _105833, _105831, _105829, _105827, _105825, _105823, _105821, _106207, _106205])]]], (603 ^ _82546) ^ [_106559, _106561, _106563, _106565, _106567, _106569, _106571, _106573] ^ [] : [606 ^ _82546 : [(607 ^ _82546) ^ [_106767] ^ [] : [p0 : [_106573, _106571, _106569, _106567, _106565, _106563, _106561, _106559, 604 ^ [_106559, _106561, _106563, _106565, _106567, _106569, _106571, _106573], _106767]]], 611 ^ _82546 : [(612 ^ _82546) ^ [_107059, _107061] ^ [] : [-(p0) : -([_106573, _106571, _106569, _106567, _106565, _106563, _106561, _106559, _107061, _107059, 610 ^ [_106559, _106561, _106563, _106565, _106567, _106569, _106571, _106573, _107059, _107061]])]]], (622 ^ _82546) ^ [_107439, _107441, _107443, _107445, _107447, _107449, _107451, _107453] ^ [] : [p0 : [_107453, _107451, _107449, _107447, _107445, _107443, _107441, _107439], 627 ^ _82546 : [(628 ^ _82546) ^ [_107751] ^ [] : [-(p0) : -([_107453, _107451, _107449, _107447, _107445, _107443, _107441, _107439, _107751, 626 ^ [_107439, _107441, _107443, _107445, _107447, _107449, _107451, _107453, _107751]])]]], (638 ^ _82546) ^ [_108124, _108126, _108128, _108130, _108132, _108134, _108136, _108138] ^ [] : [-(p0) : -([_108138, _108136, _108134, _108132, _108130, _108128, _108126, _108124]), 643 ^ _82546 : [(644 ^ _82546) ^ [_108436] ^ [] : [p0 : [_108138, _108136, _108134, _108132, _108130, _108128, _108126, _108124, _108436, 642 ^ [_108124, _108126, _108128, _108130, _108132, _108134, _108136, _108138, _108436]]]]], (657 ^ _82546) ^ [_108977] ^ [] : [-(p0) : -([645 ^ [], 646 ^ [], 647 ^ [], 648 ^ [], 649 ^ [], 650 ^ [], 651 ^ [], 652 ^ [], 653 ^ [], 654 ^ [], _108977])], (659 ^ _82546) ^ [] ^ [] : [p0 : [645 ^ [], 646 ^ [], 647 ^ [], 648 ^ [], 649 ^ [], 650 ^ [], 651 ^ [], 652 ^ [], 653 ^ [], 654 ^ []]], (671 ^ _82546) ^ [_109441, _109443, _109445, _109447, _109449, _109451, _109453, _109455, _109457] ^ [] : [false___ : [_109457, _109455, _109453, _109451, _109449, _109447, _109445, _109443, _109441, 669 ^ [_109441, _109443, _109445, _109447, _109449, _109451, _109453, _109455, _109457]], -(false___) : -([_109457, _109455, _109453, _109451, _109449, _109447, _109445, _109443, _109441, 669 ^ [_109441, _109443, _109445, _109447, _109449, _109451, _109453, _109455, _109457]])], (686 ^ _82546) ^ [_110106, _110108, _110110, _110112, _110114, _110116, _110118, _110120, _110122] ^ [] : [p0 : [_110122, _110120, _110118, _110116, _110114, _110112, _110110, _110108, _110106, 687 ^ [_110106, _110108, _110110, _110112, _110114, _110116, _110118, _110120, _110122]], 692 ^ _82546 : [(693 ^ _82546) ^ [_110512, _110514] ^ [] : [-(p0) : -([_110122, _110120, _110118, _110116, _110114, _110112, _110110, _110108, _110106, _110514, _110512])]]], (704 ^ _82546) ^ [_110905, _110907, _110909, _110911, _110913, _110915, _110917, _110919, _110921] ^ [] : [707 ^ _82546 : [(708 ^ _82546) ^ [_111125] ^ [] : [p0 : [_110921, _110919, _110917, _110915, _110913, _110911, _110909, _110907, _110905, 705 ^ [_110905, _110907, _110909, _110911, _110913, _110915, _110917, _110919, _110921], _111125]]], 712 ^ _82546 : [(713 ^ _82546) ^ [_111435, _111437] ^ [] : [-(p0) : -([_110921, _110919, _110917, _110915, _110913, _110911, _110909, _110907, _110905, _111437, _111435, 711 ^ [_110905, _110907, _110909, _110911, _110913, _110915, _110917, _110919, _110921, _111435, _111437]])]]], (724 ^ _82546) ^ [_111856, _111858, _111860, _111862, _111864, _111866, _111868, _111870, _111872] ^ [] : [p0 : [_111872, _111870, _111868, _111866, _111864, _111862, _111860, _111858, _111856], 729 ^ _82546 : [(730 ^ _82546) ^ [_112184] ^ [] : [-(p0) : -([_111872, _111870, _111868, _111866, _111864, _111862, _111860, _111858, _111856, _112184, 728 ^ [_111856, _111858, _111860, _111862, _111864, _111866, _111868, _111870, _111872, _112184]])]]], (741 ^ _82546) ^ [_112598, _112600, _112602, _112604, _112606, _112608, _112610, _112612, _112614] ^ [] : [-(p0) : -([_112614, _112612, _112610, _112608, _112606, _112604, _112602, _112600, _112598]), 746 ^ _82546 : [(747 ^ _82546) ^ [_112926] ^ [] : [p0 : [_112614, _112612, _112610, _112608, _112606, _112604, _112602, _112600, _112598, _112926, 745 ^ [_112598, _112600, _112602, _112604, _112606, _112608, _112610, _112612, _112614, _112926]]]]], (760 ^ _82546) ^ [_113473] ^ [] : [-(p0) : -([748 ^ [], 749 ^ [], 750 ^ [], 751 ^ [], 752 ^ [], 753 ^ [], 754 ^ [], 755 ^ [], 756 ^ [], 757 ^ [], _113473])], (762 ^ _82546) ^ [] ^ [] : [p0 : [748 ^ [], 749 ^ [], 750 ^ [], 751 ^ [], 752 ^ [], 753 ^ [], 754 ^ [], 755 ^ [], 756 ^ [], 757 ^ []]], (775 ^ _82546) ^ [_113976, _113978, _113980, _113982, _113984, _113986, _113988, _113990, _113992, _113994] ^ [] : [false___ : [_113994, _113992, _113990, _113988, _113986, _113984, _113982, _113980, _113978, _113976, 773 ^ [_113976, _113978, _113980, _113982, _113984, _113986, _113988, _113990, _113992, _113994]], -(false___) : -([_113994, _113992, _113990, _113988, _113986, _113984, _113982, _113980, _113978, _113976, 773 ^ [_113976, _113978, _113980, _113982, _113984, _113986, _113988, _113990, _113992, _113994]])], (791 ^ _82546) ^ [_114696, _114698, _114700, _114702, _114704, _114706, _114708, _114710, _114712, _114714] ^ [] : [p0 : [_114714, _114712, _114710, _114708, _114706, _114704, _114702, _114700, _114698, _114696, 792 ^ [_114696, _114698, _114700, _114702, _114704, _114706, _114708, _114710, _114712, _114714]], 797 ^ _82546 : [(798 ^ _82546) ^ [_115124, _115126] ^ [] : [-(p0) : -([_114714, _114712, _114710, _114708, _114706, _114704, _114702, _114700, _114698, _114696, _115126, _115124])]]], (810 ^ _82546) ^ [_115558, _115560, _115562, _115564, _115566, _115568, _115570, _115572, _115574, _115576] ^ [] : [813 ^ _82546 : [(814 ^ _82546) ^ [_115790] ^ [] : [p0 : [_115576, _115574, _115572, _115570, _115568, _115566, _115564, _115562, _115560, _115558, 811 ^ [_115558, _115560, _115562, _115564, _115566, _115568, _115570, _115572, _115574, _115576], _115790]]], 818 ^ _82546 : [(819 ^ _82546) ^ [_116118, _116120] ^ [] : [-(p0) : -([_115576, _115574, _115572, _115570, _115568, _115566, _115564, _115562, _115560, _115558, _116120, _116118, 817 ^ [_115558, _115560, _115562, _115564, _115566, _115568, _115570, _115572, _115574, _115576, _116118, _116120]])]]], (831 ^ _82546) ^ [_116582, _116584, _116586, _116588, _116590, _116592, _116594, _116596, _116598, _116600] ^ [] : [p0 : [_116600, _116598, _116596, _116594, _116592, _116590, _116588, _116586, _116584, _116582], 836 ^ _82546 : [(837 ^ _82546) ^ [_116926] ^ [] : [-(p0) : -([_116600, _116598, _116596, _116594, _116592, _116590, _116588, _116586, _116584, _116582, _116926, 835 ^ [_116582, _116584, _116586, _116588, _116590, _116592, _116594, _116596, _116598, _116600, _116926]])]]], (849 ^ _82546) ^ [_117360, _117362, _117364, _117366, _117368, _117370, _117372, _117374, _117376, _117378] ^ [] : [-(p0) : -([_117378, _117376, _117374, _117372, _117370, _117368, _117366, _117364, _117362, _117360]), 854 ^ _82546 : [(855 ^ _82546) ^ [_117704] ^ [] : [p0 : [_117378, _117376, _117374, _117372, _117370, _117368, _117366, _117364, _117362, _117360, _117704, 853 ^ [_117360, _117362, _117364, _117366, _117368, _117370, _117372, _117374, _117376, _117378, _117704]]]]]]
% 12.11/13.16
% 12.11/13.16 We prove that the given matrix is valid, i.e. for
% 12.11/13.16 a given substitution it evaluates to true for all
% 12.11/13.16 interpretations. A matrix is true iff at least one
% 12.11/13.16 of its clauses is true; a clause is true iff all of
% 12.11/13.16 its elements (literals and submatrices) are true.
% 12.11/13.16
% 12.11/13.16 The proof is by contradiction:
% 12.11/13.16 Assume there is an interpretation so that the given
% 12.11/13.16 matrix evaluates to false. Then in each clause there
% 12.11/13.16 has to be at least one element that is false.
% 12.11/13.16
% 12.11/13.16 Then clause (15 ^ 0) is false if at least one of the following is false:
% 12.11/13.16 [p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ []]]
% 12.11/13.16 1 Assume p0 : [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], []] is false.
% 12.11/13.16 Then clause (13 ^ 1) under the substitution [[_83005], [[]]]
% 12.11/13.16 is true.
% 12.11/13.16
% 12.11/13.16 Therefore there is no interpretation that makes the
% 12.11/13.16 given matrix false. Hence the given matrix is valid.
% 12.11/13.16 q.e.d.
% 12.11/13.16 ------------------------------------------------------
% 12.11/13.16 % SZS output end Proof for /export/starexec/sandbox2/tmp/tmp.IsDEBWvIBH/theBenchmark.p.qmf
% 12.11/13.16 % nanoCoP-M exiting
%------------------------------------------------------------------------------