public void testCanProve(){
        try{
        	System.out.print("HeadTest ");
            Identifier idA = new Identifier("A", 1);
            Identifier idB = new Identifier("B", 1);
            Identifier idC = new Identifier("C", 1);

            Constant c1 = new Constant("Id1", 1);
            Constant c2 = new Constant("Id2", 1);
            Constant c3 = new Constant("Id3", 1);

            Predicate s1 = createPredicate("A('Id1')");
            Predicate s2 = createPredicate("A('Id2')");

            Predicate s3 = createPredicate("B('Id1', 'Id2')");
            Predicate s4 = createPredicate("B('Id2','Id3')");

            Predicate s5 = createPredicate("C('Id1','Id2','Id3')");
            Predicate s6 = createPredicate("C('Id3','Id2','Id1')");

            Predicate bad1 = createPredicate("A(Id1)");
            Predicate bad2 = createPredicate("A(Id1, 'Id2')");
            Predicate bad3 = createPredicate("A('Id1', Id2)");
            Predicate bad4 = createPredicate("A(Id1, Id2)");
            Predicate bad5 = createPredicate("C(Id2,'Id3','Id1')");
            Predicate bad6 = createPredicate("C('Id2',Id3,'Id1')");
            Predicate bad7 = createPredicate("C('Id2','Id3',Id1)");
            Predicate bad8 = createPredicate("C('Id2',Id3,Id1)");
            Predicate bad9 = createPredicate("C(Id2,'Id3',Id1)");
            Predicate bad10 = createPredicate("C(Id2,Id3,'Id1')");
            Predicate bad11 = createPredicate("C(Id2,Id3,Id1)");

            Predicate[] badOnes =
                {bad1, bad2, bad3, bad4, bad5, bad6, bad7, bad8, bad9, bad10,
                 bad11};

            //=================================================================
            
            Head h = createHead("A(A)");

            try{
                h.unify(null); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            try{
                h.unify(s3); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            assertTrue(checkAllBad(h, badOnes));

            HashMap<Identifier,Constant> map = h.unify(s1);

            assertTrue(map.get(idA).equals(c1));
            assertFalse(map.get(idA).equals(c2));
            assertTrue(map.get(idB) == null);

            map = h.unify(s2);
            assertFalse(map.get(idA).equals(c1));
            assertTrue(map.get(idA).equals(c2));
            assertTrue(map.get(idB) == null);

            //=================================================================

            h = createHead("A(A, B)");

            try{
                h.unify(null); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            try{
                h.unify(s1); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            try{
                h.unify(s5); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            assertTrue(checkAllBad(h, badOnes));

            map = h.unify(s3);
            assertTrue(map.get(idA).equals(c1));
            assertTrue(map.get(idB).equals(c2));
            assertFalse(map.get(idA).equals(c2));
            assertFalse(map.get(idB).equals(c1));
            assertTrue(map.get(idC) == null);

            map = h.unify(s4);
            assertTrue(map.get(idA).equals(c2));
            assertTrue(map.get(idB).equals(c3));
            assertFalse(map.get(idA).equals(c3));
            assertFalse(map.get(idB).equals(c2));
            assertTrue(map.get(idC) == null);
            
            //=================================================================

            h = createHead("A(A, B, C)");

            try{
                h.unify(null); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            try{
                h.unify(s1); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            try{
                h.unify(s3); 
                assertTrue(false);
            }catch(AssertionError e){
                assertTrue(true);
            };

            assertTrue(checkAllBad(h, badOnes));

            map = h.unify(s5);
            assertTrue(map.get(idA).equals(c1));
            assertTrue(map.get(idB).equals(c2));
            assertTrue(map.get(idC).equals(c3));
            assertFalse(map.get(idA).equals(c2));
            assertFalse(map.get(idA).equals(c3));
            assertFalse(map.get(idB).equals(c1));
            assertFalse(map.get(idB).equals(c3));
            assertFalse(map.get(idC).equals(c1));
            assertFalse(map.get(idC).equals(c2));

            map = h.unify(s6);
            assertTrue(map.get(idA).equals(c3));
            assertTrue(map.get(idB).equals(c2));
            assertTrue(map.get(idC).equals(c1));
            assertFalse(map.get(idA).equals(c1));
            assertFalse(map.get(idA).equals(c2));
            assertFalse(map.get(idB).equals(c1));
            assertFalse(map.get(idB).equals(c3));
            assertFalse(map.get(idC).equals(c2));
            assertFalse(map.get(idC).equals(c3));

        	System.out.println("PASSED");
        }catch(ParserException e){
             System.out.println(
                 "ERROR: in HeadTest::testCanProve()\n" +
                 e.getMessage());
        };
    }