The cat needs the squirrel. The cow is not red. The cow likes the cat. The cow likes the tiger. The cow visits the cat. The squirrel likes the tiger. The squirrel needs the cat. The squirrel visits the cow. The squirrel visits the tiger. The tiger is red. The tiger likes the squirrel. The tiger does not visit the squirrel. If something visits the tiger and the tiger does not need the cat then it does not visit the cat. If something needs the cat and it is rough then it likes the squirrel. If something is green then it likes the squirrel. If something is red and it needs the squirrel then it does not visit the tiger. If something is rough then it visits the tiger. If something visits the cow and the cow is red then it is rough. All red things are green. If something visits the cat and it is not young then the cat does not visit the cow.
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cow is not red.
("cow" "is" "red" "-")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
If something visits the tiger and the tiger does not need the cat then it does not visit the cat.
((("something" "visits" "tiger" "+") ("tiger" "needs" "cat" "~")) -> ("something" "visits" "cat" "-"))
If something needs the cat and it is rough then it likes the squirrel.
((("something" "needs" "cat" "+") ("something" "is" "rough" "+")) -> ("something" "likes" "squirrel" "+"))
If something is green then it likes the squirrel.
((("something" "is" "green" "+")) -> ("something" "likes" "squirrel" "+"))
If something is red and it needs the squirrel then it does not visit the tiger.
((("something" "is" "red" "+") ("something" "needs" "squirrel" "+")) -> ("something" "visits" "tiger" "-"))
If something is rough then it visits the tiger.
((("something" "is" "rough" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the cow and the cow is red then it is rough.
((("something" "visits" "cow" "+") ("cow" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something visits the cat and it is not young then the cat does not visit the cow.
((("something" "visits" "cat" "+") ("something" "is" "young" "~")) -> ("cat" "visits" "cow" "-"))
The cow is not red.
True
1
proof
[(triple2)]
("cow" "is" "red" "-")
triple2
The tiger does not like the squirrel.
False
1
inv-proof
[(triple11 OR ((((triple10) -> rule7)) -> rule3))]
("tiger" "likes" "squirrel" "-")
triple11
((((triple10) -> (rule7 % int2))) -> (rule3 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is green.
True
2
proof
[(((triple10) -> rule7))]
("tiger" "is" "green" "+")
((triple10) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple10) -> rule7))]
("tiger" "is" "green" "-")
((triple10) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "green" "-")
The cow visits the tiger.
Unknown
rconc
[@2: The cow visits the tiger.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("cow" "visits" "tiger" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat needs the squirrel.[(triple1)] The cow is not red.[(triple2)] The cow likes the cat.[(triple3)] The cow likes the tiger.[(triple4)] The cow visits the cat.[(triple5)] The squirrel likes the tiger.[(triple6)] The squirrel needs the cat.[(triple7)] The squirrel visits the cow.[(triple8)] The squirrel visits the tiger.[(triple9)] The tiger does not visit the squirrel.[(triple12)] The tiger is red.[(triple10)] The tiger likes the squirrel.[(triple11 OR ((((triple10) -> rule7)) -> rule3))] @1: The tiger is green.[(((triple10) -> rule7))]
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple1
The cow is not red.
("cow" "is" "red" "-")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The cow visits the cat.
("cow" "visits" "cat" "+")
triple5
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple6
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple7
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple8
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple9
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple11
((((triple10) -> (rule7 % int2))) -> (rule3 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((triple10) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1