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