%------------------------------------------------------------------------------
% File : nanoCoP-M---2.0
% Problem : SYO924_1.002 : TPTP v9.0.0. Released v9.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_nanocopm %s %d
% Computer : n007.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 14 09:14:07 EDT 2024
% Result : Theorem 15.25s 16.05s
% Output : Proof 15.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYO924_1.002 : TPTP v9.0.0. Released v9.0.0.
% 0.07/0.13 % Command : run_nanocopm %s %d
% 0.14/0.34 % Computer : n007.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon May 13 15:33:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.20/0.48 % Logic is s5
% 0.20/0.49 % Assuming rigid designation
% 0.20/0.49 % Designation is rigid
% 0.20/0.49 % Assuming local terms
% 0.20/0.49 % Terms are local
% 0.20/0.50 % Assuming constants domains
% 0.20/0.50 % Domains are const
% 0.20/0.51 ------------ Start QMF file ---------------
% 0.20/0.51 %------------------------------------------------------------------------------
% 0.20/0.51 % File : SYO924_1.002 : TPTP v9.0.0. Released v9.0.0.
% 0.20/0.51 % Domain : Syntactic
% 0.20/0.51 % Problem : KSP problem s5_t4p_p.0002
% 0.20/0.51 % Version : Especial.
% 0.20/0.51 % English :
% 0.20/0.51 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro
% 0.20/0.51 % : [NH+22] Nalon et al. (2022), Local Reductions for the Modal Cu
% 0.20/0.51 % : [Nal22] Nalon (2022), Email to Geoff Sutcliffe
% 0.20/0.51 % : [NH+23] Nalon et al. (2023), Buy One Get 14 Free: Evaluating L
% 0.20/0.51 % Source : [Nal22]
% 0.20/0.51 % Names : s5_t4p_p.0002 [Nal22]
% 0.20/0.51 % Status : Theorem
% 0.20/0.51 % Rating : ? v9.0.0
% 0.20/0.51 % Syntax : Number of formulae : 14 ( 0 unt; 13 typ; 0 def)
% 0.20/0.51 % Number of atoms : 167 ( 0 equ)
% 0.20/0.51 % Maximal formula atoms : 167 ( 167 avg)
% 0.20/0.51 % Number of connectives : 489 ( 88 ~; 78 |; 88 &)
% 0.20/0.51 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.20/0.51 % ( 235 {.}; 0 {#})
% 0.20/0.51 % Maximal formula depth : 31 ( 31 avg)
% 0.20/0.51 % Maximal term depth : 0 ( 0 avg)
% 0.20/0.51 % Number of types : 1 ( 0 usr)
% 0.20/0.51 % Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% 0.20/0.51 % Number of predicates : 13 ( 13 usr; 13 prp; 0-0 aty)
% 0.20/0.51 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.20/0.51 % Number of variables : 0 (; 0 !; 0 ?; 0 :)
% 0.20/0.51 % SPC : NX0_THM_PRP_NEQ_NAR
% 0.20/0.51 % Comments : Uses instances of T and 4 to produce the formula.
% 0.20/0.51 %------------------------------------------------------------------------------
% 0.20/0.51 qmf(prove,conjecture,(~ ( ( x0 & #box : ( ~ ( x0 ) ) ) | ( #box : ( #dia : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) | #box : ( #box : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) & #dia : ( #box : ( #dia : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) | #box : ( #box : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) & #dia : ( #box : ( #dia : ( ~ ( p0 ) | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) ) ) & #dia : ( #dia : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) & #dia : ( #box : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) ) & #dia : ( #dia : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) & #dia : ( #box : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) & #box : ( #dia : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) | #box : ( #box : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) & #box : ( #box : ( #dia : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) | #box : ( #box : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) & #box : ( ( #dia : ( #box : ( ~ ( p0 ) | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) ) | #dia : ( ( p0 | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) & #dia : ( ~ ( p3 ) | ( ~ ( y3 ) & #box : ( y3 ) ) | ( ~ ( z3 ) & #dia : ( #dia : ( #dia : ( #box : ( z3 ) ) ) ) ) ) ) ) & #box : ( #dia : ( #box : ( #dia : ( ( p0 | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) & #dia : ( ~ ( p3 ) | ( ~ ( y3 ) & #box : ( y3 ) ) | ( ~ ( z3 ) & #dia : ( #dia : ( #dia : ( #box : ( z3 ) ) ) ) ) ) ) ) ) | #dia : ( #box : ( ~ ( p0 ) | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) ) ) & ( #dia : ( #box : ( ~ ( p0 ) | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) ) | #box : ( #box : ( #dia : ( ( p0 | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) & #dia : ( ~ ( p3 ) | ( ~ ( y3 ) & #box : ( y3 ) ) | ( ~ ( z3 ) & #dia : ( #dia : ( #dia : ( #box : ( z3 ) ) ) ) ) ) ) ) ) ) & #box : ( #box : ( #dia : ( #box : ( ~ ( p0 ) | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) ) ) | ~ ( p0 ) | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) | #box : ( ( p0 | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) & #dia : ( ~ ( p3 ) | ( ~ ( y3 ) & #box : ( y3 ) ) | ( ~ ( z3 ) & #dia : ( #dia : ( #dia : ( #box : ( z3 ) ) ) ) ) ) ) ) & #box : ( #dia : ( ( p0 | ( ~ ( y0 ) & #box : ( y0 ) ) | ( ~ ( z0 ) & #dia : ( #dia : ( #dia : ( #box : ( z0 ) ) ) ) ) ) & #dia : ( ~ ( p3 ) | ( ~ ( y3 ) & #box : ( y3 ) ) | ( ~ ( z3 ) & #dia : ( #dia : ( #dia : ( #box : ( z3 ) ) ) ) ) ) ) ) ) & #box : ( #dia : ( #box : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) | #box : ( #box : ( #dia : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) ) ) & #box : ( #dia : ( #box : ( ~ ( p1 ) | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) | #box : ( #box : ( #dia : ( p1 | ( ~ ( y1 ) & #box : ( y1 ) ) | ( ~ ( z1 ) & #dia : ( #dia : ( #dia : ( #box : ( z1 ) ) ) ) ) ) ) ) ) & #box : ( ~ ( p4 ) | ( ~ ( y4 ) & #box : ( y4 ) ) | ( ~ ( z4 ) & #dia : ( #dia : ( #dia : ( #box : ( z4 ) ) ) ) ) ) ) ) )).
% 0.20/0.51 %------------------------------------------------------------------------------
% 0.20/0.51 ------------ End QMF file ---------------
% 15.25/16.05
% 15.25/16.05 % SZS status Theorem for $/export/starexec/sandbox/tmp/tmp.qFUf3JFESR/theBenchmark.p.qmf : (modal (s5/const))
% 15.25/16.05 % SZS output start Proof for /export/starexec/sandbox/tmp/tmp.qFUf3JFESR/theBenchmark.p.qmf
% 15.25/16.05 ------------------------------------------------------
% 15.25/16.05 Explanations for the proof presented below:
% 15.25/16.05 - equality axioms are added if required
% 15.25/16.05 - terms and variables are represented by Prolog terms
% 15.25/16.05 and Prolog variables, negation is represented by -
% 15.25/16.05 - a prefix Pre is a list of variables and constants
% 15.25/16.05 and assigned to each literal Lit, i.e. Pre:Lit
% 15.25/16.05 - clauses and (sub-)matrices have a unique label I^K:
% 15.25/16.05 or I^K^[..]:, where I is a unique number/identifier
% 15.25/16.05 and K identifies the instance of clause/matrix I
% 15.25/16.05 - I:Lit refers to literal Lit in clause number I
% 15.25/16.05 - in the matrix, I^[t1,..,tn] may represent the atom
% 15.25/16.05 P_I(t1,..,tn) or the Skolem term f_I(t1,t2,..,tn)
% 15.25/16.05 - the substitution [[X1,..,Xn],[t1,..,tn]] represents
% 15.25/16.05 the assignments X1:=t1, .., Xn:=tn (for both term
% 15.25/16.05 and prefix variables)
% 15.25/16.05
% 15.25/16.05 Proof:
% 15.25/16.05 ------
% 15.25/16.05 Translation into a non-clausal matrix:
% 15.25/16.05 [(2 ^ _130028) ^ [] ^ [] : [3 ^ _130028 : [(4 ^ _130028) ^ [] ^ [] : [-(x0) : -([])], (7 ^ _130028) ^ [_130214] ^ [] : [x0 : [_130214]]], 9 ^ _130028 : [(10 ^ _130028) ^ [_130341] ^ [] : [-(p1) : -([_130341, 11 ^ [_130341]]), 18 ^ _130028 : [(19 ^ _130028) ^ [] ^ [] : [y1 : [_130341, 11 ^ [_130341]]], (22 ^ _130028) ^ [_130725] ^ [] : [-(y1) : -([_130341, 11 ^ [_130341], _130725])]], 23 ^ _130028 : [(24 ^ _130028) ^ [] ^ [] : [z1 : [_130341, 11 ^ [_130341]]], (30 ^ _130028) ^ [_131032] ^ [] : [-(z1) : -([_130341, 11 ^ [_130341], 25 ^ [_130341], 26 ^ [_130341], 27 ^ [_130341], _131032])]], 33 ^ _130028 : [(34 ^ _130028) ^ [_131208, _131210] ^ [] : [p1 : [_130341, _131210, _131208], 39 ^ _130028 : [(40 ^ _130028) ^ [] ^ [] : [y1 : [_130341, _131210, _131208]], (43 ^ _130028) ^ [_131552] ^ [] : [-(y1) : -([_130341, _131210, _131208, _131552])]], 44 ^ _130028 : [(45 ^ _130028) ^ [] ^ [] : [z1 : [_130341, _131210, _131208]], (51 ^ _130028) ^ [_131885] ^ [] : [-(z1) : -([_130341, _131210, _131208, 46 ^ [_130341, _131208, _131210], 47 ^ [_130341, _131208, _131210], 48 ^ [_130341, _131208, _131210], _131885])]]]]], (55 ^ _130028) ^ [_132122] ^ [] : [-(p1) : -([52 ^ [], _132122, 56 ^ [_132122]]), 63 ^ _130028 : [(64 ^ _130028) ^ [] ^ [] : [y1 : [52 ^ [], _132122, 56 ^ [_132122]]], (67 ^ _130028) ^ [_132516] ^ [] : [-(y1) : -([52 ^ [], _132122, 56 ^ [_132122], _132516])]], 68 ^ _130028 : [(69 ^ _130028) ^ [] ^ [] : [z1 : [52 ^ [], _132122, 56 ^ [_132122]]], (75 ^ _130028) ^ [_132835] ^ [] : [-(z1) : -([52 ^ [], _132122, 56 ^ [_132122], 70 ^ [_132122], 71 ^ [_132122], 72 ^ [_132122], _132835])]], 78 ^ _130028 : [(79 ^ _130028) ^ [_133017, _133019] ^ [] : [p1 : [52 ^ [], _132122, _133019, _133017], 84 ^ _130028 : [(85 ^ _130028) ^ [] ^ [] : [y1 : [52 ^ [], _132122, _133019, _133017]], (88 ^ _130028) ^ [_133369] ^ [] : [-(y1) : -([52 ^ [], _132122, _133019, _133017, _133369])]], 89 ^ _130028 : [(90 ^ _130028) ^ [] ^ [] : [z1 : [52 ^ [], _132122, _133019, _133017]], (96 ^ _130028) ^ [_133714] ^ [] : [-(z1) : -([52 ^ [], _132122, _133019, _133017, 91 ^ [_132122, _133017, _133019], 92 ^ [_132122, _133017, _133019], 93 ^ [_132122, _133017, _133019], _133714])]]]]], (101 ^ _130028) ^ [_133961] ^ [] : [p0 : [52 ^ [], 97 ^ [], _133961, 99 ^ [_133961]], 106 ^ _130028 : [(107 ^ _130028) ^ [] ^ [] : [y0 : [52 ^ [], 97 ^ [], _133961, 99 ^ [_133961]]], (110 ^ _130028) ^ [_134306] ^ [] : [-(y0) : -([52 ^ [], 97 ^ [], _133961, 99 ^ [_133961], _134306])]], 111 ^ _130028 : [(112 ^ _130028) ^ [] ^ [] : [z0 : [52 ^ [], 97 ^ [], _133961, 99 ^ [_133961]]], (118 ^ _130028) ^ [_134637] ^ [] : [-(z0) : -([52 ^ [], 97 ^ [], _133961, 99 ^ [_133961], 113 ^ [_133961], 114 ^ [_133961], 115 ^ [_133961], _134637])]]], (122 ^ _130028) ^ [] ^ [] : [p1 : [52 ^ [], 119 ^ [], 120 ^ []], 127 ^ _130028 : [(128 ^ _130028) ^ [] ^ [] : [y1 : [52 ^ [], 119 ^ [], 120 ^ []]], (131 ^ _130028) ^ [_135063] ^ [] : [-(y1) : -([52 ^ [], 119 ^ [], 120 ^ [], _135063])]], 132 ^ _130028 : [(133 ^ _130028) ^ [] ^ [] : [z1 : [52 ^ [], 119 ^ [], 120 ^ []]], (139 ^ _130028) ^ [_135342] ^ [] : [-(z1) : -([52 ^ [], 119 ^ [], 120 ^ [], 134 ^ [], 135 ^ [], 136 ^ [], _135342])]]], (143 ^ _130028) ^ [_135499] ^ [] : [-(p1) : -([52 ^ [], 119 ^ [], 140 ^ [], _135499]), 148 ^ _130028 : [(149 ^ _130028) ^ [] ^ [] : [y1 : [52 ^ [], 119 ^ [], 140 ^ [], _135499]], (152 ^ _130028) ^ [_135828] ^ [] : [-(y1) : -([52 ^ [], 119 ^ [], 140 ^ [], _135499, _135828])]], 153 ^ _130028 : [(154 ^ _130028) ^ [] ^ [] : [z1 : [52 ^ [], 119 ^ [], 140 ^ [], _135499]], (160 ^ _130028) ^ [_136149] ^ [] : [-(z1) : -([52 ^ [], 119 ^ [], 140 ^ [], _135499, 155 ^ [_135499], 156 ^ [_135499], 157 ^ [_135499], _136149])]]], (164 ^ _130028) ^ [] ^ [] : [p1 : [161 ^ [], 162 ^ []], 169 ^ _130028 : [(170 ^ _130028) ^ [] ^ [] : [y1 : [161 ^ [], 162 ^ []]], (173 ^ _130028) ^ [_136593] ^ [] : [-(y1) : -([161 ^ [], 162 ^ [], _136593])]], 174 ^ _130028 : [(175 ^ _130028) ^ [] ^ [] : [z1 : [161 ^ [], 162 ^ []]], (181 ^ _130028) ^ [_136862] ^ [] : [-(z1) : -([161 ^ [], 162 ^ [], 176 ^ [], 177 ^ [], 178 ^ [], _136862])]]], (185 ^ _130028) ^ [_137013] ^ [] : [-(p1) : -([161 ^ [], 182 ^ [], _137013]), 190 ^ _130028 : [(191 ^ _130028) ^ [] ^ [] : [y1 : [161 ^ [], 182 ^ [], _137013]], (194 ^ _130028) ^ [_137334] ^ [] : [-(y1) : -([161 ^ [], 182 ^ [], _137013, _137334])]], 195 ^ _130028 : [(196 ^ _130028) ^ [] ^ [] : [z1 : [161 ^ [], 182 ^ [], _137013]], (202 ^ _130028) ^ [_137643] ^ [] : [-(z1) : -([161 ^ [], 182 ^ [], _137013, 197 ^ [_137013], 198 ^ [_137013], 199 ^ [_137013], _137643])]]], (205 ^ _130028) ^ [_137811] ^ [] : [p1 : [_137811, 206 ^ [_137811]], 213 ^ _130028 : [(214 ^ _130028) ^ [] ^ [] : [y1 : [_137811, 206 ^ [_137811]]], (217 ^ _130028) ^ [_138196] ^ [] : [-(y1) : -([_137811, 206 ^ [_137811], _138196])]], 218 ^ _130028 : [(219 ^ _130028) ^ [] ^ [] : [z1 : [_137811, 206 ^ [_137811]]], (225 ^ _130028) ^ [_138503] ^ [] : [-(z1) : -([_137811, 206 ^ [_137811], 220 ^ [_137811], 221 ^ [_137811], 222 ^ [_137811], _138503])]], 228 ^ _130028 : [(229 ^ _130028) ^ [_138679, _138681] ^ [] : [-(p1) : -([_137811, _138681, _138679]), 234 ^ _130028 : [(235 ^ _130028) ^ [] ^ [] : [y1 : [_137811, _138681, _138679]], (238 ^ _130028) ^ [_139022] ^ [] : [-(y1) : -([_137811, _138681, _138679, _139022])]], 239 ^ _130028 : [(240 ^ _130028) ^ [] ^ [] : [z1 : [_137811, _138681, _138679]], (246 ^ _130028) ^ [_139355] ^ [] : [-(z1) : -([_137811, _138681, _138679, 241 ^ [_137811, _138679, _138681], 242 ^ [_137811, _138679, _138681], 243 ^ [_137811, _138679, _138681], _139355])]]]]], (708 ^ _130028) ^ [_160957] ^ [] : [p4 : [_160957], 713 ^ _130028 : [(714 ^ _130028) ^ [] ^ [] : [y4 : [_160957]], (717 ^ _130028) ^ [_161263] ^ [] : [-(y4) : -([_160957, _161263])]], 718 ^ _130028 : [(719 ^ _130028) ^ [] ^ [] : [z4 : [_160957]], (725 ^ _130028) ^ [_161548] ^ [] : [-(z4) : -([_160957, 720 ^ [_160957], 721 ^ [_160957], 722 ^ [_160957], _161548])]]], (662 ^ _130028) ^ [_159009] ^ [] : [665 ^ _130028 : [(666 ^ _130028) ^ [_159145] ^ [] : [p1 : [_159009, 663 ^ [_159009], _159145], 671 ^ _130028 : [(672 ^ _130028) ^ [] ^ [] : [y1 : [_159009, 663 ^ [_159009], _159145]], (675 ^ _130028) ^ [_159494] ^ [] : [-(y1) : -([_159009, 663 ^ [_159009], _159145, _159494])]], 676 ^ _130028 : [(677 ^ _130028) ^ [] ^ [] : [z1 : [_159009, 663 ^ [_159009], _159145]], (683 ^ _130028) ^ [_159825] ^ [] : [-(z1) : -([_159009, 663 ^ [_159009], _159145, 678 ^ [_159009, _159145], 679 ^ [_159009, _159145], 680 ^ [_159009, _159145], _159825])]]]], 687 ^ _130028 : [(688 ^ _130028) ^ [_160040, _160042] ^ [] : [-(p1) : -([_159009, _160042, _160040, 686 ^ [_159009, _160040, _160042]]), 693 ^ _130028 : [(694 ^ _130028) ^ [] ^ [] : [y1 : [_159009, _160042, _160040, 686 ^ [_159009, _160040, _160042]]], (697 ^ _130028) ^ [_160418] ^ [] : [-(y1) : -([_159009, _160042, _160040, 686 ^ [_159009, _160040, _160042], _160418])]], 698 ^ _130028 : [(699 ^ _130028) ^ [] ^ [] : [z1 : [_159009, _160042, _160040, 686 ^ [_159009, _160040, _160042]]], (705 ^ _130028) ^ [_160781] ^ [] : [-(z1) : -([_159009, _160042, _160040, 686 ^ [_159009, _160040, _160042], 700 ^ [_159009, _160040, _160042], 701 ^ [_159009, _160040, _160042], 702 ^ [_159009, _160040, _160042], _160781])]]]]], (250 ^ _130028) ^ [_139591, _139593] ^ [] : [p1 : [_139593, _139591, 251 ^ [_139591, _139593]], 258 ^ _130028 : [(259 ^ _130028) ^ [] ^ [] : [y1 : [_139593, _139591, 251 ^ [_139591, _139593]]], (262 ^ _130028) ^ [_140004] ^ [] : [-(y1) : -([_139593, _139591, 251 ^ [_139591, _139593], _140004])]], 263 ^ _130028 : [(264 ^ _130028) ^ [] ^ [] : [z1 : [_139593, _139591, 251 ^ [_139591, _139593]]], (270 ^ _130028) ^ [_140339] ^ [] : [-(z1) : -([_139593, _139591, 251 ^ [_139591, _139593], 265 ^ [_139591, _139593], 266 ^ [_139591, _139593], 267 ^ [_139591, _139593], _140339])]], 273 ^ _130028 : [(274 ^ _130028) ^ [_140535, _140537] ^ [] : [-(p1) : -([_139593, _139591, _140537, _140535]), 279 ^ _130028 : [(280 ^ _130028) ^ [] ^ [] : [y1 : [_139593, _139591, _140537, _140535]], (283 ^ _130028) ^ [_140898] ^ [] : [-(y1) : -([_139593, _139591, _140537, _140535, _140898])]], 284 ^ _130028 : [(285 ^ _130028) ^ [] ^ [] : [z1 : [_139593, _139591, _140537, _140535]], (291 ^ _130028) ^ [_141255] ^ [] : [-(z1) : -([_139593, _139591, _140537, _140535, 286 ^ [_139591, _139593, _140535, _140537], 287 ^ [_139591, _139593, _140535, _140537], 288 ^ [_139591, _139593, _140535, _140537], _141255])]]]]], (616 ^ _130028) ^ [_156878, _156880] ^ [] : [619 ^ _130028 : [(620 ^ _130028) ^ [_157026] ^ [] : [p1 : [_156880, _156878, 617 ^ [_156878, _156880], _157026], 625 ^ _130028 : [(626 ^ _130028) ^ [] ^ [] : [y1 : [_156880, _156878, 617 ^ [_156878, _156880], _157026]], (629 ^ _130028) ^ [_157401] ^ [] : [-(y1) : -([_156880, _156878, 617 ^ [_156878, _156880], _157026, _157401])]], 630 ^ _130028 : [(631 ^ _130028) ^ [] ^ [] : [z1 : [_156880, _156878, 617 ^ [_156878, _156880], _157026]], (637 ^ _130028) ^ [_157760] ^ [] : [-(z1) : -([_156880, _156878, 617 ^ [_156878, _156880], _157026, 632 ^ [_156878, _156880, _157026], 633 ^ [_156878, _156880, _157026], 634 ^ [_156878, _156880, _157026], _157760])]]]], 641 ^ _130028 : [(642 ^ _130028) ^ [_157999, _158001] ^ [] : [-(p1) : -([_156880, _156878, _158001, _157999, 640 ^ [_156878, _156880, _157999, _158001]]), 647 ^ _130028 : [(648 ^ _130028) ^ [] ^ [] : [y1 : [_156880, _156878, _158001, _157999, 640 ^ [_156878, _156880, _157999, _158001]]], (651 ^ _130028) ^ [_158403] ^ [] : [-(y1) : -([_156880, _156878, _158001, _157999, 640 ^ [_156878, _156880, _157999, _158001], _158403])]], 652 ^ _130028 : [(653 ^ _130028) ^ [] ^ [] : [z1 : [_156880, _156878, _158001, _157999, 640 ^ [_156878, _156880, _157999, _158001]]], (659 ^ _130028) ^ [_158794] ^ [] : [-(z1) : -([_156880, _156878, _158001, _157999, 640 ^ [_156878, _156880, _157999, _158001], 654 ^ [_156878, _156880, _157999, _158001], 655 ^ [_156878, _156880, _157999, _158001], 656 ^ [_156878, _156880, _157999, _158001], _158794])]]]]], (294 ^ _130028) ^ [_141481, _141483] ^ [] : [297 ^ _130028 : [(298 ^ _130028) ^ [_141629] ^ [] : [p0 : [_141483, _141481, 295 ^ [_141481, _141483], _141629], 303 ^ _130028 : [(304 ^ _130028) ^ [] ^ [] : [y0 : [_141483, _141481, 295 ^ [_141481, _141483], _141629]], (307 ^ _130028) ^ [_142004] ^ [] : [-(y0) : -([_141483, _141481, 295 ^ [_141481, _141483], _141629, _142004])]], 308 ^ _130028 : [(309 ^ _130028) ^ [] ^ [] : [z0 : [_141483, _141481, 295 ^ [_141481, _141483], _141629]], (315 ^ _130028) ^ [_142363] ^ [] : [-(z0) : -([_141483, _141481, 295 ^ [_141481, _141483], _141629, 310 ^ [_141481, _141483, _141629], 311 ^ [_141481, _141483, _141629], 312 ^ [_141481, _141483, _141629], _142363])]]]], 317 ^ _130028 : [(318 ^ _130028) ^ [] ^ [] : [-(p0) : -([_141483, _141481, 316 ^ [_141481, _141483]]), 323 ^ _130028 : [(324 ^ _130028) ^ [] ^ [] : [y0 : [_141483, _141481, 316 ^ [_141481, _141483]]], (327 ^ _130028) ^ [_142857] ^ [] : [-(y0) : -([_141483, _141481, 316 ^ [_141481, _141483], _142857])]], 328 ^ _130028 : [(329 ^ _130028) ^ [] ^ [] : [z0 : [_141483, _141481, 316 ^ [_141481, _141483]]], (335 ^ _130028) ^ [_143192] ^ [] : [-(z0) : -([_141483, _141481, 316 ^ [_141481, _141483], 330 ^ [_141481, _141483], 331 ^ [_141481, _141483], 332 ^ [_141481, _141483], _143192])]]], (338 ^ _130028) ^ [] ^ [] : [p3 : [_141483, _141481, 316 ^ [_141481, _141483], 336 ^ [_141481, _141483]], 343 ^ _130028 : [(344 ^ _130028) ^ [] ^ [] : [y3 : [_141483, _141481, 316 ^ [_141481, _141483], 336 ^ [_141481, _141483]]], (347 ^ _130028) ^ [_143676] ^ [] : [-(y3) : -([_141483, _141481, 316 ^ [_141481, _141483], 336 ^ [_141481, _141483], _143676])]], 348 ^ _130028 : [(349 ^ _130028) ^ [] ^ [] : [z3 : [_141483, _141481, 316 ^ [_141481, _141483], 336 ^ [_141481, _141483]]], (355 ^ _130028) ^ [_144037] ^ [] : [-(z3) : -([_141483, _141481, 316 ^ [_141481, _141483], 336 ^ [_141481, _141483], 350 ^ [_141481, _141483], 351 ^ [_141481, _141483], 352 ^ [_141481, _141483], _144037])]]]]], (358 ^ _130028) ^ [_144239, _144241, _144243] ^ [] : [403 ^ _130028 : [(404 ^ _130028) ^ [_146726] ^ [] : [p0 : [_144243, _144241, _144239, 401 ^ [_144239, _144241, _144243], _146726], 409 ^ _130028 : [(410 ^ _130028) ^ [] ^ [] : [y0 : [_144243, _144241, _144239, 401 ^ [_144239, _144241, _144243], _146726]], (413 ^ _130028) ^ [_147127] ^ [] : [-(y0) : -([_144243, _144241, _144239, 401 ^ [_144239, _144241, _144243], _146726, _147127])]], 414 ^ _130028 : [(415 ^ _130028) ^ [] ^ [] : [z0 : [_144243, _144241, _144239, 401 ^ [_144239, _144241, _144243], _146726]], (421 ^ _130028) ^ [_147514] ^ [] : [-(z0) : -([_144243, _144241, _144239, 401 ^ [_144239, _144241, _144243], _146726, 416 ^ [_144239, _144241, _144243, _146726], 417 ^ [_144239, _144241, _144243, _146726], 418 ^ [_144239, _144241, _144243, _146726], _147514])]]]], 362 ^ _130028 : [(363 ^ _130028) ^ [_144459] ^ [] : [-(p0) : -([_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _144459, 361 ^ [_144239, _144241, _144243, _144459]]), 368 ^ _130028 : [(369 ^ _130028) ^ [] ^ [] : [y0 : [_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _144459, 361 ^ [_144239, _144241, _144243, _144459]]], (372 ^ _130028) ^ [_144900] ^ [] : [-(y0) : -([_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _144459, 361 ^ [_144239, _144241, _144243, _144459], _144900])]], 373 ^ _130028 : [(374 ^ _130028) ^ [] ^ [] : [z0 : [_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _144459, 361 ^ [_144239, _144241, _144243, _144459]]], (380 ^ _130028) ^ [_145321] ^ [] : [-(z0) : -([_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _144459, 361 ^ [_144239, _144241, _144243, _144459], 375 ^ [_144239, _144241, _144243, _144459], 376 ^ [_144239, _144241, _144243, _144459], 377 ^ [_144239, _144241, _144243, _144459], _145321])]]], (383 ^ _130028) ^ [_145533] ^ [] : [p3 : [_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _145533, 361 ^ [_144239, _144241, _144243, _145533], 381 ^ [_144239, _144241, _144243, _145533]], 388 ^ _130028 : [(389 ^ _130028) ^ [] ^ [] : [y3 : [_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _145533, 361 ^ [_144239, _144241, _144243, _145533], 381 ^ [_144239, _144241, _144243, _145533]]], (392 ^ _130028) ^ [_146016] ^ [] : [-(y3) : -([_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _145533, 361 ^ [_144239, _144241, _144243, _145533], 381 ^ [_144239, _144241, _144243, _145533], _146016])]], 393 ^ _130028 : [(394 ^ _130028) ^ [] ^ [] : [z3 : [_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _145533, 361 ^ [_144239, _144241, _144243, _145533], 381 ^ [_144239, _144241, _144243, _145533]]], (400 ^ _130028) ^ [_146471] ^ [] : [-(z3) : -([_144243, _144241, _144239, 359 ^ [_144239, _144241, _144243], _145533, 361 ^ [_144239, _144241, _144243, _145533], 381 ^ [_144239, _144241, _144243, _145533], 395 ^ [_144239, _144241, _144243, _145533], 396 ^ [_144239, _144241, _144243, _145533], 397 ^ [_144239, _144241, _144243, _145533], _146471])]]]]], (423 ^ _130028) ^ [_147703, _147705] ^ [] : [426 ^ _130028 : [(427 ^ _130028) ^ [_147851] ^ [] : [p0 : [_147705, _147703, 424 ^ [_147703, _147705], _147851], 432 ^ _130028 : [(433 ^ _130028) ^ [] ^ [] : [y0 : [_147705, _147703, 424 ^ [_147703, _147705], _147851]], (436 ^ _130028) ^ [_148226] ^ [] : [-(y0) : -([_147705, _147703, 424 ^ [_147703, _147705], _147851, _148226])]], 437 ^ _130028 : [(438 ^ _130028) ^ [] ^ [] : [z0 : [_147705, _147703, 424 ^ [_147703, _147705], _147851]], (444 ^ _130028) ^ [_148585] ^ [] : [-(z0) : -([_147705, _147703, 424 ^ [_147703, _147705], _147851, 439 ^ [_147703, _147705, _147851], 440 ^ [_147703, _147705, _147851], 441 ^ [_147703, _147705, _147851], _148585])]]]], 448 ^ _130028 : [(449 ^ _130028) ^ [_148847, _148849] ^ [] : [-(p0) : -([_147705, _147703, _148849, _148847, 447 ^ [_147703, _147705, _148847, _148849]]), 454 ^ _130028 : [(455 ^ _130028) ^ [] ^ [] : [y0 : [_147705, _147703, _148849, _148847, 447 ^ [_147703, _147705, _148847, _148849]]], (458 ^ _130028) ^ [_149251] ^ [] : [-(y0) : -([_147705, _147703, _148849, _148847, 447 ^ [_147703, _147705, _148847, _148849], _149251])]], 459 ^ _130028 : [(460 ^ _130028) ^ [] ^ [] : [z0 : [_147705, _147703, _148849, _148847, 447 ^ [_147703, _147705, _148847, _148849]]], (466 ^ _130028) ^ [_149642] ^ [] : [-(z0) : -([_147705, _147703, _148849, _148847, 447 ^ [_147703, _147705, _148847, _148849], 461 ^ [_147703, _147705, _148847, _148849], 462 ^ [_147703, _147705, _148847, _148849], 463 ^ [_147703, _147705, _148847, _148849], _149642])]]], (469 ^ _130028) ^ [_149839, _149841] ^ [] : [p3 : [_147705, _147703, _149841, _149839, 447 ^ [_147703, _147705, _149839, _149841], 467 ^ [_147703, _147705, _149839, _149841]], 474 ^ _130028 : [(475 ^ _130028) ^ [] ^ [] : [y3 : [_147705, _147703, _149841, _149839, 447 ^ [_147703, _147705, _149839, _149841], 467 ^ [_147703, _147705, _149839, _149841]]], (478 ^ _130028) ^ [_150285] ^ [] : [-(y3) : -([_147705, _147703, _149841, _149839, 447 ^ [_147703, _147705, _149839, _149841], 467 ^ [_147703, _147705, _149839, _149841], _150285])]], 479 ^ _130028 : [(480 ^ _130028) ^ [] ^ [] : [z3 : [_147705, _147703, _149841, _149839, 447 ^ [_147703, _147705, _149839, _149841], 467 ^ [_147703, _147705, _149839, _149841]]], (486 ^ _130028) ^ [_150710] ^ [] : [-(z3) : -([_147705, _147703, _149841, _149839, 447 ^ [_147703, _147705, _149839, _149841], 467 ^ [_147703, _147705, _149839, _149841], 481 ^ [_147703, _147705, _149839, _149841], 482 ^ [_147703, _147705, _149839, _149841], 483 ^ [_147703, _147705, _149839, _149841], _150710])]]]]], (576 ^ _130028) ^ [_154960, _154962, _154964] ^ [] : [-(p0) : -([_154964, _154962, _154960, 574 ^ [_154960, _154962, _154964]]), 581 ^ _130028 : [(582 ^ _130028) ^ [] ^ [] : [y0 : [_154964, _154962, _154960, 574 ^ [_154960, _154962, _154964]]], (585 ^ _130028) ^ [_155336] ^ [] : [-(y0) : -([_154964, _154962, _154960, 574 ^ [_154960, _154962, _154964], _155336])]], 586 ^ _130028 : [(587 ^ _130028) ^ [] ^ [] : [z0 : [_154964, _154962, _154960, 574 ^ [_154960, _154962, _154964]]], (593 ^ _130028) ^ [_155699] ^ [] : [-(z0) : -([_154964, _154962, _154960, 574 ^ [_154960, _154962, _154964], 588 ^ [_154960, _154962, _154964], 589 ^ [_154960, _154962, _154964], 590 ^ [_154960, _154962, _154964], _155699])]]], (596 ^ _130028) ^ [_155878, _155880, _155882] ^ [] : [p3 : [_155882, _155880, _155878, 574 ^ [_155878, _155880, _155882], 594 ^ [_155878, _155880, _155882]], 601 ^ _130028 : [(602 ^ _130028) ^ [] ^ [] : [y3 : [_155882, _155880, _155878, 574 ^ [_155878, _155880, _155882], 594 ^ [_155878, _155880, _155882]]], (605 ^ _130028) ^ [_156290] ^ [] : [-(y3) : -([_155882, _155880, _155878, 574 ^ [_155878, _155880, _155882], 594 ^ [_155878, _155880, _155882], _156290])]], 606 ^ _130028 : [(607 ^ _130028) ^ [] ^ [] : [z3 : [_155882, _155880, _155878, 574 ^ [_155878, _155880, _155882], 594 ^ [_155878, _155880, _155882]]], (613 ^ _130028) ^ [_156683] ^ [] : [-(z3) : -([_155882, _155880, _155878, 574 ^ [_155878, _155880, _155882], 594 ^ [_155878, _155880, _155882], 608 ^ [_155878, _155880, _155882], 609 ^ [_155878, _155880, _155882], 610 ^ [_155878, _155880, _155882], _156683])]]], (489 ^ _130028) ^ [_150940, _150942, _150944] ^ [] : [493 ^ _130028 : [(494 ^ _130028) ^ [_151136, _151138] ^ [] : [p0 : [_150944, _150942, _150940, _151138, 491 ^ [_150940, _150942, _150944, _151138], _151136], 499 ^ _130028 : [(500 ^ _130028) ^ [] ^ [] : [y0 : [_150944, _150942, _150940, _151138, 491 ^ [_150940, _150942, _150944, _151138], _151136]], (503 ^ _130028) ^ [_151561] ^ [] : [-(y0) : -([_150944, _150942, _150940, _151138, 491 ^ [_150940, _150942, _150944, _151138], _151136, _151561])]], 504 ^ _130028 : [(505 ^ _130028) ^ [] ^ [] : [z0 : [_150944, _150942, _150940, _151138, 491 ^ [_150940, _150942, _150944, _151138], _151136]], (511 ^ _130028) ^ [_151976] ^ [] : [-(z0) : -([_150944, _150942, _150940, _151138, 491 ^ [_150940, _150942, _150944, _151138], _151136, 506 ^ [_150940, _150942, _150944, _151136, _151138], 507 ^ [_150940, _150942, _150944, _151136, _151138], 508 ^ [_150940, _150942, _150944, _151136, _151138], _151976])]]]], p0 : [_150944, _150942, _150940], 518 ^ _130028 : [(519 ^ _130028) ^ [] ^ [] : [y0 : [_150944, _150942, _150940]], (522 ^ _130028) ^ [_152439] ^ [] : [-(y0) : -([_150944, _150942, _150940, _152439])]], 525 ^ _130028 : [(526 ^ _130028) ^ [] ^ [] : [z0 : [_150944, _150942, _150940]], (532 ^ _130028) ^ [_152814] ^ [] : [-(z0) : -([_150944, _150942, _150940, 527 ^ [_150940, _150942, _150944], 528 ^ [_150940, _150942, _150944], 529 ^ [_150940, _150942, _150944], _152814])]], 534 ^ _130028 : [(535 ^ _130028) ^ [_152998] ^ [] : [-(p0) : -([_150944, _150942, _150940, _152998]), 540 ^ _130028 : [(541 ^ _130028) ^ [] ^ [] : [y0 : [_150944, _150942, _150940, _152998]], (544 ^ _130028) ^ [_153363] ^ [] : [-(y0) : -([_150944, _150942, _150940, _152998, _153363])]], 545 ^ _130028 : [(546 ^ _130028) ^ [] ^ [] : [z0 : [_150944, _150942, _150940, _152998]], (552 ^ _130028) ^ [_153720] ^ [] : [-(z0) : -([_150944, _150942, _150940, _152998, 547 ^ [_150940, _150942, _150944, _152998], 548 ^ [_150940, _150942, _150944, _152998], 549 ^ [_150940, _150942, _150944, _152998], _153720])]]], (555 ^ _130028) ^ [_153904] ^ [] : [p3 : [_150944, _150942, _150940, _153904, 553 ^ [_150940, _150942, _150944, _153904]], 560 ^ _130028 : [(561 ^ _130028) ^ [] ^ [] : [y3 : [_150944, _150942, _150940, _153904, 553 ^ [_150940, _150942, _150944, _153904]]], (564 ^ _130028) ^ [_154311] ^ [] : [-(y3) : -([_150944, _150942, _150940, _153904, 553 ^ [_150940, _150942, _150944, _153904], _154311])]], 565 ^ _130028 : [(566 ^ _130028) ^ [] ^ [] : [z3 : [_150944, _150942, _150940, _153904, 553 ^ [_150940, _150942, _150944, _153904]]], (572 ^ _130028) ^ [_154702] ^ [] : [-(z3) : -([_150944, _150942, _150940, _153904, 553 ^ [_150940, _150942, _150944, _153904], 567 ^ [_150940, _150942, _150944, _153904], 568 ^ [_150940, _150942, _150944, _153904], 569 ^ [_150940, _150942, _150944, _153904], _154702])]]]]]]]]
% 15.25/16.06
% 15.25/16.06 We prove that the given matrix is valid, i.e. for
% 15.25/16.06 a given substitution it evaluates to true for all
% 15.25/16.06 interpretations. A matrix is true iff at least one
% 15.25/16.06 of its clauses is true; a clause is true iff all of
% 15.25/16.06 its elements (literals and submatrices) are true.
% 15.25/16.06
% 15.25/16.06 The proof is by contradiction:
% 15.25/16.06 Assume there is an interpretation so that the given
% 15.25/16.06 matrix evaluates to false. Then in each clause there
% 15.25/16.06 has to be at least one element that is false.
% 15.25/16.06
% 15.25/16.06 Then clause (2 ^ 0) under the substitution [[_130214], [[]]]
% 15.25/16.06 is false if at least one of the following is false:
% 15.25/16.06 [7 : x0 : [[]], 122 : p1 : [52 ^ [], 119 ^ [], 120 ^ []], 128 : y1 : [52 ^ [], 119 ^ [], 120 ^ []], 133 : z1 : [52 ^ [], 119 ^ [], 120 ^ []]]
% 15.25/16.06 1 Assume x0 : [] is false.
% 15.25/16.06 Then clause (4 ^ 3) is true.
% 15.25/16.06 2 Assume p1 : [52 ^ [], 119 ^ [], 140 ^ [], 120 ^ []] is false.
% 15.25/16.06 Then clause (143 ^ 3) under the substitution [[_135499], [120 ^ []]]
% 15.25/16.06 is false if at least one of the following is false:
% 15.25/16.06 [149 : y1 : [52 ^ [], 119 ^ [], 140 ^ [], 120 ^ []], 154 : z1 : [52 ^ [], 119 ^ [], 140 ^ [], 120 ^ []]]
% 15.25/16.06 2.1 Assume y1 : [52 ^ [], 119 ^ [], 140 ^ [], 120 ^ [], 120 ^ []] is false.
% 15.25/16.06 Then clause (152 ^ 6) under the substitution [[_135828], [120 ^ []]]
% 15.25/16.06 is true.
% 15.25/16.06 2.2 Assume z1 : [52 ^ [], 119 ^ [], 140 ^ [], 120 ^ [], 155 ^ [120 ^ []], 156 ^ [120 ^ []], 157 ^ [120 ^ []], 120 ^ []] is false.
% 15.25/16.06 Then clause (160 ^ 6) under the substitution [[_136149], [120 ^ []]]
% 15.25/16.06 is true.
% 15.25/16.06 3 Assume y1 : [52 ^ [], 119 ^ [], 120 ^ [], 120 ^ []] is false.
% 15.25/16.06 Then clause (131 ^ 5) under the substitution [[_135063], [120 ^ []]]
% 15.25/16.06 is true.
% 15.25/16.06 4 Assume z1 : [52 ^ [], 119 ^ [], 120 ^ [], 134 ^ [], 135 ^ [], 136 ^ [], 120 ^ []] is false.
% 15.25/16.06 Then clause (139 ^ 5) under the substitution [[_135342], [120 ^ []]]
% 15.25/16.06 is true.
% 15.25/16.06
% 15.25/16.06 Therefore there is no interpretation that makes the
% 15.25/16.06 given matrix false. Hence the given matrix is valid.
% 15.25/16.06 q.e.d.
% 15.25/16.06 ------------------------------------------------------
% 15.25/16.06 % SZS output end Proof for /export/starexec/sandbox/tmp/tmp.qFUf3JFESR/theBenchmark.p.qmf
% 15.25/16.06 % nanoCoP-M exiting
%------------------------------------------------------------------------------