Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
139   1,994   67   2.44
12   1,473   0.48   57
57     1.18  
1    
 
  DynamicDirectInterpreterTest       Line # 36 139 67 94.7% 0.94711536
 
  (51)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.logic.model;
17   
18    import java.io.File;
19    import java.lang.reflect.InvocationTargetException;
20   
21    import org.qedeq.base.io.UrlUtility;
22    import org.qedeq.base.test.DynamicGetter;
23    import org.qedeq.kernel.bo.module.KernelQedeqBo;
24    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
25    import org.qedeq.kernel.se.base.list.Element;
26    import org.qedeq.kernel.se.common.DefaultModuleAddress;
27    import org.qedeq.kernel.se.common.ModuleAddress;
28    import org.qedeq.kernel.se.common.ModuleContext;
29    import org.qedeq.kernel.xml.parser.BasicParser;
30   
31    /**
32    * For testing {@link org.qedeq.kernel.bo.logic.model.CalculateTruth}.
33    *
34    * @author Michael Meyling
35    */
 
36    public class DynamicDirectInterpreterTest extends QedeqBoTestCase {
37   
38    private DynamicDirectInterpreter interpreter;
39    private KernelQedeqBo prop;
40   
41    /**
42    * Constructor.
43    *
44    * @param model Dynamic to use.
45    */
 
46  51 toggle public DynamicDirectInterpreterTest() {
47  51 super();
48    }
49   
 
50  51 toggle public void setUp() throws Exception {
51  51 super.setUp();
52  51 final ModuleAddress address = getServices().getModuleAddress(
53    UrlUtility.toUrl(new File(getDocDir(), "math/qedeq_set_theory_v1.xml")));
54  51 prop = (KernelQedeqBo) getServices().loadModule(
55    address);
56  51 if (!getServices().checkWellFormedness(prop.getModuleAddress())) {
57  0 throw prop.getErrors();
58    }
59    }
60   
 
61  51 toggle public void tearDown() throws Exception {
62  51 interpreter = null;
63  51 super.tearDown();
64    }
65   
66    /**
67    * Test if given formula is a tautology. This is done by checking a default model and
68    * iterating through variable values.
69    *
70    * @param formula Formula.
71    * @return Is this formula a tautology according to our tests.
72    * @throws HeuristicException Evaluation failed.
73    */
 
74  51 toggle public boolean isTautology(final Element formula)
75    throws HeuristicException {
76  51 interpreter = new DynamicDirectInterpreter(prop, new FourDynamicModel()) {
77   
78    /** Start element for calculation. */
79    private Object startElement = formula;
80   
81    /** Module context. Here were are currently. */
82    private ModuleContext startContext = new ModuleContext(new DefaultModuleAddress());
83   
 
84  496673 toggle protected void setModuleContext(KernelQedeqBo qedeq) {
85  496673 super.setModuleContext(qedeq);
86  496673 startElement = qedeq.getQedeq();
87    // System.out.println("Startelement set to " + startElement.getClass());
88    }
89   
 
90  1399451 toggle protected void setLocationWithinModule(final String localContext) {
91  1399451 super.setLocationWithinModule(localContext);
92  1399451 if (localContext.equals(startContext.getLocationWithinModule())) {
93  1547 return;
94    }
95  1397904 if (!localContext.startsWith("getChapterList")) {
96  754935 startElement = formula;
97    }
98  1397904 String position
99    = getModuleContext().getLocationWithinModule().substring(startContext.getLocationWithinModule().length());
100  1397904 if (position.startsWith(".")) {
101  754935 position = position.substring(1);
102    }
103  1397904 try {
104    // System.out.println(position);
105    // System.out.println(DynamicGetter.get(startElement, position));
106  1397904 DynamicGetter.get(startElement, position);
107    // System.out.println(Latex2Utf8Parser.transform(null,
108    // prop.getElement2Latex().getLatex((Element) DynamicGetter.get(startElement, position)), 0));
109    } catch (IllegalAccessException e) {
110  0 System.out.println(position);
111  0 e.printStackTrace(System.out);
112  0 throw new RuntimeException(e);
113    } catch (InvocationTargetException e) {
114  0 System.out.println(position);
115    // System.out.println(startElement);
116  0 e.printStackTrace(System.out);
117  0 throw new RuntimeException(e);
118    } catch (RuntimeException e) {
119  0 System.out.println(position);
120    // System.out.println(startElement);
121  0 e.printStackTrace(System.out);
122  0 throw e;
123    }
124    }
125   
126    };
127  51 final ModuleContext context = new ModuleContext(new DefaultModuleAddress());
128  51 boolean result = true;
129  51 do {
130  1547 result &= interpreter.calculateValue(context, formula);
131    // System.out.println(interpreter.toString());
132  1547 } while (result && interpreter.next());
133  51 if (!result) {
134    // System.out.println(interpreter);
135    }
136    // System.out.println("interpretation finished - and result is = " + result);
137  51 interpreter = null;
138  51 return result;
139    }
140   
141    /**
142    * Function: isTautology(Element)
143    * Type: negative
144    * Data: --A
145    *
146    * @throws Exception Test failed.
147    */
 
148  1 toggle public void testTautology01() throws Exception {
149  1 final Element ele = BasicParser.createElement(
150    "<NOT><NOT><PREDVAR id=\"A\"/></NOT></NOT>");
151    // System.out.println(ele.toString());
152  1 assertFalse(isTautology(ele));
153    }
154   
155    /**
156    * Function: isTautology(Element)
157    * Type: positive
158    * Data: A v -A
159    *
160    * @throws Exception Test failed.
161    */
 
162  1 toggle public void testTautology02() throws Exception {
163  1 final Element ele = BasicParser.createElement(
164    "<OR><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></OR>");
165    // System.out.println(ele.toString());
166  1 assertTrue(isTautology(ele));
167    }
168   
169    /**
170    * Function: isTautology(Element)
171    * Type: negative
172    * Data: A n -A
173    *
174    * @throws Exception Test failed.
175    */
 
176  1 toggle public void testTautology03() throws Exception {
177  1 final Element ele = BasicParser.createElement(
178    "<AND><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></AND>");
179    // System.out.println(ele.toString());
180  1 assertFalse(isTautology(ele));
181    }
182   
183    /**
184    * Function: isTautology(Element)
185    * Type: negative
186    * Data: A => -A
187    *
188    * @throws Exception Test failed.
189    */
 
190  1 toggle public void testTautology04() throws Exception {
191  1 final Element ele = BasicParser.createElement(
192    "<IMPL><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></IMPL>");
193    // System.out.println(ele.toString());
194  1 assertFalse(isTautology(ele));
195    }
196   
197    /**
198    * Function: isTautology(Element)
199    * Type: negative
200    * Data: -A => A
201    *
202    * @throws Exception Test failed.
203    */
 
204  1 toggle public void testTautology05() throws Exception {
205  1 final Element ele = BasicParser.createElement(
206    "<IMPL><NOT><PREDVAR id=\"A\"/></NOT><PREDVAR id=\"A\"/></IMPL>");
207    // System.out.println(ele.toString());
208  1 assertFalse(isTautology(ele));
209    }
210   
211    /**
212    * Function: isTautology(Element)
213    * Type: positive
214    * Data: A => A
215    *
216    * @throws Exception Test failed.
217    */
 
218  1 toggle public void testTautology06() throws Exception {
219  1 final Element ele = BasicParser.createElement(
220    "<IMPL><PREDVAR id=\"A\"/><PREDVAR id=\"A\"/></IMPL>");
221    // System.out.println(ele.toString());
222  1 assertTrue(isTautology(ele));
223    }
224   
225    /**
226    * Function: isTautology(Element)
227    * Type: positive
228    * Data: A -> A
229    *
230    * @throws Exception Test failed.
231    */
 
232  1 toggle public void testTautology07() throws Exception {
233  1 final Element ele = BasicParser.createElement(
234    "<IMPL><PREDVAR id=\"A\"/><NOT><NOT><PREDVAR id=\"A\"/></NOT></NOT></IMPL>");
235    // System.out.println(ele.toString());
236  1 assertTrue(isTautology(ele));
237    }
238   
239    /**
240    * Function: isTautology(Element)
241    * Type: positive
242    * Data: A <-> A
243    *
244    * @throws Exception Test failed.
245    */
 
246  1 toggle public void testTautology08() throws Exception {
247  1 final Element ele = BasicParser.createElement(
248    "<EQUI><PREDVAR id=\"A\"/><NOT><NOT><PREDVAR id=\"A\"/></NOT></NOT></EQUI>");
249    // System.out.println(ele.toString());
250  1 assertTrue(isTautology(ele));
251    }
252   
253    /**
254    * Function: isTautology(Element)
255    * Type: positive
256    * Data: A -> B v A
257    *
258    * @throws Exception Test failed.
259    */
 
260  1 toggle public void testTautology09() throws Exception {
261  1 final Element ele = BasicParser.createElement(
262    "<IMPL><PREDVAR id=\"A\"/><OR><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></OR></IMPL>");
263    // System.out.println(ele.toString());
264  1 assertTrue(isTautology(ele));
265    }
266   
267    /**
268    * Function: isTautology(Element)
269    * Type: positive
270    * Data: A -> -B v A
271    *
272    * @throws Exception Test failed.
273    */
 
274  1 toggle public void testTautology10() throws Exception {
275  1 final Element ele = BasicParser.createElement(
276    "<IMPL><PREDVAR id=\"A\"/><OR><NOT><PREDVAR id=\"B\"/></NOT><PREDVAR id=\"A\"/></OR></IMPL>");
277    // System.out.println(ele.toString());
278  1 assertTrue(isTautology(ele));
279    }
280   
281    /**
282    * Function: isTautology(Element)
283    * Type: negative
284    * Data: A -> -B n A
285    *
286    * @throws Exception Test failed.
287    */
 
288  1 toggle public void testTautology11() throws Exception {
289  1 final Element ele = BasicParser.createElement(
290    "<IMPL><PREDVAR id=\"A\"/><AND><NOT><PREDVAR id=\"B\"/></NOT><PREDVAR id=\"A\"/></AND></IMPL>");
291    // System.out.println(ele.toString());
292  1 assertFalse(isTautology(ele));
293    }
294   
295    /**
296    * Function: isTautology(Element)
297    * Type: positive
298    * Data: A -> A v -A
299    *
300    * @throws Exception Test failed.
301    */
 
302  1 toggle public void testTautology12() throws Exception {
303  1 final Element ele = BasicParser.createElement(
304    "<IMPL><PREDVAR id=\"A\"/><OR><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></OR></IMPL>");
305    // System.out.println(ele.toString());
306  1 assertTrue(isTautology(ele));
307    }
308   
309    /**
310    * Function: isTautology(Element)
311    * Type: positive
312    * Data: A -> A v B v C v D v E v F v G v H v I v J
313    *
314    * @throws Exception Test failed.
315    */
 
316  1 toggle public void testTautology13() throws Exception {
317  1 final Element ele = BasicParser.createElement(
318    "<IMPL><PREDVAR id=\"A\"/><OR><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/><PREDVAR id=\"C\"/>"
319    + "<PREDVAR id=\"D\"/><PREDVAR id=\"E\"/><PREDVAR id=\"F\"/><PREDVAR id=\"G\"/>"
320    + "<PREDVAR id=\"H\"/><PREDVAR id=\"I\"/><PREDVAR id=\"J\"/></OR></IMPL>");
321    // System.out.println(ele.toString());
322  1 assertTrue(isTautology(ele));
323    }
324   
325    /**
326    * Function: isTautology(Element)
327    * Type: positive
328    * Data: A v B <-> B v A
329    *
330    * @throws Exception Test failed.
331    */
 
332  1 toggle public void testTautology14() throws Exception {
333  1 final Element ele = BasicParser.createElement(
334    "<EQUI><OR><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/></OR>"
335    + "<OR><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></OR></EQUI>");
336    // System.out.println(ele.toString());
337  1 assertTrue(isTautology(ele));
338    }
339   
340    /**
341    * Function: isTautology(Element)
342    * Type: positive
343    * Data: A n B <-> B n A
344    *
345    * @throws Exception Test failed.
346    */
 
347  1 toggle public void testTautology15() throws Exception {
348  1 final Element ele = BasicParser.createElement(
349    "<EQUI><AND><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/></AND>"
350    + "<AND><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></AND></EQUI>");
351    // System.out.println(ele.toString());
352  1 assertTrue(isTautology(ele));
353    }
354   
355    /**
356    * Function: isTautology(Element)
357    * Type: negative
358    * Data: A n B <-> B v A
359    *
360    * @throws Exception Test failed.
361    */
 
362  1 toggle public void testTautology16() throws Exception {
363  1 final Element ele = BasicParser.createElement(
364    "<EQUI><AND><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/></AND>"
365    + "<OR><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></OR></EQUI>");
366    // System.out.println(ele.toString());
367  1 assertFalse(isTautology(ele));
368    }
369   
370    /**
371    * Function: isTautology(Element)
372    * Type: positive
373    * Data: -A n B <-> -(-B v A)
374    *
375    * @throws Exception Test failed.
376    */
 
377  1 toggle public void testTautology17() throws Exception {
378  1 final Element ele = BasicParser.createElement(
379    "<EQUI><AND><NOT><PREDVAR id=\"A\"/></NOT><PREDVAR id=\"B\"/></AND>"
380    + "<NOT><OR><NOT><PREDVAR id=\"B\"/></NOT><PREDVAR id=\"A\"/></OR></NOT></EQUI>");
381    // System.out.println(ele.toString());
382  1 assertTrue(isTautology(ele));
383    }
384   
385    /**
386    * Function: isTautology(Element)
387    * Type: positive
388    * Data: A(x,y) <-> A(x,y)
389    *
390    * @throws Exception Test failed.
391    */
 
392  1 toggle public void testTautology18() throws Exception {
393  1 final Element ele = BasicParser.createElement(
394    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
395    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR></EQUI>");
396    // System.out.println(ele.toString());
397  1 assertTrue(isTautology(ele));
398    }
399   
400    /**
401    * Function: isTautology(Element)
402    * Type: negative
403    * Data: A(x,y) <-> A(y,x)
404    *
405    * @throws Exception Test failed.
406    */
 
407  1 toggle public void testTautology19() throws Exception {
408  1 final Element ele = BasicParser.createElement(
409    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
410    + "<PREDVAR id=\"A\"><VAR id=\"y\"/><VAR id=\"x\"/></PREDVAR></EQUI>");
411    // System.out.println(ele.toString());
412  1 assertFalse(isTautology(ele));
413    }
414   
415    /**
416    * Function: isTautology(Element)
417    * Type: negative
418    * Data: A(x,y) <-> A(x,x)
419    *
420    * @throws Exception Test failed.
421    */
 
422  1 toggle public void testTautology20() throws Exception {
423  1 final Element ele = BasicParser.createElement(
424    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
425    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"x\"/></PREDVAR></EQUI>");
426    // System.out.println(ele.toString());
427  1 assertFalse(isTautology(ele));
428    }
429   
430    /**
431    * Function: isTautology(Element)
432    * Type: negative
433    * Data: A(y) <-> A(x)
434    *
435    * @throws Exception Test failed.
436    */
 
437  1 toggle public void testTautology21() throws Exception {
438  1 final Element ele = BasicParser.createElement(
439    "<EQUI><PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR>"
440    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
441    // System.out.println(ele.toString());
442  1 assertFalse(isTautology(ele));
443    }
444   
445    /**
446    * Function: isTautology(Element)
447    * Type: negative
448    * Data: A(x, y) <-> A(x)
449    *
450    * @throws Exception Test failed.
451    */
 
452  1 toggle public void testTautology22() throws Exception {
453  1 final Element ele = BasicParser.createElement(
454    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
455    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
456    // System.out.println(ele.toString());
457  1 assertFalse(isTautology(ele));
458    }
459   
460    /**
461    * Function: isTautology(Element)
462    * Type: negative
463    * Data: A <-> A(x)
464    *
465    * @throws Exception Test failed.
466    */
 
467  1 toggle public void testTautology23() throws Exception {
468  1 final Element ele = BasicParser.createElement(
469    "<EQUI><PREDVAR id=\"A\"/>"
470    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
471    // System.out.println(ele.toString());
472  1 assertFalse(isTautology(ele));
473    }
474   
475    /**
476    * Function: isTautology(Element)
477    * Type: negative
478    * Data: A <-> B
479    *
480    * @throws Exception Test failed.
481    */
 
482  1 toggle public void testTautology24() throws Exception {
483  1 final Element ele = BasicParser.createElement(
484    "<EQUI><PREDVAR id=\"A\"/>"
485    + "<PREDVAR id=\"B\"/></EQUI>");
486    // System.out.println(ele.toString());
487  1 assertFalse(isTautology(ele));
488    }
489   
490    /**
491    * Function: isTautology(Element)
492    * Type: negative
493    * Data: A -> B
494    *
495    * @throws Exception Test failed.
496    */
 
497  1 toggle public void testTautology25() throws Exception {
498  1 final Element ele = BasicParser.createElement(
499    "<IMPL><PREDVAR id=\"A\"/>"
500    + "<PREDVAR id=\"B\"/></IMPL>");
501    // System.out.println(ele.toString());
502  1 assertFalse(isTautology(ele));
503    }
504   
505    /**
506    * Function: isTautology(Element)
507    * Type: negative
508    * Data: A -> A(x)
509    *
510    * @throws Exception Test failed.
511    */
 
512  1 toggle public void testTautology26() throws Exception {
513  1 final Element ele = BasicParser.createElement(
514    "<IMPL><PREDVAR id=\"A\"/>"
515    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></IMPL>");
516    // System.out.println(ele.toString());
517  1 assertFalse(isTautology(ele));
518    }
519   
520    /**
521    * Function: isTautology(Element)
522    * Type: positive
523    * Data: \forall x (A(x) -> A(x))
524    *
525    * @throws Exception Test failed.
526    */
 
527  1 toggle public void testTautology27() throws Exception {
528  1 final Element ele = BasicParser.createElement(
529    "<FORALL><VAR id=\"x\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
530    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></IMPL></FORALL>");
531    // System.out.println(ele.toString());
532  1 assertTrue(isTautology(ele));
533    }
534   
535    /**
536    * Function: isTautology(Element)
537    * Type: negative
538    * Data: \forall x \forall y (A(x) -> A(y))
539    *
540    * @throws Exception Test failed.
541    */
 
542  1 toggle public void testTautology28() throws Exception {
543  1 final Element ele = BasicParser.createElement(
544    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
545    + "<PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR></IMPL></FORALL></FORALL>");
546    // System.out.println(ele.toString());
547  1 assertFalse(isTautology(ele));
548    }
549   
550    /**
551    * Function: isTautology(Element)
552    * Type: positive
553    * Data: \forall x \forall y (A(x,y) -> A(x,y))
554    *
555    * @throws Exception Test failed.
556    */
 
557  1 toggle public void testTautology29() throws Exception {
558  1 final Element ele = BasicParser.createElement(
559    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
560    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR></IMPL></FORALL></FORALL>");
561    // System.out.println(ele.toString());
562  1 assertTrue(isTautology(ele));
563    }
564   
565    /**
566    * Function: isTautology(Element)
567    * Type: positive
568    * Data: \forall x \forall A(x,y): A(x,y))
569    *
570    * @throws Exception Test failed.
571    */
 
572  1 toggle public void testTautology30() throws Exception {
573  1 final Element ele = BasicParser.createElement(
574    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
575    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR></FORALL></FORALL>");
576    // System.out.println(ele.toString());
577  1 assertTrue(isTautology(ele));
578    }
579   
580    /**
581    * Function: isTautology(Element)
582    * Type: negative
583    * Data: \forall x \forall A(x,y): A(y,x))
584    *
585    * @throws Exception Test failed.
586    */
 
587  1 toggle public void testTautology31() throws Exception {
588  1 final Element ele = BasicParser.createElement(
589    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
590    + "<PREDVAR id=\"A\"><VAR id=\"y\"/><VAR id=\"x\"/></PREDVAR></FORALL></FORALL>");
591    // System.out.println(ele.toString());
592  1 assertFalse(isTautology(ele));
593    }
594   
595    /**
596    * Function: isTautology(Element)
597    * Type: positive
598    * Data: \forall x \exists y (A(x) -> A(y))
599    *
600    * @throws Exception Test failed.
601    */
 
602  1 toggle public void testTautology32() throws Exception {
603  1 final Element ele = BasicParser.createElement(
604    "<FORALL><VAR id=\"x\"/><EXISTS><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
605    + "<PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR></IMPL></EXISTS></FORALL>");
606    // System.out.println(ele.toString());
607  1 assertTrue(isTautology(ele));
608    }
609   
610    /**
611    * Function: isTautology(Element)
612    * Type: positive
613    * Data: \exists! y (x = y)
614    *
615    * @throws Exception Test failed.
616    */
 
617  1 toggle public void testTautology33() throws Exception {
618  1 final Element ele = BasicParser.createElement(
619    "<EXISTSU><VAR id=\"y\"/><PREDCON id=\"l.equal\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDCON>"
620    + "</EXISTSU>");
621    // System.out.println(ele.toString());
622  1 assertTrue(isTautology(ele));
623    }
624   
625    /**
626    * Function: isTautology(Element)
627    * Type: negative
628    * Data: \exists! y (y = y)
629    *
630    * @throws Exception Test failed.
631    */
 
632  1 toggle public void testTautology34() throws Exception {
633  1 final Element ele = BasicParser.createElement(
634    "<EXISTSU><VAR id=\"y\"/><PREDCON id=\"l.equal\"><VAR id=\"y\"/><VAR id=\"y\"/></PREDCON>"
635    + "</EXISTSU>");
636    // System.out.println(ele.toString());
637  1 assertFalse(isTautology(ele));
638    }
639   
640    /**
641    * Function: isTautology(Element)
642    * Type: positive
643    * Data: \exists y (y = y)
644    *
645    * @throws Exception Test failed.
646    */
 
647  1 toggle public void testTautology35() throws Exception {
648  1 final Element ele = BasicParser.createElement(
649    "<EXISTS><VAR id=\"y\"/><PREDCON id=\"equal\"><VAR id=\"y\"/><VAR id=\"y\"/></PREDCON>"
650    + "</EXISTS>");
651    // System.out.println(ele.toString());
652  1 assertTrue(isTautology(ele));
653    }
654   
655    /**
656    * Function: isTautology(Element)
657    * Type: positive
658    * Data: f(y) = f(y)
659    *
660    * @throws Exception Test failed.
661    */
 
662  1 toggle public void testTautology36() throws Exception {
663  1 final Element ele = BasicParser.createElement(
664    "<PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR>"
665    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON>");
666    // System.out.println(ele.toString());
667  1 assertTrue(isTautology(ele));
668    }
669   
670    /**
671    * Function: isTautology(Element)
672    * Type: negative
673    * Data: f(x) = f(y)
674    *
675    * @throws Exception Test failed.
676    */
 
677  1 toggle public void testTautology37() throws Exception {
678  1 final Element ele = BasicParser.createElement(
679    "<PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"x\"/></FUNVAR>"
680    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON>");
681    // System.out.println(ele.toString());
682  1 assertFalse(isTautology(ele));
683    }
684   
685    /**
686    * Function: isTautology(Element)
687    * Type: negative
688    * Data: \exists y f(x) = f(y)
689    *
690    * @throws Exception Test failed.
691    */
 
692  1 toggle public void testTautology38() throws Exception {
693  1 final Element ele = BasicParser.createElement(
694    "<EXISTS><VAR id=\"y\"/><PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"x\"/></FUNVAR>"
695    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON></EXISTS>");
696    // System.out.println(ele.toString());
697  1 assertTrue(isTautology(ele));
698    }
699   
700    /**
701    * Function: isTautology(Element)
702    * Type: positive
703    * Data: see qedeq_logic_v1.xml theorem:propositionalCalculus from 2010-09-26
704    *
705    * @throws Exception Test failed.
706    */
 
707  1 toggle public void testTautology39() throws Exception {
708  1 final Element ele = BasicParser.createElement(
709    "\n <AND>\n" +
710    "\n" +
711    "\n <PREDCON ref=\"TRUE\" />\n" +
712    "\n" +
713    "\n <NOT>\n" +
714    "\n <PREDCON ref=\"FALSE\" />\n" +
715    "\n </NOT>" +
716    "\n" +
717    "\n <IMPL>" +
718    "\n <PREDVAR id=\"A\" />" +
719    "\n <PREDVAR id=\"A\" />" +
720    "\n </IMPL>" +
721    "\n" +
722    "\n <EQUI>" +
723    "\n <PREDVAR id=\"A\" />" +
724    "\n <PREDVAR id=\"A\" />" +
725    "\n </EQUI>" +
726    "\n" +
727    "\n <EQUI>" +
728    "\n <OR>" +
729    "\n <PREDVAR id=\"A\" />" +
730    "\n <PREDVAR id=\"B\" />" +
731    "\n </OR>" +
732    "\n <OR>" +
733    "\n <PREDVAR id=\"B\" />" +
734    "\n <PREDVAR id=\"A\" />" +
735    "\n </OR>" +
736    "\n </EQUI>" +
737    "\n" +
738    "\n <EQUI>" +
739    "\n <AND>" +
740    "\n <PREDVAR id=\"A\" />" +
741    "\n <PREDVAR id=\"B\" />" +
742    "\n </AND>" +
743    "\n <AND>" +
744    "\n <PREDVAR id=\"B\" />" +
745    "\n <PREDVAR id=\"A\" />" +
746    "\n </AND>" +
747    "\n </EQUI>" +
748    "\n" +
749    "\n <IMPL>" +
750    "\n <AND>" +
751    "\n <PREDVAR id=\"A\" />" +
752    "\n <PREDVAR id=\"B\" />" +
753    "\n </AND>" +
754    "\n <PREDVAR id=\"A\" />" +
755    "\n </IMPL>" +
756    "\n" +
757    "\n <EQUI>" +
758    "\n <EQUI>" +
759    "\n <PREDVAR id=\"A\" />" +
760    "\n <PREDVAR id=\"B\" />" +
761    "\n </EQUI>" +
762    "\n <EQUI>" +
763    "\n <PREDVAR id=\"B\" />" +
764    "\n <PREDVAR id=\"A\" />" +
765    "\n </EQUI>" +
766    "\n </EQUI>" +
767    "\n" +
768    "\n <EQUI>" +
769    "\n <OR>" +
770    "\n <PREDVAR id=\"A\" />" +
771    "\n <OR>" +
772    "\n <PREDVAR id=\"B\" />" +
773    "\n <PREDVAR id=\"C\" />" +
774    "\n </OR>" +
775    "\n </OR>" +
776    "\n <OR>" +
777    "\n <OR>" +
778    "\n <PREDVAR id=\"A\" />" +
779    "\n <PREDVAR id=\"B\" />" +
780    "\n </OR>" +
781    "\n <PREDVAR id=\"C\" />" +
782    "\n </OR>" +
783    "\n </EQUI>" +
784    "\n" +
785    "\n <EQUI>" +
786    "\n <AND>" +
787    "\n <PREDVAR id=\"A\" />" +
788    "\n <AND>" +
789    "\n <PREDVAR id=\"B\" />" +
790    "\n <PREDVAR id=\"C\" />" +
791    "\n </AND>" +
792    "\n </AND>" +
793    "\n <AND>" +
794    "\n <AND>" +
795    "\n <PREDVAR id=\"A\" />" +
796    "\n <PREDVAR id=\"B\" />" +
797    "\n </AND>" +
798    "\n <PREDVAR id=\"C\" />" +
799    "\n </AND>" +
800    "\n </EQUI>" +
801    "\n" +
802    "\n <EQUI>" +
803    "\n <PREDVAR id=\"A\" />" +
804    "\n <OR>" +
805    "\n <PREDVAR id=\"A\" />" +
806    "\n <PREDVAR id=\"A\" />" +
807    "\n </OR>" +
808    "\n </EQUI>" +
809    "\n" +
810    "\n <EQUI>" +
811    "\n <PREDVAR id=\"A\" />" +
812    "\n <AND>" +
813    "\n <PREDVAR id=\"A\" />" +
814    "\n <PREDVAR id=\"A\" />" +
815    "\n </AND>" +
816    "\n </EQUI>" +
817    "\n" +
818    "\n <EQUI>" +
819    "\n <PREDVAR id=\"A\" />" +
820    "\n <NOT>" +
821    "\n <NOT>" +
822    "\n <PREDVAR id=\"A\" />" +
823    "\n </NOT>" +
824    "\n </NOT>" +
825    "\n </EQUI>" +
826    "\n" +
827    "\n <EQUI>" +
828    "\n <IMPL>" +
829    "\n <PREDVAR id=\"A\" />" +
830    "\n <PREDVAR id=\"B\" />" +
831    "\n </IMPL>" +
832    "\n <IMPL>" +
833    "\n <NOT>" +
834    "\n <PREDVAR id=\"B\" />" +
835    "\n </NOT>" +
836    "\n <NOT>" +
837    "\n <PREDVAR id=\"A\" />" +
838    "\n </NOT>" +
839    "\n </IMPL>" +
840    "\n </EQUI>" +
841    "\n" +
842    "\n <EQUI>" +
843    "\n <EQUI>" +
844    "\n <PREDVAR id=\"A\" />" +
845    "\n <PREDVAR id=\"B\" />" +
846    "\n </EQUI>" +
847    "\n <EQUI>" +
848    "\n <NOT>" +
849    "\n <PREDVAR id=\"A\" />" +
850    "\n </NOT>" +
851    "\n <NOT>" +
852    "\n <PREDVAR id=\"B\" />" +
853    "\n </NOT>" +
854    "\n </EQUI>" +
855    "\n </EQUI>" +
856    "\n" +
857    "\n <EQUI>" +
858    "\n <IMPL>" +
859    "\n <PREDVAR id=\"A\" />" +
860    "\n <IMPL>" +
861    "\n <PREDVAR id=\"B\" />" +
862    "\n <PREDVAR id=\"C\" />" +
863    "\n </IMPL>" +
864    "\n </IMPL>" +
865    "\n <IMPL>" +
866    "\n <PREDVAR id=\"B\" />" +
867    "\n <IMPL>" +
868    "\n <PREDVAR id=\"A\" />" +
869    "\n <PREDVAR id=\"C\" />" +
870    "\n </IMPL>" +
871    "\n </IMPL>" +
872    "\n </EQUI>" +
873    "\n" +
874    "\n <EQUI>" +
875    "\n <NOT>" +
876    "\n <OR>" +
877    "\n <PREDVAR id=\"A\" />" +
878    "\n <PREDVAR id=\"B\" />" +
879    "\n </OR>" +
880    "\n </NOT>" +
881    "\n <AND>" +
882    "\n <NOT>" +
883    "\n <PREDVAR id=\"A\" />" +
884    "\n </NOT>" +
885    "\n <NOT>" +
886    "\n <PREDVAR id=\"B\" />" +
887    "\n </NOT>" +
888    "\n </AND>" +
889    "\n </EQUI>" +
890    "\n" +
891    "\n <EQUI>" +
892    "\n <NOT>" +
893    "\n <AND>" +
894    "\n <PREDVAR id=\"A\" />" +
895    "\n <PREDVAR id=\"B\" />" +
896    "\n </AND>" +
897    "\n </NOT>" +
898    "\n <OR>" +
899    "\n <NOT>" +
900    "\n <PREDVAR id=\"A\" />" +
901    "\n </NOT>" +
902    "\n <NOT>" +
903    "\n <PREDVAR id=\"B\" />" +
904    "\n </NOT>" +
905    "\n </OR>" +
906    "\n </EQUI>" +
907    "\n" +
908    "\n <EQUI>" +
909    "\n <OR>" +
910    "\n <PREDVAR id=\"A\" />" +
911    "\n <AND>" +
912    "\n <PREDVAR id=\"B\" />" +
913    "\n <PREDVAR id=\"C\" />" +
914    "\n </AND>" +
915    "\n </OR>" +
916    "\n <AND>" +
917    "\n <OR>" +
918    "\n <PREDVAR id=\"A\" />" +
919    "\n <PREDVAR id=\"B\" />" +
920    "\n </OR>" +
921    "\n <OR>" +
922    "\n <PREDVAR id=\"A\" />" +
923    "\n <PREDVAR id=\"C\" />" +
924    "\n </OR>" +
925    "\n </AND>" +
926    "\n </EQUI>" +
927    "\n" +
928    "\n <EQUI>" +
929    "\n <AND>" +
930    "\n <PREDVAR id=\"A\" />" +
931    "\n <OR>" +
932    "\n <PREDVAR id=\"B\" />" +
933    "\n <PREDVAR id=\"C\" />" +
934    "\n </OR>" +
935    "\n </AND>" +
936    "\n <OR>" +
937    "\n <AND>" +
938    "\n <PREDVAR id=\"A\" />" +
939    "\n <PREDVAR id=\"B\" />" +
940    "\n </AND>" +
941    "\n <AND>" +
942    "\n <PREDVAR id=\"A\" />" +
943    "\n <PREDVAR id=\"C\" />" +
944    "\n </AND>" +
945    "\n </OR>" +
946    "\n </EQUI>" +
947    "\n" +
948    "\n <EQUI>" +
949    "\n <AND>" +
950    "\n <PREDVAR id=\"A\" />" +
951    "\n <PREDCON ref=\"TRUE\" />" +
952    "\n </AND>" +
953    "\n <PREDVAR id=\"A\" />" +
954    "\n </EQUI>" +
955    "\n" +
956    "\n <EQUI>" +
957    "\n <AND>" +
958    "\n <PREDVAR id=\"A\" />" +
959    "\n <PREDCON ref=\"FALSE\" />" +
960    "\n </AND>" +
961    "\n <PREDCON ref=\"FALSE\" />" +
962    "\n </EQUI>" +
963    "\n" +
964    "\n <EQUI>" +
965    "\n <OR>" +
966    "\n <PREDVAR id=\"A\" />" +
967    "\n <PREDCON ref=\"TRUE\" />" +
968    "\n </OR>" +
969    "\n <PREDCON ref=\"TRUE\" />" +
970    "\n </EQUI>" +
971    "\n" +
972    "\n <EQUI>" +
973    "\n <OR>" +
974    "\n <PREDVAR id=\"A\" />" +
975    "\n <PREDCON ref=\"FALSE\" />" +
976    "\n </OR>" +
977    "\n <PREDVAR id=\"A\" />" +
978    "\n </EQUI>" +
979    "\n" +
980    "\n <EQUI>" +
981    "\n <OR>" +
982    "\n <PREDVAR id=\"A\" />" +
983    "\n <NOT>" +
984    "\n <PREDVAR id=\"A\" />" +
985    "\n </NOT>" +
986    "\n </OR>" +
987    "\n <PREDCON ref=\"TRUE\" />" +
988    "\n </EQUI>" +
989    "\n" +
990    "\n <EQUI>" +
991    "\n <AND>" +
992    "\n <PREDVAR id=\"A\" />" +
993    "\n <NOT>" +
994    "\n <PREDVAR id=\"A\" />" +
995    "\n </NOT>" +
996    "\n </AND>" +
997    "\n <PREDCON ref=\"FALSE\" />" +
998    "\n </EQUI>" +
999    "\n" +
1000    "\n <EQUI>" +
1001    "\n <IMPL>" +
1002    "\n <PREDCON ref=\"TRUE\" />" +
1003    "\n <PREDVAR id=\"A\" />" +
1004    "\n </IMPL>" +
1005    "\n <PREDVAR id=\"A\" />" +
1006    "\n </EQUI>" +
1007    "\n" +
1008    "\n <EQUI>" +
1009    "\n <IMPL>" +
1010    "\n <PREDCON ref=\"FALSE\" />" +
1011    "\n <PREDVAR id=\"A\" />" +
1012    "\n </IMPL>" +
1013    "\n <PREDCON ref=\"TRUE\" />" +
1014    "\n </EQUI>" +
1015    "\n" +
1016    "\n <EQUI>" +
1017    "\n <IMPL>" +
1018    "\n <PREDVAR id=\"A\" />" +
1019    "\n <PREDCON ref=\"FALSE\" />" +
1020    "\n </IMPL>" +
1021    "\n <NOT>" +
1022    "\n <PREDVAR id=\"A\" />" +
1023    "\n </NOT>" +
1024    "\n </EQUI>" +
1025    "\n" +
1026    "\n <EQUI>" +
1027    "\n <IMPL>" +
1028    "\n <PREDVAR id=\"A\" />" +
1029    "\n <PREDCON ref=\"TRUE\" />" +
1030    "\n </IMPL>" +
1031    "\n <PREDCON ref=\"TRUE\" />" +
1032    "\n </EQUI>" +
1033    "\n" +
1034    "\n <EQUI>" +
1035    "\n <EQUI>" +
1036    "\n <PREDVAR id=\"A\" />" +
1037    "\n <PREDCON ref=\"TRUE\" />" +
1038    "\n </EQUI>" +
1039    "\n <PREDVAR id=\"A\" />" +
1040    "\n </EQUI>" +
1041    "\n " +
1042    "\n <IMPL>" +
1043    "\n <AND>" +
1044    "\n <IMPL>" +
1045    "\n <PREDVAR id=\"A\" />" +
1046    "\n <PREDVAR id=\"B\" />" +
1047    "\n </IMPL>" +
1048    "\n <IMPL>" +
1049    "\n <PREDVAR id=\"B\" />" +
1050    "\n <PREDVAR id=\"C\" />" +
1051    "\n </IMPL>" +
1052    "\n </AND>" +
1053    "\n <IMPL>" +
1054    "\n <PREDVAR id=\"A\" />" +
1055    "\n <PREDVAR id=\"C\" />" +
1056    "\n </IMPL>" +
1057    "\n </IMPL>" +
1058    "\n" +
1059    "\n <IMPL>" +
1060    "\n <AND>" +
1061    "\n <EQUI>" +
1062    "\n <PREDVAR id=\"A\" />" +
1063    "\n <PREDVAR id=\"B\" />" +
1064    "\n </EQUI>" +
1065    "\n <EQUI>" +
1066    "\n <PREDVAR id=\"C\" />" +
1067    "\n <PREDVAR id=\"B\" />" +
1068    "\n </EQUI>" +
1069    "\n </AND>" +
1070    "\n <EQUI>" +
1071    "\n <PREDVAR id=\"A\" />" +
1072    "\n <PREDVAR id=\"C\" />" +
1073    "\n </EQUI>" +
1074    "\n </IMPL>" +
1075    "\n" +
1076    "\n <EQUI>" +
1077    "\n <EQUI>" +
1078    "\n <AND>" +
1079    "\n <PREDVAR id=\"A\" />" +
1080    "\n <PREDVAR id=\"B\" />" +
1081    "\n </AND>" +
1082    "\n <AND>" +
1083    "\n <PREDVAR id=\"A\" />" +
1084    "\n <PREDVAR id=\"C\" />" +
1085    "\n </AND>" +
1086    "\n </EQUI>" +
1087    "\n <IMPL>" +
1088    "\n <PREDVAR id=\"A\" />" +
1089    "\n <EQUI>" +
1090    "\n <PREDVAR id=\"B\" />" +
1091    "\n <PREDVAR id=\"C\" />" +
1092    "\n </EQUI>" +
1093    "\n </IMPL>" +
1094    "\n </EQUI>" +
1095    "\n" +
1096    "\n <EQUI>" +
1097    "\n <EQUI>" +
1098    "\n <AND>" +
1099    "\n <PREDVAR id=\"A\" />" +
1100    "\n <PREDVAR id=\"B\" />" +
1101    "\n </AND>" +
1102    "\n <AND>" +
1103    "\n <PREDVAR id=\"A\" />" +
1104    "\n <NOT>" +
1105    "\n <PREDVAR id=\"B\" />" +
1106    "\n </NOT>" +
1107    "\n </AND>" +
1108    "\n </EQUI>" +
1109    "\n <NOT>" +
1110    "\n <PREDVAR id=\"A\" />" +
1111    "\n </NOT>" +
1112    "\n </EQUI>" +
1113    "\n" +
1114    "\n <EQUI>" +
1115    "\n <EQUI>" +
1116    "\n <PREDVAR id=\"A\" />" +
1117    "\n <AND>" +
1118    "\n <PREDVAR id=\"A\" />" +
1119    "\n <PREDVAR id=\"B\" />" +
1120    "\n </AND>" +
1121    "\n </EQUI>" +
1122    "\n <IMPL>" +
1123    "\n <PREDVAR id=\"A\" />" +
1124    "\n <PREDVAR id=\"B\" />" +
1125    "\n </IMPL>" +
1126    "\n </EQUI>" +
1127    "\n" +
1128    "\n <IMPL>" +
1129    "\n <IMPL>" +
1130    "\n <PREDVAR id=\"A\" />" +
1131    "\n <PREDVAR id=\"B\" />" +
1132    "\n </IMPL>" +
1133    "\n <IMPL>" +
1134    "\n <AND>" +
1135    "\n <PREDVAR id=\"A\" />" +
1136    "\n <PREDVAR id=\"C\" />" +
1137    "\n </AND>" +
1138    "\n <AND>" +
1139    "\n <PREDVAR id=\"B\" />" +
1140    "\n <PREDVAR id=\"C\" />" +
1141    "\n </AND>" +
1142    "\n </IMPL>" +
1143    "\n </IMPL>" +
1144    "\n" +
1145    "\n <IMPL>" +
1146    "\n <EQUI>" +
1147    "\n <PREDVAR id=\"A\" />" +
1148    "\n <PREDVAR id=\"B\" />" +
1149    "\n </EQUI>" +
1150    "\n <EQUI>" +
1151    "\n <AND>" +
1152    "\n <PREDVAR id=\"A\" />" +
1153    "\n <PREDVAR id=\"C\" />" +
1154    "\n </AND>" +
1155    "\n <AND>" +
1156    "\n <PREDVAR id=\"B\" />" +
1157    "\n <PREDVAR id=\"C\" />" +
1158    "\n </AND>" +
1159    "\n </EQUI>" +
1160    "\n </IMPL>" +
1161    "\n" +
1162    "\n </AND>" +
1163    "\n");
1164    // System.out.println(ele.toString());
1165  1 assertTrue(isTautology(ele));
1166    }
1167   
1168    /**
1169    * Function: isTautology(Element)
1170    * Type: positive
1171    * Data: f(y) = f(y)
1172    *
1173    * @throws Exception Test failed.
1174    */
 
1175  1 toggle public void testTautology40() throws Exception {
1176  1 final Element ele = BasicParser.createElement(
1177    " <AND>"
1178    + "\n "
1179    + "\n <IMPL>"
1180    + "\n <FORALL>"
1181    + "\n <VAR id=\"x\" />"
1182    + "\n <IMPL>"
1183    + "\n <PREDVAR id=\"\\phi\">"
1184    + "\n <VAR id=\"x\" />"
1185    + "\n </PREDVAR>"
1186    + "\n <PREDVAR id=\"\\psi\">"
1187    + "\n <VAR id=\"x\" />"
1188    + "\n </PREDVAR>"
1189    + "\n </IMPL>"
1190    + "\n </FORALL>"
1191    + "\n <IMPL>"
1192    + "\n <FORALL>"
1193    + "\n <VAR id=\"x\" />"
1194    + "\n <PREDVAR id=\"\\phi\">"
1195    + "\n <VAR id=\"x\" />"
1196    + "\n </PREDVAR>"
1197    + "\n </FORALL>"
1198    + "\n <FORALL>"
1199    + "\n <VAR id=\"x\" />"
1200    + "\n <PREDVAR id=\"\\psi\">"
1201    + "\n <VAR id=\"x\" />"
1202    + "\n </PREDVAR>"
1203    + "\n </FORALL>"
1204    + "\n </IMPL>"
1205    + "\n </IMPL>"
1206    + "\n"
1207    + "\n <IMPL>"
1208    + "\n <FORALL>"
1209    + "\n <VAR id=\"x\" />"
1210    + "\n <IMPL>"
1211    + "\n <PREDVAR id=\"\\phi\">"
1212    + "\n <VAR id=\"x\" />"
1213    + "\n </PREDVAR>"
1214    + "\n <PREDVAR id=\"\\psi\">"
1215    + "\n <VAR id=\"x\" />"
1216    + "\n </PREDVAR>"
1217    + "\n </IMPL>"
1218    + "\n </FORALL>"
1219    + "\n <IMPL>"
1220    + "\n <EXISTS>"
1221    + "\n <VAR id=\"x\" />"
1222    + "\n <PREDVAR id=\"\\phi\">"
1223    + "\n <VAR id=\"x\" />"
1224    + "\n </PREDVAR>"
1225    + "\n </EXISTS>"
1226    + "\n <EXISTS>"
1227    + "\n <VAR id=\"x\" />"
1228    + "\n <PREDVAR id=\"\\psi\">"
1229    + "\n <VAR id=\"x\" />"
1230    + "\n </PREDVAR>"
1231    + "\n </EXISTS>"
1232    + "\n </IMPL>"
1233    + "\n </IMPL>"
1234    + "\n"
1235    + "\n <IMPL>"
1236    + "\n <EXISTS>"
1237    + "\n <VAR id=\"x\" />"
1238    + "\n <AND>"
1239    + "\n <PREDVAR id=\"\\phi\">"
1240    + "\n <VAR id=\"x\" />"
1241    + "\n </PREDVAR>"
1242    + "\n <PREDVAR id=\"\\psi\">"
1243    + "\n <VAR id=\"x\" />"
1244    + "\n </PREDVAR>"
1245    + "\n </AND>"
1246    + "\n </EXISTS>"
1247    + "\n <AND>"
1248    + "\n <EXISTS>"
1249    + "\n <VAR id=\"x\" />"
1250    + "\n <PREDVAR id=\"\\phi\">"
1251    + "\n <VAR id=\"x\" />"
1252    + "\n </PREDVAR>"
1253    + "\n </EXISTS>"
1254    + "\n <EXISTS>"
1255    + "\n <VAR id=\"x\" />"
1256    + "\n <PREDVAR id=\"\\psi\">"
1257    + "\n <VAR id=\"x\" />"
1258    + "\n </PREDVAR>"
1259    + "\n </EXISTS>"
1260    + "\n </AND>"
1261    + "\n </IMPL>"
1262    + "\n"
1263    + "\n <IMPL>"
1264    + "\n <OR>"
1265    + "\n <FORALL>"
1266    + "\n <VAR id=\"x\" />"
1267    + "\n <PREDVAR id=\"\\psi\">"
1268    + "\n <VAR id=\"x\" />"
1269    + "\n </PREDVAR>"
1270    + "\n </FORALL>"
1271    + "\n <FORALL>"
1272    + "\n <VAR id=\"x\" />"
1273    + "\n <PREDVAR id=\"\\psi\">"
1274    + "\n <VAR id=\"x\" />"
1275    + "\n </PREDVAR>"
1276    + "\n </FORALL>"
1277    + "\n </OR>"
1278    + "\n <FORALL>"
1279    + "\n <VAR id=\"x\" />"
1280    + "\n <OR>"
1281    + "\n <PREDVAR id=\"\\phi\">"
1282    + "\n <VAR id=\"x\" />"
1283    + "\n </PREDVAR>"
1284    + "\n <PREDVAR id=\"\\psi\">"
1285    + "\n <VAR id=\"x\" />"
1286    + "\n </PREDVAR>"
1287    + "\n </OR>"
1288    + "\n </FORALL>"
1289    + "\n </IMPL>"
1290    + "\n"
1291    + "\n <EQUI>"
1292    + "\n <EXISTS>"
1293    + "\n <VAR id=\"x\" />"
1294    + "\n <OR>"
1295    + "\n <PREDVAR id=\"\\phi\">"
1296    + "\n <VAR id=\"x\" />"
1297    + "\n </PREDVAR>"
1298    + "\n <PREDVAR id=\"\\psi\">"
1299    + "\n <VAR id=\"x\" />"
1300    + "\n </PREDVAR>"
1301    + "\n </OR>"
1302    + "\n </EXISTS>"
1303    + "\n <OR>"
1304    + "\n <EXISTS>"
1305    + "\n <VAR id=\"x\" />"
1306    + "\n <PREDVAR id=\"\\phi\">"
1307    + "\n <VAR id=\"x\" />"
1308    + "\n </PREDVAR>"
1309    + "\n </EXISTS>"
1310    + "\n <EXISTS>"
1311    + "\n <VAR id=\"x\" />"
1312    + "\n <PREDVAR id=\"\\psi\">"
1313    + "\n <VAR id=\"x\" />"
1314    + "\n </PREDVAR>"
1315    + "\n </EXISTS>"
1316    + "\n </OR>"
1317    + "\n </EQUI>"
1318    + "\n"
1319    + "\n <EQUI>"
1320    + "\n <FORALL>"
1321    + "\n <VAR id=\"x\" />"
1322    + "\n <AND>"
1323    + "\n <PREDVAR id=\"\\phi\">"
1324    + "\n <VAR id=\"x\" />"
1325    + "\n </PREDVAR>"
1326    + "\n <PREDVAR id=\"\\psi\">"
1327    + "\n <VAR id=\"x\" />"
1328    + "\n </PREDVAR>"
1329    + "\n </AND>"
1330    + "\n </FORALL>"
1331    + "\n <AND>"
1332    + "\n <FORALL>"
1333    + "\n <VAR id=\"x\" />"
1334    + "\n <PREDVAR id=\"\\phi\">"
1335    + "\n <VAR id=\"x\" />"
1336    + "\n </PREDVAR>"
1337    + "\n </FORALL>"
1338    + "\n <FORALL>"
1339    + "\n <VAR id=\"x\" />"
1340    + "\n <PREDVAR id=\"\\psi\">"
1341    + "\n <VAR id=\"x\" />"
1342    + "\n </PREDVAR>"
1343    + "\n </FORALL>"
1344    + "\n </AND>"
1345    + "\n </EQUI>"
1346    + "\n"
1347    + "\n <EQUI>"
1348    + "\n <FORALL>"
1349    + "\n <VAR id=\"x\" />"
1350    + "\n <FORALL>"
1351    + "\n <VAR id=\"y\" />"
1352    + "\n <PREDVAR id=\"\\phi\">"
1353    + "\n <VAR id=\"x\" />"
1354    + "\n <VAR id=\"y\" />"
1355    + "\n </PREDVAR>"
1356    + "\n </FORALL>"
1357    + "\n </FORALL>"
1358    + "\n <FORALL>"
1359    + "\n <VAR id=\"y\" />"
1360    + "\n <FORALL>"
1361    + "\n <VAR id=\"x\" />"
1362    + "\n <PREDVAR id=\"\\phi\">"
1363    + "\n <VAR id=\"x\" />"
1364    + "\n <VAR id=\"y\" />"
1365    + "\n </PREDVAR>"
1366    + "\n </FORALL>"
1367    + "\n </FORALL>"
1368    + "\n </EQUI>"
1369    + "\n"
1370    + "\n <EQUI>"
1371    + "\n <EXISTS>"
1372    + "\n <VAR id=\"x\" />"
1373    + "\n <EXISTS>"
1374    + "\n <VAR id=\"y\" />"
1375    + "\n <PREDVAR id=\"\\phi\">"
1376    + "\n <VAR id=\"x\" />"
1377    + "\n <VAR id=\"y\" />"
1378    + "\n </PREDVAR>"
1379    + "\n </EXISTS>"
1380    + "\n </EXISTS>"
1381    + "\n <EXISTS>"
1382    + "\n <VAR id=\"y\" />"
1383    + "\n <EXISTS>"
1384    + "\n <VAR id=\"x\" />"
1385    + "\n <PREDVAR id=\"\\phi\">"
1386    + "\n <VAR id=\"x\" />"
1387    + "\n <VAR id=\"y\" />"
1388    + "\n </PREDVAR>"
1389    + "\n </EXISTS>"
1390    + "\n </EXISTS>"
1391    + "\n </EQUI>"
1392    + "\n"
1393    + "\n <IMPL>"
1394    + "\n <FORALL>"
1395    + "\n <VAR id=\"x\" />"
1396    + "\n <IMPL>"
1397    + "\n <PREDVAR id=\"\\phi\">"
1398    + "\n <VAR id=\"x\" />"
1399    + "\n </PREDVAR>"
1400    + "\n <PREDVAR id=\"A\" />"
1401    + "\n </IMPL>"
1402    + "\n </FORALL>"
1403    + "\n <IMPL>"
1404    + "\n <FORALL>"
1405    + "\n <VAR id=\"x\" />"
1406    + "\n <PREDVAR id=\"\\phi\">"
1407    + "\n <VAR id=\"x\" />"
1408    + "\n </PREDVAR>"
1409    + "\n </FORALL>"
1410    + "\n <PREDVAR id=\"A\" />"
1411    + "\n </IMPL>"
1412    + "\n </IMPL>"
1413    + "\n"
1414    + "\n <EQUI>"
1415    + "\n <FORALL>"
1416    + "\n <VAR id=\"x\" />"
1417    + "\n <IMPL>"
1418    + "\n <PREDVAR id=\"A\" />"
1419    + "\n <PREDVAR id=\"\\phi\">"
1420    + "\n <VAR id=\"x\" />"
1421    + "\n </PREDVAR>"
1422    + "\n </IMPL>"
1423    + "\n </FORALL>"
1424    + "\n <IMPL>"
1425    + "\n <PREDVAR id=\"A\" />"
1426    + "\n <FORALL>"
1427    + "\n <VAR id=\"x\" />"
1428    + "\n <PREDVAR id=\"\\phi\">"
1429    + "\n <VAR id=\"x\" />"
1430    + "\n </PREDVAR>"
1431    + "\n </FORALL>"
1432    + "\n </IMPL>"
1433    + "\n </EQUI>"
1434    + "\n"
1435    + "\n <EQUI>"
1436    + "\n <FORALL>"
1437    + "\n <VAR id=\"x\" />"
1438    + "\n <AND>"
1439    + "\n <PREDVAR id=\"\\phi\">"
1440    + "\n <VAR id=\"x\" />"
1441    + "\n </PREDVAR>"
1442    + "\n <PREDVAR id=\"A\" />"
1443    + "\n </AND>"
1444    + "\n </FORALL>"
1445    + "\n <AND>"
1446    + "\n <FORALL>"
1447    + "\n <VAR id=\"x\" />"
1448    + "\n <PREDVAR id=\"\\phi\">"
1449    + "\n <VAR id=\"x\" />"
1450    + "\n </PREDVAR>"
1451    + "\n </FORALL>"
1452    + "\n <PREDVAR id=\"A\" />"
1453    + "\n </AND>"
1454    + "\n </EQUI>"
1455    + "\n"
1456    + "\n <EQUI>"
1457    + "\n <FORALL>"
1458    + "\n <VAR id=\"x\" />"
1459    + "\n <OR>"
1460    + "\n <PREDVAR id=\"\\phi\">"
1461    + "\n <VAR id=\"x\" />"
1462    + "\n </PREDVAR>"
1463    + "\n <PREDVAR id=\"A\" />"
1464    + "\n </OR>"
1465    + "\n </FORALL>"
1466    + "\n <OR>"
1467    + "\n <FORALL>"
1468    + "\n <VAR id=\"x\" />"
1469    + "\n <PREDVAR id=\"\\phi\">"
1470    + "\n <VAR id=\"x\" />"
1471    + "\n </PREDVAR>"
1472    + "\n </FORALL>"
1473    + "\n <PREDVAR id=\"A\" />"
1474    + "\n </OR>"
1475    + "\n </EQUI>"
1476    + "\n"
1477    + "\n <IMPL>"
1478    + "\n <FORALL>"
1479    + "\n <VAR id=\"x\" />"
1480    + "\n <EQUI>"
1481    + "\n <PREDVAR id=\"\\phi\">"
1482    + "\n <VAR id=\"x\" />"
1483    + "\n </PREDVAR>"
1484    + "\n <PREDVAR id=\"A\" />"
1485    + "\n </EQUI>"
1486    + "\n </FORALL>"
1487    + "\n <EQUI>"
1488    + "\n <FORALL>"
1489    + "\n <VAR id=\"x\" />"
1490    + "\n <PREDVAR id=\"\\phi\">"
1491    + "\n <VAR id=\"x\" />"
1492    + "\n </PREDVAR>"
1493    + "\n </FORALL>"
1494    + "\n <PREDVAR id=\"A\" />"
1495    + "\n </EQUI>"
1496    + "\n </IMPL>"
1497    + "\n"
1498    + "\n <IMPL>"
1499    + "\n <FORALL>"
1500    + "\n <VAR id=\"x\" />"
1501    + "\n <EQUI>"
1502    + "\n <PREDVAR id=\"\\phi\">"
1503    + "\n <VAR id=\"x\" />"
1504    + "\n </PREDVAR>"
1505    + "\n <PREDVAR id=\"\\psi\">"
1506    + "\n <VAR id=\"x\" />"
1507    + "\n </PREDVAR>"
1508    + "\n </EQUI>"
1509    + "\n </FORALL>"
1510    + "\n <EQUI>"
1511    + "\n <FORALL>"
1512    + "\n <VAR id=\"x\" />"
1513    + "\n <PREDVAR id=\"\\phi\">"
1514    + "\n <VAR id=\"x\" />"
1515    + "\n </PREDVAR>"
1516    + "\n </FORALL>"
1517    + "\n <FORALL>"
1518    + "\n <VAR id=\"x\" />"
1519    + "\n <PREDVAR id=\"\\psi\">"
1520    + "\n <VAR id=\"x\" />"
1521    + "\n </PREDVAR>"
1522    + "\n </FORALL>"
1523    + "\n </EQUI>"
1524    + "\n </IMPL>"
1525    + "\n"
1526    + "\n </AND>"
1527    + "\n"
1528    );
1529    // System.out.println(ele.toString());
1530  1 assertTrue(isTautology(ele));
1531    }
1532   
1533    /**
1534    * Function: isTautology(Element)
1535    * Type: negative
1536    * Data: \forall x (\phi(x) <-> A) <-> (\forall x (\phi(x)) <-> A)
1537    * \forall x ( 2 | x) <-> F) <-> (\forall x (2 | x)) <-> F)
1538    * f t
1539    *
1540    * @throws Exception Test failed.
1541    */
 
1542  1 toggle public void testTautology41() throws Exception {
1543  1 final Element ele = BasicParser.createElement(
1544    "\n <EQUI>"
1545    + "\n <FORALL>"
1546    + "\n <VAR id=\"x\" />"
1547    + "\n <EQUI>"
1548    + "\n <PREDVAR id=\"\\phi\">"
1549    + "\n <VAR id=\"x\" />"
1550    + "\n </PREDVAR>"
1551    + "\n <PREDVAR id=\"A\" />"
1552    + "\n </EQUI>"
1553    + "\n </FORALL>"
1554    + "\n <EQUI>"
1555    + "\n <FORALL>"
1556    + "\n <VAR id=\"x\" />"
1557    + "\n <PREDVAR id=\"\\phi\">"
1558    + "\n <VAR id=\"x\" />"
1559    + "\n </PREDVAR>"
1560    + "\n </FORALL>"
1561    + "\n <PREDVAR id=\"A\" />"
1562    + "\n </EQUI>"
1563    + "\n </EQUI>"
1564    );
1565    // System.out.println(ele.toString());
1566  1 assertFalse(isTautology(ele));
1567    }
1568   
1569    /**
1570    * Function: isTautology(Element)
1571    * Type: positive
1572    * Data: \forall x (\phi(x) -> A) -> (\forall x (\phi(x)) -> A)
1573    *
1574    * @throws Exception Test failed.
1575    */
 
1576  1 toggle public void testTautology42() throws Exception {
1577  1 final Element ele = BasicParser.createElement(
1578    "\n <IMPL>"
1579    + "\n <FORALL>"
1580    + "\n <VAR id=\"x\" />"
1581    + "\n <IMPL>"
1582    + "\n <PREDVAR id=\"\\phi\">"
1583    + "\n <VAR id=\"x\" />"
1584    + "\n </PREDVAR>"
1585    + "\n <PREDVAR id=\"A\" />"
1586    + "\n </IMPL>"
1587    + "\n </FORALL>"
1588    + "\n <IMPL>"
1589    + "\n <FORALL>"
1590    + "\n <VAR id=\"x\" />"
1591    + "\n <PREDVAR id=\"\\phi\">"
1592    + "\n <VAR id=\"x\" />"
1593    + "\n </PREDVAR>"
1594    + "\n </FORALL>"
1595    + "\n <PREDVAR id=\"A\" />"
1596    + "\n </IMPL>"
1597    + "\n </IMPL>"
1598   
1599    );
1600    // System.out.println(ele.toString());
1601  1 assertTrue(isTautology(ele));
1602    }
1603   
1604    /**
1605    * Function: isTautology(Element)
1606    * Type: positive
1607    * Data: \forall z (z \in x <-> z \in y) -> x = y)
1608    *
1609    * @throws Exception Test failed.
1610    */
 
1611  1 toggle public void testTautology43() throws Exception {
1612  1 final Element ele = BasicParser.createElement(
1613    " <IMPL>\n"
1614    + " <FORALL>\n"
1615    + " <VAR id=\"z\"/>\n"
1616    + " <EQUI>\n"
1617    + " <PREDCON ref=\"in\">\n"
1618    + " <VAR id=\"z\"/>\n"
1619    + " <VAR id=\"x\"/>\n"
1620    + " </PREDCON>\n"
1621    + " <PREDCON ref=\"in\">\n"
1622    + " <VAR id=\"z\"/>\n"
1623    + " <VAR id=\"y\"/>\n"
1624    + " </PREDCON>\n"
1625    + " </EQUI>\n"
1626    + " </FORALL>\n"
1627    + " <PREDCON ref=\"l.equal\">\n"
1628    + " <VAR id=\"x\"/>\n"
1629    + " <VAR id=\"y\"/>\n"
1630    + " </PREDCON>\n"
1631    + " </IMPL>\n"
1632    );
1633    // System.out.println(ele.toString());
1634  1 assertTrue(isTautology(ele));
1635    }
1636   
1637    /**
1638    * Function: isTautology(Element)
1639    * Type: positive
1640    * Data: (y \in {x | \phi(x)} <-> (isSet(y) n \phi(y))
1641    *
1642    * @throws Exception Test failed.
1643    */
 
1644  1 toggle public void testTautology44() throws Exception {
1645  1 final Element ele = BasicParser.createElement(
1646    " <EQUI>\n"
1647    + " <PREDCON ref=\"in\">\n"
1648    + " <VAR id=\"y\"/>\n"
1649    + " <CLASS>\n"
1650    + " <VAR id=\"x\"/>\n"
1651    + " <PREDVAR id=\"\\phi\">\n"
1652    + " <VAR id=\"x\"/>\n"
1653    + " </PREDVAR>\n"
1654    + " </CLASS>\n"
1655    + " </PREDCON>\n"
1656    + " <AND>\n"
1657    + " <PREDCON ref=\"isSet\">\n"
1658    + " <VAR id=\"y\"/>\n"
1659    + " </PREDCON>\n"
1660    + " <PREDVAR id=\"\\phi\">\n"
1661    + " <VAR id=\"y\"/>\n"
1662    + " </PREDVAR>\n"
1663    + " </AND>\n"
1664    + " </EQUI>\n"
1665    );
1666    // System.out.println(ele.toString());
1667  1 assertTrue(isTautology(ele));
1668    }
1669   
1670    /**
1671    * Function: isTautology(Element)
1672    * Type: positive
1673    * Data: C(x) = (z | z \nin x}
1674    *
1675    * @throws Exception Test failed.
1676    */
 
1677  1 toggle public void testTautology45() throws Exception {
1678  1 final Element ele = BasicParser.createElement(
1679    "<PREDCON id=\"equal\">\n"
1680    + " <FUNCON id=\"complement\">\n"
1681    + " <VAR id=\"x\" />\n"
1682    + " </FUNCON>\n"
1683    + " <CLASS>\n"
1684    + " <VAR id=\"z\" />\n"
1685    + " <PREDCON ref=\"notIn\">\n"
1686    + " <VAR id=\"z\" />\n"
1687    + " <VAR id=\"x\" />\n"
1688    + " </PREDCON>\n"
1689    + " </CLASS>\n"
1690    + "</PREDCON>\n"
1691    );
1692    // System.out.println(ele.toString());
1693  1 assertTrue(isTautology(ele));
1694    }
1695   
1696    /**
1697    * Function: isTautology(Element)
1698    * Type: positive
1699    * Data: x <= y <-> x n C(y) = 0
1700    *
1701    * @throws Exception Test failed.
1702    */
 
1703  1 toggle public void testTautology46() throws Exception {
1704  1 final Element ele = BasicParser.createElement(
1705    " <EQUI>\n"
1706    + " <PREDCON ref=\"subclass\">\n"
1707    + " <VAR id=\"x\" />\n"
1708    + " <VAR id=\"y\" />\n"
1709    + " </PREDCON>\n"
1710    + " <PREDCON ref=\"l.equal\">\n"
1711    + " <FUNCON ref=\"intersection\">\n"
1712    + " <VAR id=\"x\" />\n"
1713    + " <FUNCON ref=\"complement\">\n"
1714    + " <VAR id=\"y\" />\n"
1715    + " </FUNCON>\n"
1716    + " </FUNCON>\n"
1717    + " <FUNCON ref=\"emptySet\" />\n"
1718    + " </PREDCON>\n"
1719    + " </EQUI>\n"
1720    );
1721    // System.out.println(ele.toString());
1722  1 assertTrue(isTautology(ele));
1723    }
1724   
1725    /**
1726    * Function: isTautology(Element)
1727    * Type: positive
1728    * Data: see below
1729    *
1730    * @throws Exception Test failed.
1731    */
 
1732  1 toggle public void testTautology47() throws Exception {
1733  1 final Element ele = BasicParser.createElement(
1734    "<AND>\n"
1735    + " <EQUI>\n"
1736    + " <PREDCON ref=\"subclass\">\n"
1737    + " <VAR id=\"x\" />\n"
1738    + " <VAR id=\"y\" />\n"
1739    + " </PREDCON>\n"
1740    + " <PREDCON ref=\"l.equal\">\n"
1741    + " <FUNCON ref=\"union\">\n"
1742    + " <FUNCON ref=\"complement\">\n"
1743    + " <VAR id=\"x\" />\n"
1744    + " </FUNCON>\n"
1745    + " <VAR id=\"y\" />\n"
1746    + " </FUNCON>\n"
1747    + " <FUNCON ref=\"universalClass\" />\n"
1748    + " </PREDCON>\n"
1749    + " </EQUI>\n"
1750    + " \n"
1751    + " <EQUI>\n"
1752    + " <PREDCON ref=\"subclass\">\n"
1753    + " <VAR id=\"x\" />\n"
1754    + " <FUNCON ref=\"complement\">\n"
1755    + " <VAR id=\"y\" />\n"
1756    + " </FUNCON>\n"
1757    + " </PREDCON>\n"
1758    + " <PREDCON ref=\"l.equal\">\n"
1759    + " <FUNCON ref=\"intersection\">\n"
1760    + " <VAR id=\"x\" />\n"
1761    + " <VAR id=\"y\" />\n"
1762    + " </FUNCON>\n"
1763    + " <FUNCON ref=\"emptySet\" />\n"
1764    + " </PREDCON>\n"
1765    + " </EQUI>\n"
1766    + " \n"
1767    + " <EQUI>\n"
1768    + " <PREDCON ref=\"subclass\">\n"
1769    + " <FUNCON ref=\"intersection\">\n"
1770    + " <VAR id=\"x\" />\n"
1771    + " <VAR id=\"y\" />\n"
1772    + " </FUNCON>\n"
1773    + " <VAR id=\"z\" />\n"
1774    + " </PREDCON>\n"
1775    + " <PREDCON ref=\"subclass\">\n"
1776    + " <VAR id=\"x\" />\n"
1777    + " <FUNCON ref=\"union\">\n"
1778    + " <FUNCON ref=\"complement\">\n"
1779    + " <VAR id=\"y\" />\n"
1780    + " </FUNCON>\n"
1781    + " <VAR id=\"z\" />\n"
1782    + " </FUNCON>\n"
1783    + " </PREDCON>\n"
1784    + " </EQUI> \n"
1785    + " \n"
1786    + "</AND>\n"
1787    );
1788    // System.out.println(ele.toString());
1789  1 assertTrue(isTautology(ele));
1790    }
1791   
1792    /**
1793    * Function: isTautology(Element)
1794    * Type: positive
1795    * Data: A v -A
1796    *
1797    * @throws Exception Test failed.
1798    */
 
1799  1 toggle public void testTautology50() throws Exception {
1800  1 final Element ele = BasicParser.createElement(
1801    "<OR>\n"
1802    + " <PREDVAR id=\"A\"/>\n"
1803    + " <NOT>\n"
1804    + " <PREDVAR id=\"A\"/>\n"
1805    + " </NOT>\n"
1806    +"</OR>\n");
1807    //System.out.println(ele.toString());
1808  1 assertTrue(isTautology(ele));
1809    }
1810   
1811    /**
1812    * Function: isTautology(Element)
1813    * Type: positive
1814    * Data: TRUE <-> (A v -A)
1815    *
1816    * @throws Exception Test failed.
1817    */
 
1818  1 toggle public void testTautology51() throws Exception {
1819  1 final Element ele = BasicParser.createElement(
1820    "<EQUI>\n"
1821    + " <PREDCON id=\"l.TRUE\"/>\n"
1822    + " <OR>\n"
1823    + " <PREDVAR id=\"A\"/>\n"
1824    + " <NOT>\n"
1825    + " <PREDVAR id=\"A\"/>\n"
1826    + " </NOT>\n"
1827    + " </OR>\n"
1828    + "</EQUI>\n");
1829    //System.out.println(ele.toString());
1830  1 assertTrue(isTautology(ele));
1831    }
1832   
1833    /**
1834    * Function: isTautology(Element)
1835    * Type: positive
1836    * Data: \forall x (\phi(x) -> A) -> (\forall x (\phi(x)) -> A)
1837    *
1838    * @throws Exception Test failed.
1839    */
 
1840  1 toggle public void testTautology52() throws Exception {
1841  1 final Element formula = BasicParser.createElement(
1842    "<EQUI>\n"
1843    + " <PREDCON id=\"TRUE\"/>\n"
1844    + " <OR>\n"
1845    + " <PREDVAR id=\"A\"/>\n"
1846    + " <NOT>\n"
1847    + " <PREDVAR id=\"A\"/>\n"
1848    + " </NOT>\n"
1849    + " </OR>\n"
1850    + "</EQUI>\n");
1851  1 assertTrue(isTautology(formula));
1852    }
1853   
1854   
1855    /**
1856    * Function: isTautology(Element)
1857    * Type: positive
1858    * Data: see theorem:powerProposition in qedeq_set_theory_v1.xml
1859    *
1860    * @throws Exception Test failed.
1861    */
 
1862  1 toggle public void testTautology53() throws Exception {
1863  1 final Element formula = BasicParser.createElement(
1864    " <AND>"
1865    + " <EQUI>"
1866    + " <PREDCON ref=\"in\">"
1867    + " <VAR id=\"z\" />"
1868    + " <FUNCON ref=\"power\">"
1869    + " <VAR id=\"x\" />"
1870    + " </FUNCON>"
1871    + " </PREDCON>"
1872    + " <AND>"
1873    + " <PREDCON ref=\"isSet\">"
1874    + " <VAR id=\"z\" />"
1875    + " </PREDCON>"
1876    + " <PREDCON ref=\"subclass\">"
1877    + " <VAR id=\"z\" />"
1878    + " <VAR id=\"x\" />"
1879    + " </PREDCON>"
1880    + " </AND>"
1881    + " </EQUI>"
1882    + " <PREDCON ref=\"l.equal\">"
1883    + " <FUNCON ref=\"power\">"
1884    + " <FUNCON ref=\"universalClass\" />"
1885    + " </FUNCON>"
1886    + " <FUNCON ref=\"universalClass\" />"
1887    + " </PREDCON>"
1888    + " <PREDCON ref=\"l.equal\">"
1889    + " <FUNCON ref=\"power\">"
1890    + " <FUNCON ref=\"emptySet\" />"
1891    + " </FUNCON>"
1892    + " <FUNCON ref=\"classList\">"
1893    + " <FUNCON ref=\"emptySet\" />"
1894    + " </FUNCON>"
1895    + " </PREDCON>"
1896    + " <EQUI>"
1897    + " <PREDCON ref=\"isSet\">"
1898    + " <VAR id=\"x\" />"
1899    + " </PREDCON>"
1900    + " <PREDCON ref=\"in\">"
1901    + " <VAR id=\"x\" />"
1902    + " <FUNCON ref=\"power\">"
1903    + " <VAR id=\"x\" />"
1904    + " </FUNCON>"
1905    + " </PREDCON>"
1906    + " </EQUI>"
1907    + " <IMPL>"
1908    + " <PREDCON ref=\"subclass\">"
1909    + " <VAR id=\"x\" />"
1910    + " <VAR id=\"y\" />"
1911    + " </PREDCON>"
1912    + " <PREDCON ref=\"subclass\">"
1913    + " <FUNCON ref=\"power\">"
1914    + " <VAR id=\"x\" />"
1915    + " </FUNCON>"
1916    + " <FUNCON ref=\"power\">"
1917    + " <VAR id=\"y\" />"
1918    + " </FUNCON>"
1919    + " </PREDCON>"
1920    + " </IMPL>"
1921    + " <IMPL>"
1922    + " <AND>"
1923    + " <PREDCON ref=\"isSet\">"
1924    + " <VAR id=\"x\" />"
1925    + " </PREDCON>"
1926    + " <PREDCON ref=\"subclass\">"
1927    + " <FUNCON ref=\"power\">"
1928    + " <VAR id=\"x\" />"
1929    + " </FUNCON>"
1930    + " <FUNCON ref=\"power\">"
1931    + " <VAR id=\"y\" />"
1932    + " </FUNCON>"
1933    + " </PREDCON>"
1934    + " </AND>"
1935    + " <PREDCON ref=\"subclass\">"
1936    + " <VAR id=\"x\" />"
1937    + " <VAR id=\"y\" />"
1938    + " </PREDCON>"
1939    + " </IMPL>"
1940    + " <PREDCON ref=\"l.equal\">"
1941    + " <FUNCON ref=\"power\">"
1942    + " <FUNCON ref=\"intersection\">"
1943    + " <VAR id=\"x\" />"
1944    + " <VAR id=\"y\" />"
1945    + " </FUNCON>"
1946    + " </FUNCON>"
1947    + " <FUNCON ref=\"intersection\">"
1948    + " <FUNCON ref=\"power\">"
1949    + " <VAR id=\"x\" />"
1950    + " </FUNCON>"
1951    + " <FUNCON ref=\"power\">"
1952    + " <VAR id=\"y\" />"
1953    + " </FUNCON>"
1954    + " </FUNCON>"
1955    + " </PREDCON>"
1956    + " <PREDCON ref=\"subclass\">"
1957    + " <FUNCON ref=\"union\">"
1958    + " <FUNCON ref=\"power\">"
1959    + " <VAR id=\"x\" />"
1960    + " </FUNCON>"
1961    + " <FUNCON ref=\"power\">"
1962    + " <VAR id=\"y\" />"
1963    + " </FUNCON>"
1964    + " </FUNCON>"
1965    + " <FUNCON ref=\"power\">"
1966    + " <FUNCON ref=\"union\">"
1967    + " <VAR id=\"x\" />"
1968    + " <VAR id=\"y\" />"
1969    + " </FUNCON>"
1970    + " </FUNCON>"
1971    + " </PREDCON>"
1972    + " <PREDCON ref=\"subclass\">"
1973    + " <VAR id=\"x\" />"
1974    + " <FUNCON ref=\"power\">"
1975    + " <FUNCON ref=\"setSum\">"
1976    + " <VAR id=\"x\" />"
1977    + " </FUNCON>"
1978    + " </FUNCON>"
1979    + " </PREDCON>"
1980    + " <PREDCON ref=\"subclass\">"
1981    + " <FUNCON ref=\"setSum\">"
1982    + " <FUNCON ref=\"power\">"
1983    + " <VAR id=\"x\" />"
1984    + " </FUNCON>"
1985    + " </FUNCON>"
1986    + " <VAR id=\"x\" />"
1987    + " </PREDCON>"
1988    + " </AND>"
1989    );
1990  1 assertTrue(isTautology(formula));
1991    }
1992   
1993   
1994    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .