The bear likes the cow. The cat is big. The cat visits the cow. The cow is cold. The cow is green. The cow needs the cat. The squirrel likes the cat. If someone is cold and they visit the bear then they like the cat. If the cow needs the cat then the cow visits the bear. If the cat visits the bear and the bear is round then the bear visits the cat.
The bear likes the cow.
("bear" "likes" "cow" "+")
The cat is big.
("cat" "is" "big" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If someone is cold and they visit the bear then they like the cat.
((("someone" "is" "cold" "+") ("someone" "visits" "bear" "+")) -> ("someone" "likes" "cat" "+"))
If the cow needs the cat then the cow visits the bear.
((("cow" "needs" "cat" "+")) -> ("cow" "visits" "bear" "+"))
If the cat visits the bear and the bear is round then the bear visits the cat.
((("cat" "visits" "bear" "+") ("bear" "is" "round" "+")) -> ("bear" "visits" "cat" "+"))
The cat is big.
True
1
proof
[(triple2)]
("cat" "is" "big" "+")
triple2
The bear does not like the cow.
False
1
inv-proof
[(triple1)]
("bear" "likes" "cow" "-")
triple1
The cow visits the bear.
True
2
proof
[(((triple6) -> rule2))]
("cow" "visits" "bear" "+")
((triple6) -> (rule2 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow does not visit the bear.
False
2
inv-proof
[(((triple6) -> rule2))]
("cow" "visits" "bear" "-")
((triple6) -> (rule2 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow likes the cat.
True
4
proof
[(((triple4 ((triple6) -> rule2)) -> rule1))]
("cow" "likes" "cat" "+")
((triple4 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow does not like the cat.
False
4
inv-proof
[(((triple4 ((triple6) -> rule2)) -> rule1))]
("cow" "likes" "cat" "-")
((triple4 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "-")
The bear visits the cat.
Unknown
rconc
[@1: The bear visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "cat" "+")
The bear does not like the cat.
Unknown
inv-rconc
[@1: The bear likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "cat" "-")
The cat visits the bear.
Unknown
random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The bear likes the cow.[(triple1)] The cat is big.[(triple2)] The cat visits the cow.[(triple3)] The cow is cold.[(triple4)] The cow is green.[(triple5)] The cow needs the cat.[(triple6)] The squirrel likes the cat.[(triple7)] @1: The cow visits the bear.[(((triple6) -> rule2))] @2: The cow likes the cat.[(((triple4 ((triple6) -> rule2)) -> rule1))]
The bear likes the cow.
("bear" "likes" "cow" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow is green.
("cow" "is" "green" "+")
triple5
The cow needs the cat.
("cow" "needs" "cat" "+")
triple6
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple7
The cow visits the bear.
("cow" "visits" "bear" "+")
((triple6) -> (rule2 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
((triple4 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2