The cat is round. The cat visits the cow. The cow likes the cat. If someone is round and they visit the cow then they eat the cat. If the cat is red then the cat is nice. If someone visits the cow and they eat the cat then the cow visits the cat.
The cat is round.
("cat" "is" "round" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If someone is round and they visit the cow then they eat the cat.
((("someone" "is" "round" "+") ("someone" "visits" "cow" "+")) -> ("someone" "eats" "cat" "+"))
If the cat is red then the cat is nice.
((("cat" "is" "red" "+")) -> ("cat" "is" "nice" "+"))
If someone visits the cow and they eat the cat then the cow visits the cat.
((("someone" "visits" "cow" "+") ("someone" "eats" "cat" "+")) -> ("cow" "visits" "cat" "+"))
The cat is round.
True
1
proof
[(triple1)]
("cat" "is" "round" "+")
triple1
The cat does not visit the cow.
False
1
inv-proof
[(triple2)]
("cat" "visits" "cow" "-")
triple2
The cat eats the cat.
True
3
proof
[(((triple1 triple2) -> rule1))]
("cat" "eats" "cat" "+")
((triple1 triple2) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("cat" "eats" "cat" "-")
((triple1 triple2) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cow visits the cat.
True
5
proof
[(((triple2 ((triple1 triple2) -> rule1)) -> rule3))]
("cow" "visits" "cat" "+")
((triple2 ((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cow does not visit the cat.
False
5
inv-proof
[(((triple2 ((triple1 triple2) -> rule1)) -> rule3))]
("cow" "visits" "cat" "-")
((triple2 ((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "nice" "-")
The cow eats the cat.
Unknown
rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cat" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cat is round.[(triple1)] The cat visits the cow.[(triple2)] The cow likes the cat.[(triple3)] @1: The cat eats the cat.[(((triple1 triple2) -> rule1))] @2: The cow visits the cat.[(((triple2 ((triple1 triple2) -> rule1)) -> rule3))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple1 triple2) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple2 ((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2