The cat needs the cow. The cat visits the cow. The cow eats the tiger. The cow is rough. The tiger is blue. The tiger is rough. The tiger visits the cow. If something eats the tiger and the tiger needs the cow then the cow visits the tiger.
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is rough.
("cow" "is" "rough" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something eats the tiger and the tiger needs the cow then the cow visits the tiger.
((("something" "eats" "tiger" "+") ("tiger" "needs" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
The cat visits the cow.
True
1
proof
[(triple2)]
("cat" "visits" "cow" "+")
triple2
The tiger is not blue.
False
1
inv-proof
[(triple5)]
("tiger" "is" "blue" "-")
triple5
The cow does not visit the tiger.
Unknown
inv-rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "tiger" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cat needs the cow.[(triple1)] The cat visits the cow.[(triple2)] The cow eats the tiger.[(triple3)] The cow is rough.[(triple4)] The tiger is blue.[(triple5)] The tiger is rough.[(triple6)] The tiger visits the cow.[(triple7)]
The cat needs the cow.
("cat" "needs" "cow" "+")
triple1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The tiger is blue.
("tiger" "is" "blue" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7