%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP107_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 07:14:06 PM UTC 2026
% Result : Theorem 7.92s 8.96s
% Output : Proof 7.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYP107_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : run_nanocopm %s %d
% 0.15/0.34 % Computer : n023.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 17:43:08 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.28/0.48 % Logic is t
% 0.28/0.48 % Designation is rigid
% 0.28/0.49 % Terms are local
% 0.28/0.49 % Domains are const
% 0.28/0.51 ------------ Start QMF file ---------------
% 0.28/0.51 %------------------------------------------------------------------------------
% 0.28/0.51 % File : SYP107_1 : TPTP v9.3.0. Released v9.3.0.
% 0.28/0.51 % Domain : Syntactic
% 0.28/0.51 % Problem : Logic KT, problem k_lin, size 10
% 0.28/0.51 % Version : Especial.
% 0.28/0.51 % English :
% 0.28/0.51 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.28/0.51 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.28/0.51 % Source : [Ste24]
% 0.28/0.51 % Names : KT/k_lin_p/10.p
% 0.28/0.51 % Status : Theorem
% 0.28/0.51 % Rating : ? v9.2.0
% 0.28/0.51 % Syntax : Number of formulae : 12 ( 0 unt; 11 typ; 0 def)
% 0.28/0.51 % Number of atoms : 286 ( 0 equ)
% 0.28/0.51 % Maximal formula atoms : 286 ( 286 avg)
% 0.28/0.51 % Number of connectives : 529 ( 90 ~; 51 |; 142 &)
% 0.28/0.51 % ( 0 <=>; 92 =>; 0 <=; 0 <~>)
% 0.28/0.51 % ( 154 {.}; 0 {#})
% 0.28/0.51 % Maximal formula depth : 23 ( 23 avg)
% 0.28/0.51 % Maximal term depth : 0 ( 0 avg)
% 0.28/0.51 % Number of types : 1 ( 0 usr)
% 0.28/0.51 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.28/0.51 % Number of predicates : 11 ( 11 usr; 11 prp; 0-0 aty)
% 0.28/0.51 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.28/0.51 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.28/0.51 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.28/0.51 % Comments :
% 0.28/0.51 %------------------------------------------------------------------------------
% 0.28/0.51 qmf(10,conjecture,(~ ( ( ( #box : ( ( ( p1 & #box : ( p1 ) & p1 ) => p2 ) | ( ~ ( p1 ) => ~ ( #box : ( p2 ) & p2 ) ) ) & #box : ( #box : ( ( ( p1 & #box : ( p1 ) & p1 ) => p2 ) ) | ( ~ ( p1 ) => ~ ( #box : ( p2 ) & p2 ) ) ) & #box : ( ( ( p1 & #box : ( p1 ) & p1 ) => p2 ) | #box : ( ( ~ ( p1 ) => ~ ( #box : ( p2 ) & p2 ) ) ) ) ) => ( #box : ( ( ( p1 & #box : ( p1 ) & p1 ) => p2 ) ) | #box : ( ( ~ ( p1 ) => ~ ( #box : ( p2 ) & p2 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p2 & #box : ( p2 ) & p2 ) => p3 ) | ( ~ ( p2 ) => ~ ( #box : ( p3 ) & p3 ) ) ) & #box : ( #box : ( ( ( p2 & #box : ( p2 ) & p2 ) => p3 ) ) | ( ~ ( p2 ) => ~ ( #box : ( p3 ) & p3 ) ) ) & #box : ( ( ( p2 & #box : ( p2 ) & p2 ) => p3 ) | #box : ( ( ~ ( p2 ) => ~ ( #box : ( p3 ) & p3 ) ) ) ) ) => ( #box : ( ( ( p2 & #box : ( p2 ) & p2 ) => p3 ) ) | #box : ( ( ~ ( p2 ) => ~ ( #box : ( p3 ) & p3 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p3 & #box : ( p3 ) & p3 ) => p4 ) | ( ~ ( p3 ) => ~ ( #box : ( p4 ) & p4 ) ) ) & #box : ( #box : ( ( ( p3 & #box : ( p3 ) & p3 ) => p4 ) ) | ( ~ ( p3 ) => ~ ( #box : ( p4 ) & p4 ) ) ) & #box : ( ( ( p3 & #box : ( p3 ) & p3 ) => p4 ) | #box : ( ( ~ ( p3 ) => ~ ( #box : ( p4 ) & p4 ) ) ) ) ) => ( #box : ( ( ( p3 & #box : ( p3 ) & p3 ) => p4 ) ) | #box : ( ( ~ ( p3 ) => ~ ( #box : ( p4 ) & p4 ) ) ) ) ) ) | #box : ( ( ( p10 & #box : ( p10 ) ) => p10 ) ) | #box : ( ( ( p10 & #box : ( p10 ) ) => p10 ) ) | ~ ( ( ( #box : ( ( ( p4 & #box : ( p4 ) & p4 ) => p5 ) | ( ~ ( p4 ) => ~ ( #box : ( p5 ) & p5 ) ) ) & #box : ( #box : ( ( ( p4 & #box : ( p4 ) & p4 ) => p5 ) ) | ( ~ ( p4 ) => ~ ( #box : ( p5 ) & p5 ) ) ) & #box : ( ( ( p4 & #box : ( p4 ) & p4 ) => p5 ) | #box : ( ( ~ ( p4 ) => ~ ( #box : ( p5 ) & p5 ) ) ) ) ) => ( #box : ( ( ( p4 & #box : ( p4 ) & p4 ) => p5 ) ) | #box : ( ( ~ ( p4 ) => ~ ( #box : ( p5 ) & p5 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p5 & #box : ( p5 ) & p5 ) => p6 ) | ( ~ ( p5 ) => ~ ( #box : ( p6 ) & p6 ) ) ) & #box : ( #box : ( ( ( p5 & #box : ( p5 ) & p5 ) => p6 ) ) | ( ~ ( p5 ) => ~ ( #box : ( p6 ) & p6 ) ) ) & #box : ( ( ( p5 & #box : ( p5 ) & p5 ) => p6 ) | #box : ( ( ~ ( p5 ) => ~ ( #box : ( p6 ) & p6 ) ) ) ) ) => ( #box : ( ( ( p5 & #box : ( p5 ) & p5 ) => p6 ) ) | #box : ( ( ~ ( p5 ) => ~ ( #box : ( p6 ) & p6 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p6 & #box : ( p6 ) & p6 ) => p7 ) | ( ~ ( p6 ) => ~ ( #box : ( p7 ) & p7 ) ) ) & #box : ( #box : ( ( ( p6 & #box : ( p6 ) & p6 ) => p7 ) ) | ( ~ ( p6 ) => ~ ( #box : ( p7 ) & p7 ) ) ) & #box : ( ( ( p6 & #box : ( p6 ) & p6 ) => p7 ) | #box : ( ( ~ ( p6 ) => ~ ( #box : ( p7 ) & p7 ) ) ) ) ) => ( #box : ( ( ( p6 & #box : ( p6 ) & p6 ) => p7 ) ) | #box : ( ( ~ ( p6 ) => ~ ( #box : ( p7 ) & p7 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p7 & #box : ( p7 ) & p7 ) => p8 ) | ( ~ ( p7 ) => ~ ( #box : ( p8 ) & p8 ) ) ) & #box : ( #box : ( ( ( p7 & #box : ( p7 ) & p7 ) => p8 ) ) | ( ~ ( p7 ) => ~ ( #box : ( p8 ) & p8 ) ) ) & #box : ( ( ( p7 & #box : ( p7 ) & p7 ) => p8 ) | #box : ( ( ~ ( p7 ) => ~ ( #box : ( p8 ) & p8 ) ) ) ) ) => ( #box : ( ( ( p7 & #box : ( p7 ) & p7 ) => p8 ) ) | #box : ( ( ~ ( p7 ) => ~ ( #box : ( p8 ) & p8 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p8 & #box : ( p8 ) & p8 ) => p9 ) | ( ~ ( p8 ) => ~ ( #box : ( p9 ) & p9 ) ) ) & #box : ( #box : ( ( ( p8 & #box : ( p8 ) & p8 ) => p9 ) ) | ( ~ ( p8 ) => ~ ( #box : ( p9 ) & p9 ) ) ) & #box : ( ( ( p8 & #box : ( p8 ) & p8 ) => p9 ) | #box : ( ( ~ ( p8 ) => ~ ( #box : ( p9 ) & p9 ) ) ) ) ) => ( #box : ( ( ( p8 & #box : ( p8 ) & p8 ) => p9 ) ) | #box : ( ( ~ ( p8 ) => ~ ( #box : ( p9 ) & p9 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p9 & #box : ( p9 ) & p9 ) => p10 ) | ( ~ ( p9 ) => ~ ( #box : ( p10 ) & p10 ) ) ) & #box : ( #box : ( ( ( p9 & #box : ( p9 ) & p9 ) => p10 ) ) | ( ~ ( p9 ) => ~ ( #box : ( p10 ) & p10 ) ) ) & #box : ( ( ( p9 & #box : ( p9 ) & p9 ) => p10 ) | #box : ( ( ~ ( p9 ) => ~ ( #box : ( p10 ) & p10 ) ) ) ) ) => ( #box : ( ( ( p9 & #box : ( p9 ) & p9 ) => p10 ) ) | #box : ( ( ~ ( p9 ) => ~ ( #box : ( p10 ) & p10 ) ) ) ) ) ) | ~ ( ( ( #box : ( ( ( p10 & #box : ( p10 ) & p10 ) => p11 ) | ( ~ ( p10 ) => ~ ( #box : ( p11 ) & p11 ) ) ) & #box : ( #box : ( ( ( p10 & #box : ( p10 ) & p10 ) => p11 ) ) | ( ~ ( p10 ) => ~ ( #box : ( p11 ) & p11 ) ) ) & #box : ( ( ( p10 & #box : ( p10 ) & p10 ) => p11 ) | #box : ( ( ~ ( p10 ) => ~ ( #box : ( p11 ) & p11 ) ) ) ) ) => ( #box : ( ( ( p10 & #box : ( p10 ) & p10 ) => p11 ) ) | #box : ( ( ~ ( p10 ) => ~ ( #box : ( p11 ) & p11 ) ) ) ) ) ) )).
% 0.28/0.51 %------------------------------------------------------------------------------
% 0.28/0.51 ------------ End QMF file ---------------
% 7.92/8.96
% 7.92/8.96 % SZS status Theorem for $/export/starexec/sandbox2/tmp/tmp.6l7Vw7XtYa/theBenchmark.p.qmf : (modal (t/const))
% 7.92/8.96 % SZS output start Proof for /export/starexec/sandbox2/tmp/tmp.6l7Vw7XtYa/theBenchmark.p.qmf
% 7.92/8.96 ------------------------------------------------------
% 7.92/8.96 Explanations for the proof presented below:
% 7.92/8.96 - equality axioms are added if required
% 7.92/8.96 - terms and variables are represented by Prolog terms
% 7.92/8.96 and Prolog variables, negation is represented by -
% 7.92/8.96 - a prefix Pre is a list of variables and constants
% 7.92/8.96 and assigned to each literal Lit, i.e. Pre:Lit
% 7.92/8.96 - clauses and (sub-)matrices have a unique label I^K:
% 7.92/8.96 or I^K^[..]:, where I is a unique number/identifier
% 7.92/8.96 and K identifies the instance of clause/matrix I
% 7.92/8.96 - I:Lit refers to literal Lit in clause number I
% 7.92/8.96 - in the matrix, I^[t1,..,tn] may represent the atom
% 7.92/8.96 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 7.92/8.96 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 7.92/8.96 the assignments X1:=t1, .., Xn:=tn (for both term
% 7.92/8.96 and prefix variables)
% 7.92/8.96
% 7.92/8.96 Proof:
% 7.92/8.96 ------
% 7.92/8.96 Translation into a non-clausal matrix:
% 7.92/8.96 [(2 ^ _75842) ^ [] ^ [] : [6 ^ _75842 : [(7 ^ _75842) ^ [] ^ [] : [-(p1) : -([5 ^ []])], (10 ^ _75842) ^ [_76184] ^ [] : [-(p1) : -([5 ^ [], _76184])], (12 ^ _75842) ^ [] ^ [] : [-(p1) : -([5 ^ []])], (14 ^ _75842) ^ [] ^ [] : [p2 : [5 ^ []]], (16 ^ _75842) ^ [] ^ [] : [p1 : [5 ^ []]], (19 ^ _75842) ^ [_76506] ^ [] : [-(p2) : -([5 ^ [], _76506])], (21 ^ _75842) ^ [] ^ [] : [-(p2) : -([5 ^ []])]], 26 ^ _75842 : [(27 ^ _75842) ^ [] ^ [] : [-(p1) : -([24 ^ [], 25 ^ []])], (30 ^ _75842) ^ [_76904] ^ [] : [-(p1) : -([24 ^ [], 25 ^ [], _76904])], (32 ^ _75842) ^ [] ^ [] : [-(p1) : -([24 ^ [], 25 ^ []])], (34 ^ _75842) ^ [] ^ [] : [p2 : [24 ^ [], 25 ^ []]], (36 ^ _75842) ^ [] ^ [] : [p1 : [24 ^ []]], (39 ^ _75842) ^ [_77228] ^ [] : [-(p2) : -([24 ^ [], _77228])], (41 ^ _75842) ^ [] ^ [] : [-(p2) : -([24 ^ []])]], 43 ^ _75842 : [(44 ^ _75842) ^ [] ^ [] : [-(p1) : -([42 ^ []])], (47 ^ _75842) ^ [_77563] ^ [] : [-(p1) : -([42 ^ [], _77563])], (49 ^ _75842) ^ [] ^ [] : [-(p1) : -([42 ^ []])], (51 ^ _75842) ^ [] ^ [] : [p2 : [42 ^ []]], (54 ^ _75842) ^ [] ^ [] : [p1 : [42 ^ [], 52 ^ []]], (57 ^ _75842) ^ [_77912] ^ [] : [-(p2) : -([42 ^ [], 52 ^ [], _77912])], (59 ^ _75842) ^ [] ^ [] : [-(p2) : -([42 ^ [], 52 ^ []])]], 79 ^ _75842 : [(80 ^ _75842) ^ [_78639] ^ [] : [-(p1) : -([_78639]), p2 : [_78639, 85 ^ [_78639]], p2 : [_78639]]], 63 ^ _75842 : [(64 ^ _75842) ^ [_78133] ^ [] : [-(p2) : -([_78133]), p1 : [_78133], p1 : [_78133, 71 ^ [_78133]], p1 : [_78133]]]], (91 ^ _75842) ^ [] ^ [] : [95 ^ _75842 : [(96 ^ _75842) ^ [] ^ [] : [-(p2) : -([94 ^ []])], (99 ^ _75842) ^ [_79318] ^ [] : [-(p2) : -([94 ^ [], _79318])], (101 ^ _75842) ^ [] ^ [] : [-(p2) : -([94 ^ []])], (103 ^ _75842) ^ [] ^ [] : [p3 : [94 ^ []]], (105 ^ _75842) ^ [] ^ [] : [p2 : [94 ^ []]], (108 ^ _75842) ^ [_79640] ^ [] : [-(p3) : -([94 ^ [], _79640])], (110 ^ _75842) ^ [] ^ [] : [-(p3) : -([94 ^ []])]], 115 ^ _75842 : [(116 ^ _75842) ^ [] ^ [] : [-(p2) : -([113 ^ [], 114 ^ []])], (119 ^ _75842) ^ [_80038] ^ [] : [-(p2) : -([113 ^ [], 114 ^ [], _80038])], (121 ^ _75842) ^ [] ^ [] : [-(p2) : -([113 ^ [], 114 ^ []])], (123 ^ _75842) ^ [] ^ [] : [p3 : [113 ^ [], 114 ^ []]], (125 ^ _75842) ^ [] ^ [] : [p2 : [113 ^ []]], (128 ^ _75842) ^ [_80362] ^ [] : [-(p3) : -([113 ^ [], _80362])], (130 ^ _75842) ^ [] ^ [] : [-(p3) : -([113 ^ []])]], 132 ^ _75842 : [(133 ^ _75842) ^ [] ^ [] : [-(p2) : -([131 ^ []])], (136 ^ _75842) ^ [_80697] ^ [] : [-(p2) : -([131 ^ [], _80697])], (138 ^ _75842) ^ [] ^ [] : [-(p2) : -([131 ^ []])], (140 ^ _75842) ^ [] ^ [] : [p3 : [131 ^ []]], (143 ^ _75842) ^ [] ^ [] : [p2 : [131 ^ [], 141 ^ []]], (146 ^ _75842) ^ [_81046] ^ [] : [-(p3) : -([131 ^ [], 141 ^ [], _81046])], (148 ^ _75842) ^ [] ^ [] : [-(p3) : -([131 ^ [], 141 ^ []])]], 168 ^ _75842 : [(169 ^ _75842) ^ [_81773] ^ [] : [-(p2) : -([_81773]), p3 : [_81773, 174 ^ [_81773]], p3 : [_81773]]], 152 ^ _75842 : [(153 ^ _75842) ^ [_81267] ^ [] : [-(p3) : -([_81267]), p2 : [_81267], p2 : [_81267, 160 ^ [_81267]], p2 : [_81267]]]], (180 ^ _75842) ^ [] ^ [] : [184 ^ _75842 : [(185 ^ _75842) ^ [] ^ [] : [-(p3) : -([183 ^ []])], (188 ^ _75842) ^ [_82452] ^ [] : [-(p3) : -([183 ^ [], _82452])], (190 ^ _75842) ^ [] ^ [] : [-(p3) : -([183 ^ []])], (192 ^ _75842) ^ [] ^ [] : [p4 : [183 ^ []]], (194 ^ _75842) ^ [] ^ [] : [p3 : [183 ^ []]], (197 ^ _75842) ^ [_82774] ^ [] : [-(p4) : -([183 ^ [], _82774])], (199 ^ _75842) ^ [] ^ [] : [-(p4) : -([183 ^ []])]], 204 ^ _75842 : [(205 ^ _75842) ^ [] ^ [] : [-(p3) : -([202 ^ [], 203 ^ []])], (208 ^ _75842) ^ [_83172] ^ [] : [-(p3) : -([202 ^ [], 203 ^ [], _83172])], (210 ^ _75842) ^ [] ^ [] : [-(p3) : -([202 ^ [], 203 ^ []])], (212 ^ _75842) ^ [] ^ [] : [p4 : [202 ^ [], 203 ^ []]], (214 ^ _75842) ^ [] ^ [] : [p3 : [202 ^ []]], (217 ^ _75842) ^ [_83496] ^ [] : [-(p4) : -([202 ^ [], _83496])], (219 ^ _75842) ^ [] ^ [] : [-(p4) : -([202 ^ []])]], 221 ^ _75842 : [(222 ^ _75842) ^ [] ^ [] : [-(p3) : -([220 ^ []])], (225 ^ _75842) ^ [_83831] ^ [] : [-(p3) : -([220 ^ [], _83831])], (227 ^ _75842) ^ [] ^ [] : [-(p3) : -([220 ^ []])], (229 ^ _75842) ^ [] ^ [] : [p4 : [220 ^ []]], (232 ^ _75842) ^ [] ^ [] : [p3 : [220 ^ [], 230 ^ []]], (235 ^ _75842) ^ [_84180] ^ [] : [-(p4) : -([220 ^ [], 230 ^ [], _84180])], (237 ^ _75842) ^ [] ^ [] : [-(p4) : -([220 ^ [], 230 ^ []])]], 257 ^ _75842 : [(258 ^ _75842) ^ [_84907] ^ [] : [-(p3) : -([_84907]), p4 : [_84907, 263 ^ [_84907]], p4 : [_84907]]], 241 ^ _75842 : [(242 ^ _75842) ^ [_84401] ^ [] : [-(p4) : -([_84401]), p3 : [_84401], p3 : [_84401, 249 ^ [_84401]], p3 : [_84401]]]], (270 ^ _75842) ^ [] ^ [] : [-(p10) : -([268 ^ []])], (273 ^ _75842) ^ [_85464] ^ [] : [-(p10) : -([268 ^ [], _85464])], (275 ^ _75842) ^ [] ^ [] : [p10 : [268 ^ []]], (278 ^ _75842) ^ [] ^ [] : [-(p10) : -([276 ^ []])], (281 ^ _75842) ^ [_85767] ^ [] : [-(p10) : -([276 ^ [], _85767])], (283 ^ _75842) ^ [] ^ [] : [p10 : [276 ^ []]], (285 ^ _75842) ^ [] ^ [] : [289 ^ _75842 : [(290 ^ _75842) ^ [] ^ [] : [-(p4) : -([288 ^ []])], (293 ^ _75842) ^ [_86192] ^ [] : [-(p4) : -([288 ^ [], _86192])], (295 ^ _75842) ^ [] ^ [] : [-(p4) : -([288 ^ []])], (297 ^ _75842) ^ [] ^ [] : [p5 : [288 ^ []]], (299 ^ _75842) ^ [] ^ [] : [p4 : [288 ^ []]], (302 ^ _75842) ^ [_86514] ^ [] : [-(p5) : -([288 ^ [], _86514])], (304 ^ _75842) ^ [] ^ [] : [-(p5) : -([288 ^ []])]], 309 ^ _75842 : [(310 ^ _75842) ^ [] ^ [] : [-(p4) : -([307 ^ [], 308 ^ []])], (313 ^ _75842) ^ [_86912] ^ [] : [-(p4) : -([307 ^ [], 308 ^ [], _86912])], (315 ^ _75842) ^ [] ^ [] : [-(p4) : -([307 ^ [], 308 ^ []])], (317 ^ _75842) ^ [] ^ [] : [p5 : [307 ^ [], 308 ^ []]], (319 ^ _75842) ^ [] ^ [] : [p4 : [307 ^ []]], (322 ^ _75842) ^ [_87236] ^ [] : [-(p5) : -([307 ^ [], _87236])], (324 ^ _75842) ^ [] ^ [] : [-(p5) : -([307 ^ []])]], 326 ^ _75842 : [(327 ^ _75842) ^ [] ^ [] : [-(p4) : -([325 ^ []])], (330 ^ _75842) ^ [_87571] ^ [] : [-(p4) : -([325 ^ [], _87571])], (332 ^ _75842) ^ [] ^ [] : [-(p4) : -([325 ^ []])], (334 ^ _75842) ^ [] ^ [] : [p5 : [325 ^ []]], (337 ^ _75842) ^ [] ^ [] : [p4 : [325 ^ [], 335 ^ []]], (340 ^ _75842) ^ [_87920] ^ [] : [-(p5) : -([325 ^ [], 335 ^ [], _87920])], (342 ^ _75842) ^ [] ^ [] : [-(p5) : -([325 ^ [], 335 ^ []])]], 362 ^ _75842 : [(363 ^ _75842) ^ [_88647] ^ [] : [-(p4) : -([_88647]), p5 : [_88647, 368 ^ [_88647]], p5 : [_88647]]], 346 ^ _75842 : [(347 ^ _75842) ^ [_88141] ^ [] : [-(p5) : -([_88141]), p4 : [_88141], p4 : [_88141, 354 ^ [_88141]], p4 : [_88141]]]], (374 ^ _75842) ^ [] ^ [] : [378 ^ _75842 : [(379 ^ _75842) ^ [] ^ [] : [-(p5) : -([377 ^ []])], (382 ^ _75842) ^ [_89326] ^ [] : [-(p5) : -([377 ^ [], _89326])], (384 ^ _75842) ^ [] ^ [] : [-(p5) : -([377 ^ []])], (386 ^ _75842) ^ [] ^ [] : [p6 : [377 ^ []]], (388 ^ _75842) ^ [] ^ [] : [p5 : [377 ^ []]], (391 ^ _75842) ^ [_89648] ^ [] : [-(p6) : -([377 ^ [], _89648])], (393 ^ _75842) ^ [] ^ [] : [-(p6) : -([377 ^ []])]], 398 ^ _75842 : [(399 ^ _75842) ^ [] ^ [] : [-(p5) : -([396 ^ [], 397 ^ []])], (402 ^ _75842) ^ [_90046] ^ [] : [-(p5) : -([396 ^ [], 397 ^ [], _90046])], (404 ^ _75842) ^ [] ^ [] : [-(p5) : -([396 ^ [], 397 ^ []])], (406 ^ _75842) ^ [] ^ [] : [p6 : [396 ^ [], 397 ^ []]], (408 ^ _75842) ^ [] ^ [] : [p5 : [396 ^ []]], (411 ^ _75842) ^ [_90370] ^ [] : [-(p6) : -([396 ^ [], _90370])], (413 ^ _75842) ^ [] ^ [] : [-(p6) : -([396 ^ []])]], 415 ^ _75842 : [(416 ^ _75842) ^ [] ^ [] : [-(p5) : -([414 ^ []])], (419 ^ _75842) ^ [_90705] ^ [] : [-(p5) : -([414 ^ [], _90705])], (421 ^ _75842) ^ [] ^ [] : [-(p5) : -([414 ^ []])], (423 ^ _75842) ^ [] ^ [] : [p6 : [414 ^ []]], (426 ^ _75842) ^ [] ^ [] : [p5 : [414 ^ [], 424 ^ []]], (429 ^ _75842) ^ [_91054] ^ [] : [-(p6) : -([414 ^ [], 424 ^ [], _91054])], (431 ^ _75842) ^ [] ^ [] : [-(p6) : -([414 ^ [], 424 ^ []])]], 451 ^ _75842 : [(452 ^ _75842) ^ [_91781] ^ [] : [-(p5) : -([_91781]), p6 : [_91781, 457 ^ [_91781]], p6 : [_91781]]], 435 ^ _75842 : [(436 ^ _75842) ^ [_91275] ^ [] : [-(p6) : -([_91275]), p5 : [_91275], p5 : [_91275, 443 ^ [_91275]], p5 : [_91275]]]], (463 ^ _75842) ^ [] ^ [] : [467 ^ _75842 : [(468 ^ _75842) ^ [] ^ [] : [-(p6) : -([466 ^ []])], (471 ^ _75842) ^ [_92460] ^ [] : [-(p6) : -([466 ^ [], _92460])], (473 ^ _75842) ^ [] ^ [] : [-(p6) : -([466 ^ []])], (475 ^ _75842) ^ [] ^ [] : [p7 : [466 ^ []]], (477 ^ _75842) ^ [] ^ [] : [p6 : [466 ^ []]], (480 ^ _75842) ^ [_92782] ^ [] : [-(p7) : -([466 ^ [], _92782])], (482 ^ _75842) ^ [] ^ [] : [-(p7) : -([466 ^ []])]], 487 ^ _75842 : [(488 ^ _75842) ^ [] ^ [] : [-(p6) : -([485 ^ [], 486 ^ []])], (491 ^ _75842) ^ [_93180] ^ [] : [-(p6) : -([485 ^ [], 486 ^ [], _93180])], (493 ^ _75842) ^ [] ^ [] : [-(p6) : -([485 ^ [], 486 ^ []])], (495 ^ _75842) ^ [] ^ [] : [p7 : [485 ^ [], 486 ^ []]], (497 ^ _75842) ^ [] ^ [] : [p6 : [485 ^ []]], (500 ^ _75842) ^ [_93504] ^ [] : [-(p7) : -([485 ^ [], _93504])], (502 ^ _75842) ^ [] ^ [] : [-(p7) : -([485 ^ []])]], 504 ^ _75842 : [(505 ^ _75842) ^ [] ^ [] : [-(p6) : -([503 ^ []])], (508 ^ _75842) ^ [_93839] ^ [] : [-(p6) : -([503 ^ [], _93839])], (510 ^ _75842) ^ [] ^ [] : [-(p6) : -([503 ^ []])], (512 ^ _75842) ^ [] ^ [] : [p7 : [503 ^ []]], (515 ^ _75842) ^ [] ^ [] : [p6 : [503 ^ [], 513 ^ []]], (518 ^ _75842) ^ [_94188] ^ [] : [-(p7) : -([503 ^ [], 513 ^ [], _94188])], (520 ^ _75842) ^ [] ^ [] : [-(p7) : -([503 ^ [], 513 ^ []])]], 540 ^ _75842 : [(541 ^ _75842) ^ [_94915] ^ [] : [-(p6) : -([_94915]), p7 : [_94915, 546 ^ [_94915]], p7 : [_94915]]], 524 ^ _75842 : [(525 ^ _75842) ^ [_94409] ^ [] : [-(p7) : -([_94409]), p6 : [_94409], p6 : [_94409, 532 ^ [_94409]], p6 : [_94409]]]], (552 ^ _75842) ^ [] ^ [] : [556 ^ _75842 : [(557 ^ _75842) ^ [] ^ [] : [-(p7) : -([555 ^ []])], (560 ^ _75842) ^ [_95594] ^ [] : [-(p7) : -([555 ^ [], _95594])], (562 ^ _75842) ^ [] ^ [] : [-(p7) : -([555 ^ []])], (564 ^ _75842) ^ [] ^ [] : [p8 : [555 ^ []]], (566 ^ _75842) ^ [] ^ [] : [p7 : [555 ^ []]], (569 ^ _75842) ^ [_95916] ^ [] : [-(p8) : -([555 ^ [], _95916])], (571 ^ _75842) ^ [] ^ [] : [-(p8) : -([555 ^ []])]], 576 ^ _75842 : [(577 ^ _75842) ^ [] ^ [] : [-(p7) : -([574 ^ [], 575 ^ []])], (580 ^ _75842) ^ [_96314] ^ [] : [-(p7) : -([574 ^ [], 575 ^ [], _96314])], (582 ^ _75842) ^ [] ^ [] : [-(p7) : -([574 ^ [], 575 ^ []])], (584 ^ _75842) ^ [] ^ [] : [p8 : [574 ^ [], 575 ^ []]], (586 ^ _75842) ^ [] ^ [] : [p7 : [574 ^ []]], (589 ^ _75842) ^ [_96638] ^ [] : [-(p8) : -([574 ^ [], _96638])], (591 ^ _75842) ^ [] ^ [] : [-(p8) : -([574 ^ []])]], 593 ^ _75842 : [(594 ^ _75842) ^ [] ^ [] : [-(p7) : -([592 ^ []])], (597 ^ _75842) ^ [_96973] ^ [] : [-(p7) : -([592 ^ [], _96973])], (599 ^ _75842) ^ [] ^ [] : [-(p7) : -([592 ^ []])], (601 ^ _75842) ^ [] ^ [] : [p8 : [592 ^ []]], (604 ^ _75842) ^ [] ^ [] : [p7 : [592 ^ [], 602 ^ []]], (607 ^ _75842) ^ [_97322] ^ [] : [-(p8) : -([592 ^ [], 602 ^ [], _97322])], (609 ^ _75842) ^ [] ^ [] : [-(p8) : -([592 ^ [], 602 ^ []])]], 629 ^ _75842 : [(630 ^ _75842) ^ [_98049] ^ [] : [-(p7) : -([_98049]), p8 : [_98049, 635 ^ [_98049]], p8 : [_98049]]], 613 ^ _75842 : [(614 ^ _75842) ^ [_97543] ^ [] : [-(p8) : -([_97543]), p7 : [_97543], p7 : [_97543, 621 ^ [_97543]], p7 : [_97543]]]], (641 ^ _75842) ^ [] ^ [] : [645 ^ _75842 : [(646 ^ _75842) ^ [] ^ [] : [-(p8) : -([644 ^ []])], (649 ^ _75842) ^ [_98728] ^ [] : [-(p8) : -([644 ^ [], _98728])], (651 ^ _75842) ^ [] ^ [] : [-(p8) : -([644 ^ []])], (653 ^ _75842) ^ [] ^ [] : [p9 : [644 ^ []]], (655 ^ _75842) ^ [] ^ [] : [p8 : [644 ^ []]], (658 ^ _75842) ^ [_99050] ^ [] : [-(p9) : -([644 ^ [], _99050])], (660 ^ _75842) ^ [] ^ [] : [-(p9) : -([644 ^ []])]], 665 ^ _75842 : [(666 ^ _75842) ^ [] ^ [] : [-(p8) : -([663 ^ [], 664 ^ []])], (669 ^ _75842) ^ [_99448] ^ [] : [-(p8) : -([663 ^ [], 664 ^ [], _99448])], (671 ^ _75842) ^ [] ^ [] : [-(p8) : -([663 ^ [], 664 ^ []])], (673 ^ _75842) ^ [] ^ [] : [p9 : [663 ^ [], 664 ^ []]], (675 ^ _75842) ^ [] ^ [] : [p8 : [663 ^ []]], (678 ^ _75842) ^ [_99772] ^ [] : [-(p9) : -([663 ^ [], _99772])], (680 ^ _75842) ^ [] ^ [] : [-(p9) : -([663 ^ []])]], 682 ^ _75842 : [(683 ^ _75842) ^ [] ^ [] : [-(p8) : -([681 ^ []])], (686 ^ _75842) ^ [_100107] ^ [] : [-(p8) : -([681 ^ [], _100107])], (688 ^ _75842) ^ [] ^ [] : [-(p8) : -([681 ^ []])], (690 ^ _75842) ^ [] ^ [] : [p9 : [681 ^ []]], (693 ^ _75842) ^ [] ^ [] : [p8 : [681 ^ [], 691 ^ []]], (696 ^ _75842) ^ [_100456] ^ [] : [-(p9) : -([681 ^ [], 691 ^ [], _100456])], (698 ^ _75842) ^ [] ^ [] : [-(p9) : -([681 ^ [], 691 ^ []])]], 718 ^ _75842 : [(719 ^ _75842) ^ [_101183] ^ [] : [-(p8) : -([_101183]), p9 : [_101183, 724 ^ [_101183]], p9 : [_101183]]], 702 ^ _75842 : [(703 ^ _75842) ^ [_100677] ^ [] : [-(p9) : -([_100677]), p8 : [_100677], p8 : [_100677, 710 ^ [_100677]], p8 : [_100677]]]], (730 ^ _75842) ^ [] ^ [] : [734 ^ _75842 : [(735 ^ _75842) ^ [] ^ [] : [-(p9) : -([733 ^ []])], (738 ^ _75842) ^ [_101862] ^ [] : [-(p9) : -([733 ^ [], _101862])], (740 ^ _75842) ^ [] ^ [] : [-(p9) : -([733 ^ []])], (742 ^ _75842) ^ [] ^ [] : [p10 : [733 ^ []]], (744 ^ _75842) ^ [] ^ [] : [p9 : [733 ^ []]], (747 ^ _75842) ^ [_102184] ^ [] : [-(p10) : -([733 ^ [], _102184])], (749 ^ _75842) ^ [] ^ [] : [-(p10) : -([733 ^ []])]], 754 ^ _75842 : [(755 ^ _75842) ^ [] ^ [] : [-(p9) : -([752 ^ [], 753 ^ []])], (758 ^ _75842) ^ [_102582] ^ [] : [-(p9) : -([752 ^ [], 753 ^ [], _102582])], (760 ^ _75842) ^ [] ^ [] : [-(p9) : -([752 ^ [], 753 ^ []])], (762 ^ _75842) ^ [] ^ [] : [p10 : [752 ^ [], 753 ^ []]], (764 ^ _75842) ^ [] ^ [] : [p9 : [752 ^ []]], (767 ^ _75842) ^ [_102906] ^ [] : [-(p10) : -([752 ^ [], _102906])], (769 ^ _75842) ^ [] ^ [] : [-(p10) : -([752 ^ []])]], 771 ^ _75842 : [(772 ^ _75842) ^ [] ^ [] : [-(p9) : -([770 ^ []])], (775 ^ _75842) ^ [_103241] ^ [] : [-(p9) : -([770 ^ [], _103241])], (777 ^ _75842) ^ [] ^ [] : [-(p9) : -([770 ^ []])], (779 ^ _75842) ^ [] ^ [] : [p10 : [770 ^ []]], (782 ^ _75842) ^ [] ^ [] : [p9 : [770 ^ [], 780 ^ []]], (785 ^ _75842) ^ [_103590] ^ [] : [-(p10) : -([770 ^ [], 780 ^ [], _103590])], (787 ^ _75842) ^ [] ^ [] : [-(p10) : -([770 ^ [], 780 ^ []])]], 807 ^ _75842 : [(808 ^ _75842) ^ [_104317] ^ [] : [-(p9) : -([_104317]), p10 : [_104317, 813 ^ [_104317]], p10 : [_104317]]], 791 ^ _75842 : [(792 ^ _75842) ^ [_103811] ^ [] : [-(p10) : -([_103811]), p9 : [_103811], p9 : [_103811, 799 ^ [_103811]], p9 : [_103811]]]], (819 ^ _75842) ^ [] ^ [] : [823 ^ _75842 : [(824 ^ _75842) ^ [] ^ [] : [-(p10) : -([822 ^ []])], (827 ^ _75842) ^ [_104973] ^ [] : [-(p10) : -([822 ^ [], _104973])], (829 ^ _75842) ^ [] ^ [] : [-(p10) : -([822 ^ []])], (831 ^ _75842) ^ [] ^ [] : [p11 : [822 ^ []]], (833 ^ _75842) ^ [] ^ [] : [p10 : [822 ^ []]], (836 ^ _75842) ^ [_105295] ^ [] : [-(p11) : -([822 ^ [], _105295])], (838 ^ _75842) ^ [] ^ [] : [-(p11) : -([822 ^ []])]], 843 ^ _75842 : [(844 ^ _75842) ^ [] ^ [] : [-(p10) : -([841 ^ [], 842 ^ []])], (847 ^ _75842) ^ [_105693] ^ [] : [-(p10) : -([841 ^ [], 842 ^ [], _105693])], (849 ^ _75842) ^ [] ^ [] : [-(p10) : -([841 ^ [], 842 ^ []])], (851 ^ _75842) ^ [] ^ [] : [p11 : [841 ^ [], 842 ^ []]], (853 ^ _75842) ^ [] ^ [] : [p10 : [841 ^ []]], (856 ^ _75842) ^ [_106017] ^ [] : [-(p11) : -([841 ^ [], _106017])], (858 ^ _75842) ^ [] ^ [] : [-(p11) : -([841 ^ []])]], 860 ^ _75842 : [(861 ^ _75842) ^ [] ^ [] : [-(p10) : -([859 ^ []])], (864 ^ _75842) ^ [_106352] ^ [] : [-(p10) : -([859 ^ [], _106352])], (866 ^ _75842) ^ [] ^ [] : [-(p10) : -([859 ^ []])], (868 ^ _75842) ^ [] ^ [] : [p11 : [859 ^ []]], (871 ^ _75842) ^ [] ^ [] : [p10 : [859 ^ [], 869 ^ []]], (874 ^ _75842) ^ [_106701] ^ [] : [-(p11) : -([859 ^ [], 869 ^ [], _106701])], (876 ^ _75842) ^ [] ^ [] : [-(p11) : -([859 ^ [], 869 ^ []])]], 896 ^ _75842 : [(897 ^ _75842) ^ [_107428] ^ [] : [-(p10) : -([_107428]), p11 : [_107428, 902 ^ [_107428]], p11 : [_107428]]], 880 ^ _75842 : [(881 ^ _75842) ^ [_106922] ^ [] : [-(p11) : -([_106922]), p10 : [_106922], p10 : [_106922, 888 ^ [_106922]], p10 : [_106922]]]]]
% 7.92/8.96
% 7.92/8.96 We prove that the given matrix is valid, i.e. for
% 7.92/8.96 a given substitution it evaluates to true for all
% 7.92/8.96 interpretations. A matrix is true iff at least one
% 7.92/8.96 of its clauses is true; a clause is true iff all of
% 7.92/8.96 its elements (literals and submatrices) are true.
% 7.92/8.96
% 7.92/8.96 The proof is by contradiction:
% 7.92/8.96 Assume there is an interpretation so that the given
% 7.92/8.96 matrix evaluates to false. Then in each clause there
% 7.92/8.96 has to be at least one element that is false.
% 7.92/8.96
% 7.92/8.96 Then clause (275 ^ 0) is false if at least one of the following is false:
% 7.92/8.96 [p10 : [268 ^ []]]
% 7.92/8.96 1 Assume p10 : [268 ^ []] is false.
% 7.92/8.96 Then clause (270 ^ 1) is true.
% 7.92/8.96
% 7.92/8.96 Therefore there is no interpretation that makes the
% 7.92/8.96 given matrix false. Hence the given matrix is valid.
% 7.92/8.96 q.e.d.
% 7.92/8.96 ------------------------------------------------------
% 7.92/8.96 % SZS output end Proof for /export/starexec/sandbox2/tmp/tmp.6l7Vw7XtYa/theBenchmark.p.qmf
% 7.92/8.96 % nanoCoP-M exiting
%------------------------------------------------------------------------------