%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYP089_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n003.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 7.92s 8.99s
% Output : Proof 7.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYP089_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : run_nanocopm %s %d
% 0.15/0.32 % Computer : n003.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 17:24:56 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.28/0.46 % Logic is d
% 0.28/0.46 % Designation is rigid
% 0.28/0.47 % Terms are local
% 0.28/0.47 % Domains are const
% 0.28/0.48 ------------ Start QMF file ---------------
% 0.28/0.49 %------------------------------------------------------------------------------
% 0.28/0.49 % File : SYP089_1 : TPTP v9.3.0. Released v9.3.0.
% 0.28/0.49 % Domain : Syntactic
% 0.28/0.49 % Problem : Logic KD, problem k_lin, size 10
% 0.28/0.49 % Version : Especial.
% 0.28/0.49 % English :
% 0.28/0.49 % Refs : [BHS98] Balsiger et al. (1998), Logics Workbench 1.0
% 0.28/0.49 % : [Ste24] Steen (2024), Email to Geoff Sutcliffe
% 0.28/0.49 % Source : [Ste24]
% 0.28/0.49 % Names : KD/k_lin_p/10.p
% 0.28/0.49 % Status : Theorem
% 0.28/0.49 % Rating : ? v9.2.0
% 0.28/0.49 % Syntax : Number of formulae : 12 ( 0 unt; 11 typ; 0 def)
% 0.28/0.49 % Number of atoms : 286 ( 0 equ)
% 0.28/0.49 % Maximal formula atoms : 286 ( 286 avg)
% 0.28/0.49 % Number of connectives : 529 ( 90 ~; 51 |; 142 &)
% 0.28/0.49 % ( 0 <=>; 92 =>; 0 <=; 0 <~>)
% 0.28/0.49 % ( 154 {.}; 0 {#})
% 0.28/0.49 % Maximal formula depth : 23 ( 23 avg)
% 0.28/0.49 % Maximal term depth : 0 ( 0 avg)
% 0.28/0.49 % Number of types : 1 ( 0 usr)
% 0.28/0.49 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.28/0.49 % Number of predicates : 11 ( 11 usr; 11 prp; 0-0 aty)
% 0.28/0.49 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.28/0.49 % Number of variables : 0 ( 0 !; 0 ?; 0 :)
% 0.28/0.49 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.28/0.49 % Comments :
% 0.28/0.49 %------------------------------------------------------------------------------
% 0.28/0.49 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.49 %------------------------------------------------------------------------------
% 0.28/0.49 ------------ End QMF file ---------------
% 7.92/8.99
% 7.92/8.99 % SZS status Theorem for $/export/starexec/sandbox2/tmp/tmp.4EL7XcyZeF/theBenchmark.p.qmf : (modal (d/const))
% 7.92/8.99 % SZS output start Proof for /export/starexec/sandbox2/tmp/tmp.4EL7XcyZeF/theBenchmark.p.qmf
% 7.92/8.99 ------------------------------------------------------
% 7.92/8.99 Explanations for the proof presented below:
% 7.92/8.99 - equality axioms are added if required
% 7.92/8.99 - terms and variables are represented by Prolog terms
% 7.92/8.99 and Prolog variables, negation is represented by -
% 7.92/8.99 - a prefix Pre is a list of variables and constants
% 7.92/8.99 and assigned to each literal Lit, i.e. Pre:Lit
% 7.92/8.99 - clauses and (sub-)matrices have a unique label I^K:
% 7.92/8.99 or I^K^[..]:, where I is a unique number/identifier
% 7.92/8.99 and K identifies the instance of clause/matrix I
% 7.92/8.99 - I:Lit refers to literal Lit in clause number I
% 7.92/8.99 - in the matrix, I^[t1,..,tn] may represent the atom
% 7.92/8.99 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 7.92/8.99 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 7.92/8.99 the assignments X1:=t1, .., Xn:=tn (for both term
% 7.92/8.99 and prefix variables)
% 7.92/8.99
% 7.92/8.99 Proof:
% 7.92/8.99 ------
% 7.92/8.99 Translation into a non-clausal matrix:
% 7.92/8.99 [(2 ^ _75840) ^ [] ^ [] : [6 ^ _75840 : [(7 ^ _75840) ^ [] ^ [] : [-(p1) : -([5 ^ []])], (10 ^ _75840) ^ [_76182] ^ [] : [-(p1) : -([5 ^ [], _76182])], (12 ^ _75840) ^ [] ^ [] : [-(p1) : -([5 ^ []])], (14 ^ _75840) ^ [] ^ [] : [p2 : [5 ^ []]], (16 ^ _75840) ^ [] ^ [] : [p1 : [5 ^ []]], (19 ^ _75840) ^ [_76504] ^ [] : [-(p2) : -([5 ^ [], _76504])], (21 ^ _75840) ^ [] ^ [] : [-(p2) : -([5 ^ []])]], 26 ^ _75840 : [(27 ^ _75840) ^ [] ^ [] : [-(p1) : -([24 ^ [], 25 ^ []])], (30 ^ _75840) ^ [_76902] ^ [] : [-(p1) : -([24 ^ [], 25 ^ [], _76902])], (32 ^ _75840) ^ [] ^ [] : [-(p1) : -([24 ^ [], 25 ^ []])], (34 ^ _75840) ^ [] ^ [] : [p2 : [24 ^ [], 25 ^ []]], (36 ^ _75840) ^ [] ^ [] : [p1 : [24 ^ []]], (39 ^ _75840) ^ [_77226] ^ [] : [-(p2) : -([24 ^ [], _77226])], (41 ^ _75840) ^ [] ^ [] : [-(p2) : -([24 ^ []])]], 43 ^ _75840 : [(44 ^ _75840) ^ [] ^ [] : [-(p1) : -([42 ^ []])], (47 ^ _75840) ^ [_77561] ^ [] : [-(p1) : -([42 ^ [], _77561])], (49 ^ _75840) ^ [] ^ [] : [-(p1) : -([42 ^ []])], (51 ^ _75840) ^ [] ^ [] : [p2 : [42 ^ []]], (54 ^ _75840) ^ [] ^ [] : [p1 : [42 ^ [], 52 ^ []]], (57 ^ _75840) ^ [_77910] ^ [] : [-(p2) : -([42 ^ [], 52 ^ [], _77910])], (59 ^ _75840) ^ [] ^ [] : [-(p2) : -([42 ^ [], 52 ^ []])]], 79 ^ _75840 : [(80 ^ _75840) ^ [_78637] ^ [] : [-(p1) : -([_78637]), p2 : [_78637, 85 ^ [_78637]], p2 : [_78637]]], 63 ^ _75840 : [(64 ^ _75840) ^ [_78131] ^ [] : [-(p2) : -([_78131]), p1 : [_78131], p1 : [_78131, 71 ^ [_78131]], p1 : [_78131]]]], (91 ^ _75840) ^ [] ^ [] : [95 ^ _75840 : [(96 ^ _75840) ^ [] ^ [] : [-(p2) : -([94 ^ []])], (99 ^ _75840) ^ [_79316] ^ [] : [-(p2) : -([94 ^ [], _79316])], (101 ^ _75840) ^ [] ^ [] : [-(p2) : -([94 ^ []])], (103 ^ _75840) ^ [] ^ [] : [p3 : [94 ^ []]], (105 ^ _75840) ^ [] ^ [] : [p2 : [94 ^ []]], (108 ^ _75840) ^ [_79638] ^ [] : [-(p3) : -([94 ^ [], _79638])], (110 ^ _75840) ^ [] ^ [] : [-(p3) : -([94 ^ []])]], 115 ^ _75840 : [(116 ^ _75840) ^ [] ^ [] : [-(p2) : -([113 ^ [], 114 ^ []])], (119 ^ _75840) ^ [_80036] ^ [] : [-(p2) : -([113 ^ [], 114 ^ [], _80036])], (121 ^ _75840) ^ [] ^ [] : [-(p2) : -([113 ^ [], 114 ^ []])], (123 ^ _75840) ^ [] ^ [] : [p3 : [113 ^ [], 114 ^ []]], (125 ^ _75840) ^ [] ^ [] : [p2 : [113 ^ []]], (128 ^ _75840) ^ [_80360] ^ [] : [-(p3) : -([113 ^ [], _80360])], (130 ^ _75840) ^ [] ^ [] : [-(p3) : -([113 ^ []])]], 132 ^ _75840 : [(133 ^ _75840) ^ [] ^ [] : [-(p2) : -([131 ^ []])], (136 ^ _75840) ^ [_80695] ^ [] : [-(p2) : -([131 ^ [], _80695])], (138 ^ _75840) ^ [] ^ [] : [-(p2) : -([131 ^ []])], (140 ^ _75840) ^ [] ^ [] : [p3 : [131 ^ []]], (143 ^ _75840) ^ [] ^ [] : [p2 : [131 ^ [], 141 ^ []]], (146 ^ _75840) ^ [_81044] ^ [] : [-(p3) : -([131 ^ [], 141 ^ [], _81044])], (148 ^ _75840) ^ [] ^ [] : [-(p3) : -([131 ^ [], 141 ^ []])]], 168 ^ _75840 : [(169 ^ _75840) ^ [_81771] ^ [] : [-(p2) : -([_81771]), p3 : [_81771, 174 ^ [_81771]], p3 : [_81771]]], 152 ^ _75840 : [(153 ^ _75840) ^ [_81265] ^ [] : [-(p3) : -([_81265]), p2 : [_81265], p2 : [_81265, 160 ^ [_81265]], p2 : [_81265]]]], (180 ^ _75840) ^ [] ^ [] : [184 ^ _75840 : [(185 ^ _75840) ^ [] ^ [] : [-(p3) : -([183 ^ []])], (188 ^ _75840) ^ [_82450] ^ [] : [-(p3) : -([183 ^ [], _82450])], (190 ^ _75840) ^ [] ^ [] : [-(p3) : -([183 ^ []])], (192 ^ _75840) ^ [] ^ [] : [p4 : [183 ^ []]], (194 ^ _75840) ^ [] ^ [] : [p3 : [183 ^ []]], (197 ^ _75840) ^ [_82772] ^ [] : [-(p4) : -([183 ^ [], _82772])], (199 ^ _75840) ^ [] ^ [] : [-(p4) : -([183 ^ []])]], 204 ^ _75840 : [(205 ^ _75840) ^ [] ^ [] : [-(p3) : -([202 ^ [], 203 ^ []])], (208 ^ _75840) ^ [_83170] ^ [] : [-(p3) : -([202 ^ [], 203 ^ [], _83170])], (210 ^ _75840) ^ [] ^ [] : [-(p3) : -([202 ^ [], 203 ^ []])], (212 ^ _75840) ^ [] ^ [] : [p4 : [202 ^ [], 203 ^ []]], (214 ^ _75840) ^ [] ^ [] : [p3 : [202 ^ []]], (217 ^ _75840) ^ [_83494] ^ [] : [-(p4) : -([202 ^ [], _83494])], (219 ^ _75840) ^ [] ^ [] : [-(p4) : -([202 ^ []])]], 221 ^ _75840 : [(222 ^ _75840) ^ [] ^ [] : [-(p3) : -([220 ^ []])], (225 ^ _75840) ^ [_83829] ^ [] : [-(p3) : -([220 ^ [], _83829])], (227 ^ _75840) ^ [] ^ [] : [-(p3) : -([220 ^ []])], (229 ^ _75840) ^ [] ^ [] : [p4 : [220 ^ []]], (232 ^ _75840) ^ [] ^ [] : [p3 : [220 ^ [], 230 ^ []]], (235 ^ _75840) ^ [_84178] ^ [] : [-(p4) : -([220 ^ [], 230 ^ [], _84178])], (237 ^ _75840) ^ [] ^ [] : [-(p4) : -([220 ^ [], 230 ^ []])]], 257 ^ _75840 : [(258 ^ _75840) ^ [_84905] ^ [] : [-(p3) : -([_84905]), p4 : [_84905, 263 ^ [_84905]], p4 : [_84905]]], 241 ^ _75840 : [(242 ^ _75840) ^ [_84399] ^ [] : [-(p4) : -([_84399]), p3 : [_84399], p3 : [_84399, 249 ^ [_84399]], p3 : [_84399]]]], (270 ^ _75840) ^ [] ^ [] : [-(p10) : -([268 ^ []])], (273 ^ _75840) ^ [_85462] ^ [] : [-(p10) : -([268 ^ [], _85462])], (275 ^ _75840) ^ [] ^ [] : [p10 : [268 ^ []]], (278 ^ _75840) ^ [] ^ [] : [-(p10) : -([276 ^ []])], (281 ^ _75840) ^ [_85765] ^ [] : [-(p10) : -([276 ^ [], _85765])], (283 ^ _75840) ^ [] ^ [] : [p10 : [276 ^ []]], (285 ^ _75840) ^ [] ^ [] : [289 ^ _75840 : [(290 ^ _75840) ^ [] ^ [] : [-(p4) : -([288 ^ []])], (293 ^ _75840) ^ [_86190] ^ [] : [-(p4) : -([288 ^ [], _86190])], (295 ^ _75840) ^ [] ^ [] : [-(p4) : -([288 ^ []])], (297 ^ _75840) ^ [] ^ [] : [p5 : [288 ^ []]], (299 ^ _75840) ^ [] ^ [] : [p4 : [288 ^ []]], (302 ^ _75840) ^ [_86512] ^ [] : [-(p5) : -([288 ^ [], _86512])], (304 ^ _75840) ^ [] ^ [] : [-(p5) : -([288 ^ []])]], 309 ^ _75840 : [(310 ^ _75840) ^ [] ^ [] : [-(p4) : -([307 ^ [], 308 ^ []])], (313 ^ _75840) ^ [_86910] ^ [] : [-(p4) : -([307 ^ [], 308 ^ [], _86910])], (315 ^ _75840) ^ [] ^ [] : [-(p4) : -([307 ^ [], 308 ^ []])], (317 ^ _75840) ^ [] ^ [] : [p5 : [307 ^ [], 308 ^ []]], (319 ^ _75840) ^ [] ^ [] : [p4 : [307 ^ []]], (322 ^ _75840) ^ [_87234] ^ [] : [-(p5) : -([307 ^ [], _87234])], (324 ^ _75840) ^ [] ^ [] : [-(p5) : -([307 ^ []])]], 326 ^ _75840 : [(327 ^ _75840) ^ [] ^ [] : [-(p4) : -([325 ^ []])], (330 ^ _75840) ^ [_87569] ^ [] : [-(p4) : -([325 ^ [], _87569])], (332 ^ _75840) ^ [] ^ [] : [-(p4) : -([325 ^ []])], (334 ^ _75840) ^ [] ^ [] : [p5 : [325 ^ []]], (337 ^ _75840) ^ [] ^ [] : [p4 : [325 ^ [], 335 ^ []]], (340 ^ _75840) ^ [_87918] ^ [] : [-(p5) : -([325 ^ [], 335 ^ [], _87918])], (342 ^ _75840) ^ [] ^ [] : [-(p5) : -([325 ^ [], 335 ^ []])]], 362 ^ _75840 : [(363 ^ _75840) ^ [_88645] ^ [] : [-(p4) : -([_88645]), p5 : [_88645, 368 ^ [_88645]], p5 : [_88645]]], 346 ^ _75840 : [(347 ^ _75840) ^ [_88139] ^ [] : [-(p5) : -([_88139]), p4 : [_88139], p4 : [_88139, 354 ^ [_88139]], p4 : [_88139]]]], (374 ^ _75840) ^ [] ^ [] : [378 ^ _75840 : [(379 ^ _75840) ^ [] ^ [] : [-(p5) : -([377 ^ []])], (382 ^ _75840) ^ [_89324] ^ [] : [-(p5) : -([377 ^ [], _89324])], (384 ^ _75840) ^ [] ^ [] : [-(p5) : -([377 ^ []])], (386 ^ _75840) ^ [] ^ [] : [p6 : [377 ^ []]], (388 ^ _75840) ^ [] ^ [] : [p5 : [377 ^ []]], (391 ^ _75840) ^ [_89646] ^ [] : [-(p6) : -([377 ^ [], _89646])], (393 ^ _75840) ^ [] ^ [] : [-(p6) : -([377 ^ []])]], 398 ^ _75840 : [(399 ^ _75840) ^ [] ^ [] : [-(p5) : -([396 ^ [], 397 ^ []])], (402 ^ _75840) ^ [_90044] ^ [] : [-(p5) : -([396 ^ [], 397 ^ [], _90044])], (404 ^ _75840) ^ [] ^ [] : [-(p5) : -([396 ^ [], 397 ^ []])], (406 ^ _75840) ^ [] ^ [] : [p6 : [396 ^ [], 397 ^ []]], (408 ^ _75840) ^ [] ^ [] : [p5 : [396 ^ []]], (411 ^ _75840) ^ [_90368] ^ [] : [-(p6) : -([396 ^ [], _90368])], (413 ^ _75840) ^ [] ^ [] : [-(p6) : -([396 ^ []])]], 415 ^ _75840 : [(416 ^ _75840) ^ [] ^ [] : [-(p5) : -([414 ^ []])], (419 ^ _75840) ^ [_90703] ^ [] : [-(p5) : -([414 ^ [], _90703])], (421 ^ _75840) ^ [] ^ [] : [-(p5) : -([414 ^ []])], (423 ^ _75840) ^ [] ^ [] : [p6 : [414 ^ []]], (426 ^ _75840) ^ [] ^ [] : [p5 : [414 ^ [], 424 ^ []]], (429 ^ _75840) ^ [_91052] ^ [] : [-(p6) : -([414 ^ [], 424 ^ [], _91052])], (431 ^ _75840) ^ [] ^ [] : [-(p6) : -([414 ^ [], 424 ^ []])]], 451 ^ _75840 : [(452 ^ _75840) ^ [_91779] ^ [] : [-(p5) : -([_91779]), p6 : [_91779, 457 ^ [_91779]], p6 : [_91779]]], 435 ^ _75840 : [(436 ^ _75840) ^ [_91273] ^ [] : [-(p6) : -([_91273]), p5 : [_91273], p5 : [_91273, 443 ^ [_91273]], p5 : [_91273]]]], (463 ^ _75840) ^ [] ^ [] : [467 ^ _75840 : [(468 ^ _75840) ^ [] ^ [] : [-(p6) : -([466 ^ []])], (471 ^ _75840) ^ [_92458] ^ [] : [-(p6) : -([466 ^ [], _92458])], (473 ^ _75840) ^ [] ^ [] : [-(p6) : -([466 ^ []])], (475 ^ _75840) ^ [] ^ [] : [p7 : [466 ^ []]], (477 ^ _75840) ^ [] ^ [] : [p6 : [466 ^ []]], (480 ^ _75840) ^ [_92780] ^ [] : [-(p7) : -([466 ^ [], _92780])], (482 ^ _75840) ^ [] ^ [] : [-(p7) : -([466 ^ []])]], 487 ^ _75840 : [(488 ^ _75840) ^ [] ^ [] : [-(p6) : -([485 ^ [], 486 ^ []])], (491 ^ _75840) ^ [_93178] ^ [] : [-(p6) : -([485 ^ [], 486 ^ [], _93178])], (493 ^ _75840) ^ [] ^ [] : [-(p6) : -([485 ^ [], 486 ^ []])], (495 ^ _75840) ^ [] ^ [] : [p7 : [485 ^ [], 486 ^ []]], (497 ^ _75840) ^ [] ^ [] : [p6 : [485 ^ []]], (500 ^ _75840) ^ [_93502] ^ [] : [-(p7) : -([485 ^ [], _93502])], (502 ^ _75840) ^ [] ^ [] : [-(p7) : -([485 ^ []])]], 504 ^ _75840 : [(505 ^ _75840) ^ [] ^ [] : [-(p6) : -([503 ^ []])], (508 ^ _75840) ^ [_93837] ^ [] : [-(p6) : -([503 ^ [], _93837])], (510 ^ _75840) ^ [] ^ [] : [-(p6) : -([503 ^ []])], (512 ^ _75840) ^ [] ^ [] : [p7 : [503 ^ []]], (515 ^ _75840) ^ [] ^ [] : [p6 : [503 ^ [], 513 ^ []]], (518 ^ _75840) ^ [_94186] ^ [] : [-(p7) : -([503 ^ [], 513 ^ [], _94186])], (520 ^ _75840) ^ [] ^ [] : [-(p7) : -([503 ^ [], 513 ^ []])]], 540 ^ _75840 : [(541 ^ _75840) ^ [_94913] ^ [] : [-(p6) : -([_94913]), p7 : [_94913, 546 ^ [_94913]], p7 : [_94913]]], 524 ^ _75840 : [(525 ^ _75840) ^ [_94407] ^ [] : [-(p7) : -([_94407]), p6 : [_94407], p6 : [_94407, 532 ^ [_94407]], p6 : [_94407]]]], (552 ^ _75840) ^ [] ^ [] : [556 ^ _75840 : [(557 ^ _75840) ^ [] ^ [] : [-(p7) : -([555 ^ []])], (560 ^ _75840) ^ [_95592] ^ [] : [-(p7) : -([555 ^ [], _95592])], (562 ^ _75840) ^ [] ^ [] : [-(p7) : -([555 ^ []])], (564 ^ _75840) ^ [] ^ [] : [p8 : [555 ^ []]], (566 ^ _75840) ^ [] ^ [] : [p7 : [555 ^ []]], (569 ^ _75840) ^ [_95914] ^ [] : [-(p8) : -([555 ^ [], _95914])], (571 ^ _75840) ^ [] ^ [] : [-(p8) : -([555 ^ []])]], 576 ^ _75840 : [(577 ^ _75840) ^ [] ^ [] : [-(p7) : -([574 ^ [], 575 ^ []])], (580 ^ _75840) ^ [_96312] ^ [] : [-(p7) : -([574 ^ [], 575 ^ [], _96312])], (582 ^ _75840) ^ [] ^ [] : [-(p7) : -([574 ^ [], 575 ^ []])], (584 ^ _75840) ^ [] ^ [] : [p8 : [574 ^ [], 575 ^ []]], (586 ^ _75840) ^ [] ^ [] : [p7 : [574 ^ []]], (589 ^ _75840) ^ [_96636] ^ [] : [-(p8) : -([574 ^ [], _96636])], (591 ^ _75840) ^ [] ^ [] : [-(p8) : -([574 ^ []])]], 593 ^ _75840 : [(594 ^ _75840) ^ [] ^ [] : [-(p7) : -([592 ^ []])], (597 ^ _75840) ^ [_96971] ^ [] : [-(p7) : -([592 ^ [], _96971])], (599 ^ _75840) ^ [] ^ [] : [-(p7) : -([592 ^ []])], (601 ^ _75840) ^ [] ^ [] : [p8 : [592 ^ []]], (604 ^ _75840) ^ [] ^ [] : [p7 : [592 ^ [], 602 ^ []]], (607 ^ _75840) ^ [_97320] ^ [] : [-(p8) : -([592 ^ [], 602 ^ [], _97320])], (609 ^ _75840) ^ [] ^ [] : [-(p8) : -([592 ^ [], 602 ^ []])]], 629 ^ _75840 : [(630 ^ _75840) ^ [_98047] ^ [] : [-(p7) : -([_98047]), p8 : [_98047, 635 ^ [_98047]], p8 : [_98047]]], 613 ^ _75840 : [(614 ^ _75840) ^ [_97541] ^ [] : [-(p8) : -([_97541]), p7 : [_97541], p7 : [_97541, 621 ^ [_97541]], p7 : [_97541]]]], (641 ^ _75840) ^ [] ^ [] : [645 ^ _75840 : [(646 ^ _75840) ^ [] ^ [] : [-(p8) : -([644 ^ []])], (649 ^ _75840) ^ [_98726] ^ [] : [-(p8) : -([644 ^ [], _98726])], (651 ^ _75840) ^ [] ^ [] : [-(p8) : -([644 ^ []])], (653 ^ _75840) ^ [] ^ [] : [p9 : [644 ^ []]], (655 ^ _75840) ^ [] ^ [] : [p8 : [644 ^ []]], (658 ^ _75840) ^ [_99048] ^ [] : [-(p9) : -([644 ^ [], _99048])], (660 ^ _75840) ^ [] ^ [] : [-(p9) : -([644 ^ []])]], 665 ^ _75840 : [(666 ^ _75840) ^ [] ^ [] : [-(p8) : -([663 ^ [], 664 ^ []])], (669 ^ _75840) ^ [_99446] ^ [] : [-(p8) : -([663 ^ [], 664 ^ [], _99446])], (671 ^ _75840) ^ [] ^ [] : [-(p8) : -([663 ^ [], 664 ^ []])], (673 ^ _75840) ^ [] ^ [] : [p9 : [663 ^ [], 664 ^ []]], (675 ^ _75840) ^ [] ^ [] : [p8 : [663 ^ []]], (678 ^ _75840) ^ [_99770] ^ [] : [-(p9) : -([663 ^ [], _99770])], (680 ^ _75840) ^ [] ^ [] : [-(p9) : -([663 ^ []])]], 682 ^ _75840 : [(683 ^ _75840) ^ [] ^ [] : [-(p8) : -([681 ^ []])], (686 ^ _75840) ^ [_100105] ^ [] : [-(p8) : -([681 ^ [], _100105])], (688 ^ _75840) ^ [] ^ [] : [-(p8) : -([681 ^ []])], (690 ^ _75840) ^ [] ^ [] : [p9 : [681 ^ []]], (693 ^ _75840) ^ [] ^ [] : [p8 : [681 ^ [], 691 ^ []]], (696 ^ _75840) ^ [_100454] ^ [] : [-(p9) : -([681 ^ [], 691 ^ [], _100454])], (698 ^ _75840) ^ [] ^ [] : [-(p9) : -([681 ^ [], 691 ^ []])]], 718 ^ _75840 : [(719 ^ _75840) ^ [_101181] ^ [] : [-(p8) : -([_101181]), p9 : [_101181, 724 ^ [_101181]], p9 : [_101181]]], 702 ^ _75840 : [(703 ^ _75840) ^ [_100675] ^ [] : [-(p9) : -([_100675]), p8 : [_100675], p8 : [_100675, 710 ^ [_100675]], p8 : [_100675]]]], (730 ^ _75840) ^ [] ^ [] : [734 ^ _75840 : [(735 ^ _75840) ^ [] ^ [] : [-(p9) : -([733 ^ []])], (738 ^ _75840) ^ [_101860] ^ [] : [-(p9) : -([733 ^ [], _101860])], (740 ^ _75840) ^ [] ^ [] : [-(p9) : -([733 ^ []])], (742 ^ _75840) ^ [] ^ [] : [p10 : [733 ^ []]], (744 ^ _75840) ^ [] ^ [] : [p9 : [733 ^ []]], (747 ^ _75840) ^ [_102182] ^ [] : [-(p10) : -([733 ^ [], _102182])], (749 ^ _75840) ^ [] ^ [] : [-(p10) : -([733 ^ []])]], 754 ^ _75840 : [(755 ^ _75840) ^ [] ^ [] : [-(p9) : -([752 ^ [], 753 ^ []])], (758 ^ _75840) ^ [_102580] ^ [] : [-(p9) : -([752 ^ [], 753 ^ [], _102580])], (760 ^ _75840) ^ [] ^ [] : [-(p9) : -([752 ^ [], 753 ^ []])], (762 ^ _75840) ^ [] ^ [] : [p10 : [752 ^ [], 753 ^ []]], (764 ^ _75840) ^ [] ^ [] : [p9 : [752 ^ []]], (767 ^ _75840) ^ [_102904] ^ [] : [-(p10) : -([752 ^ [], _102904])], (769 ^ _75840) ^ [] ^ [] : [-(p10) : -([752 ^ []])]], 771 ^ _75840 : [(772 ^ _75840) ^ [] ^ [] : [-(p9) : -([770 ^ []])], (775 ^ _75840) ^ [_103239] ^ [] : [-(p9) : -([770 ^ [], _103239])], (777 ^ _75840) ^ [] ^ [] : [-(p9) : -([770 ^ []])], (779 ^ _75840) ^ [] ^ [] : [p10 : [770 ^ []]], (782 ^ _75840) ^ [] ^ [] : [p9 : [770 ^ [], 780 ^ []]], (785 ^ _75840) ^ [_103588] ^ [] : [-(p10) : -([770 ^ [], 780 ^ [], _103588])], (787 ^ _75840) ^ [] ^ [] : [-(p10) : -([770 ^ [], 780 ^ []])]], 807 ^ _75840 : [(808 ^ _75840) ^ [_104315] ^ [] : [-(p9) : -([_104315]), p10 : [_104315, 813 ^ [_104315]], p10 : [_104315]]], 791 ^ _75840 : [(792 ^ _75840) ^ [_103809] ^ [] : [-(p10) : -([_103809]), p9 : [_103809], p9 : [_103809, 799 ^ [_103809]], p9 : [_103809]]]], (819 ^ _75840) ^ [] ^ [] : [823 ^ _75840 : [(824 ^ _75840) ^ [] ^ [] : [-(p10) : -([822 ^ []])], (827 ^ _75840) ^ [_104971] ^ [] : [-(p10) : -([822 ^ [], _104971])], (829 ^ _75840) ^ [] ^ [] : [-(p10) : -([822 ^ []])], (831 ^ _75840) ^ [] ^ [] : [p11 : [822 ^ []]], (833 ^ _75840) ^ [] ^ [] : [p10 : [822 ^ []]], (836 ^ _75840) ^ [_105293] ^ [] : [-(p11) : -([822 ^ [], _105293])], (838 ^ _75840) ^ [] ^ [] : [-(p11) : -([822 ^ []])]], 843 ^ _75840 : [(844 ^ _75840) ^ [] ^ [] : [-(p10) : -([841 ^ [], 842 ^ []])], (847 ^ _75840) ^ [_105691] ^ [] : [-(p10) : -([841 ^ [], 842 ^ [], _105691])], (849 ^ _75840) ^ [] ^ [] : [-(p10) : -([841 ^ [], 842 ^ []])], (851 ^ _75840) ^ [] ^ [] : [p11 : [841 ^ [], 842 ^ []]], (853 ^ _75840) ^ [] ^ [] : [p10 : [841 ^ []]], (856 ^ _75840) ^ [_106015] ^ [] : [-(p11) : -([841 ^ [], _106015])], (858 ^ _75840) ^ [] ^ [] : [-(p11) : -([841 ^ []])]], 860 ^ _75840 : [(861 ^ _75840) ^ [] ^ [] : [-(p10) : -([859 ^ []])], (864 ^ _75840) ^ [_106350] ^ [] : [-(p10) : -([859 ^ [], _106350])], (866 ^ _75840) ^ [] ^ [] : [-(p10) : -([859 ^ []])], (868 ^ _75840) ^ [] ^ [] : [p11 : [859 ^ []]], (871 ^ _75840) ^ [] ^ [] : [p10 : [859 ^ [], 869 ^ []]], (874 ^ _75840) ^ [_106699] ^ [] : [-(p11) : -([859 ^ [], 869 ^ [], _106699])], (876 ^ _75840) ^ [] ^ [] : [-(p11) : -([859 ^ [], 869 ^ []])]], 896 ^ _75840 : [(897 ^ _75840) ^ [_107426] ^ [] : [-(p10) : -([_107426]), p11 : [_107426, 902 ^ [_107426]], p11 : [_107426]]], 880 ^ _75840 : [(881 ^ _75840) ^ [_106920] ^ [] : [-(p11) : -([_106920]), p10 : [_106920], p10 : [_106920, 888 ^ [_106920]], p10 : [_106920]]]]]
% 7.92/8.99
% 7.92/8.99 We prove that the given matrix is valid, i.e. for
% 7.92/8.99 a given substitution it evaluates to true for all
% 7.92/8.99 interpretations. A matrix is true iff at least one
% 7.92/8.99 of its clauses is true; a clause is true iff all of
% 7.92/8.99 its elements (literals and submatrices) are true.
% 7.92/8.99
% 7.92/8.99 The proof is by contradiction:
% 7.92/8.99 Assume there is an interpretation so that the given
% 7.92/8.99 matrix evaluates to false. Then in each clause there
% 7.92/8.99 has to be at least one element that is false.
% 7.92/8.99
% 7.92/8.99 Then clause (275 ^ 0) is false if at least one of the following is false:
% 7.92/8.99 [p10 : [268 ^ []]]
% 7.92/8.99 1 Assume p10 : [268 ^ []] is false.
% 7.92/8.99 Then clause (270 ^ 1) is true.
% 7.92/8.99
% 7.92/8.99 Therefore there is no interpretation that makes the
% 7.92/8.99 given matrix false. Hence the given matrix is valid.
% 7.92/8.99 q.e.d.
% 7.92/8.99 ------------------------------------------------------
% 7.92/8.99 % SZS output end Proof for /export/starexec/sandbox2/tmp/tmp.4EL7XcyZeF/theBenchmark.p.qmf
% 7.92/8.99 % nanoCoP-M exiting
%------------------------------------------------------------------------------