The bald eagle eats the cat. The cat likes the bald eagle. If something is young then it eats the cat. If something eats the cat then the cat sees the bald eagle. If the bald eagle likes the cat and the bald eagle is round then the bald eagle sees the cat. If something eats the cat and the cat does not eat the bald eagle then it sees the bald eagle. If something eats the cat then the cat is young. If something eats the cat and the cat sees the bald eagle then it sees the cat.
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
If something is young then it eats the cat.
((("something" "is" "young" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat then the cat sees the bald eagle.
((("something" "eats" "cat" "+")) -> ("cat" "sees" "bald eagle" "+"))
If the bald eagle likes the cat and the bald eagle is round then the bald eagle sees the cat.
((("bald eagle" "likes" "cat" "+") ("bald eagle" "is" "round" "+")) -> ("bald eagle" "sees" "cat" "+"))
If something eats the cat and the cat does not eat the bald eagle then it sees the bald eagle.
((("something" "eats" "cat" "+") ("cat" "eats" "bald eagle" "~")) -> ("something" "sees" "bald eagle" "+"))
If something eats the cat then the cat is young.
((("something" "eats" "cat" "+")) -> ("cat" "is" "young" "+"))
If something eats the cat and the cat sees the bald eagle then it sees the cat.
((("something" "eats" "cat" "+") ("cat" "sees" "bald eagle" "+")) -> ("something" "sees" "cat" "+"))
The bald eagle eats the cat.
True
1
proof
[(triple1)]
("bald eagle" "eats" "cat" "+")
triple1
The cat does not like the bald eagle.
False
1
inv-proof
[(triple2)]
("cat" "likes" "bald eagle" "-")
triple2
The cat is young.
True
2
proof
[(((triple1) -> rule5))]
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "is" "young" "-")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The bald eagle sees the cat.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule6) OR ((triple1 ((((((triple1) -> rule5)) -> rule1)) -> rule2)) -> rule6))]
("bald eagle" "sees" "cat" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat does not eat the cat.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("cat" "eats" "cat" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat sees the cat.
True
6
proof
[(((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule2)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((((((triple1) -> rule5)) -> rule1)) -> rule2)) -> rule6))]
("cat" "sees" "cat" "+")
((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat does not see the cat.
False
6
inv-proof
[(((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule2)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((((((triple1) -> rule5)) -> rule1)) -> rule2)) -> rule6))]
("cat" "sees" "cat" "-")
((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The bald eagle does not see the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The cat eats the bald eagle.
Unknown
random
[@0: The cat eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bald eagle" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The bald eagle is young.
Unknown
random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "+")
The bald eagle does not like the bald eagle.
Unknown
inv-random
[@0: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "bald eagle" "-")
The bald eagle is rough.
Unknown
random
[@0: The bald eagle is rough.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "rough" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The bald eagle is cold.
Unknown
random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "+")
@0: The bald eagle eats the cat.[(triple1)] The cat likes the bald eagle.[(triple2)] @1: The cat is young.[(((triple1) -> rule5))] The cat sees the bald eagle.[(((triple1) -> rule2) OR ((((((triple1) -> rule5)) -> rule1)) -> rule2))] @2: The bald eagle sees the cat.[(((triple1 ((triple1) -> rule2)) -> rule6) OR ((triple1 ((((((triple1) -> rule5)) -> rule1)) -> rule2)) -> rule6))] The cat eats the cat.[(((((triple1) -> rule5)) -> rule1))] @3: The cat sees the cat.[(((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule2)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((((((triple1) -> rule5)) -> rule1)) -> rule2)) -> rule6))]
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
triple1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
((triple1) -> (rule2 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4