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