The cow eats the tiger. The cow is rough. The squirrel is big. The squirrel sees the tiger. The squirrel visits the cow. The tiger eats the cow. The tiger eats the squirrel. The tiger is big. The tiger is rough. The tiger sees the cow. The tiger visits the cow. The tiger visits the squirrel. If something sees the tiger and the tiger sees the squirrel then it sees the cow. If something eats the cow then it is rough. If something visits the tiger then the tiger eats the cow. If something sees the cow and the cow is young then it eats the squirrel. If something visits the cow then the cow eats the squirrel. If the cow is rough and the cow eats the tiger then the tiger visits the cow.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is rough.
("cow" "is" "rough" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something sees the tiger and the tiger sees the squirrel then it sees the cow.
((("something" "sees" "tiger" "+") ("tiger" "sees" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
If something eats the cow then it is rough.
((("something" "eats" "cow" "+")) -> ("something" "is" "rough" "+"))
If something visits the tiger then the tiger eats the cow.
((("something" "visits" "tiger" "+")) -> ("tiger" "eats" "cow" "+"))
If something sees the cow and the cow is young then it eats the squirrel.
((("something" "sees" "cow" "+") ("cow" "is" "young" "+")) -> ("something" "eats" "squirrel" "+"))
If something visits the cow then the cow eats the squirrel.
((("something" "visits" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If the cow is rough and the cow eats the tiger then the tiger visits the cow.
((("cow" "is" "rough" "+") ("cow" "eats" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
The cow eats the tiger.
True
1
proof
[(triple1)]
("cow" "eats" "tiger" "+")
triple1
The tiger does not eat the squirrel.
False
1
inv-proof
[(triple7)]
("tiger" "eats" "squirrel" "-")
triple7
The cow eats the squirrel.
True
2
proof
[(((triple11) -> rule5) OR ((triple5) -> rule5) OR ((((triple2 triple1) -> rule6)) -> rule5))]
("cow" "eats" "squirrel" "+")
((triple11) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((triple5) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((((triple2 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The cow does not eat the squirrel.
False
2
inv-proof
[(((triple11) -> rule5) OR ((triple5) -> rule5) OR ((((triple2 triple1) -> rule6)) -> rule5))]
("cow" "eats" "squirrel" "-")
((triple11) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((triple5) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((((triple2 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The squirrel does not see the cow.
Unknown
inv-rconc
[@1: The squirrel sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "cow" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The tiger sees the squirrel.
Unknown
random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "+")
@0: The cow eats the tiger.[(triple1)] The cow is rough.[(triple2)] The squirrel is big.[(triple3)] The squirrel sees the tiger.[(triple4)] The squirrel visits the cow.[(triple5)] The tiger eats the cow.[(triple6)] The tiger eats the squirrel.[(triple7)] The tiger is big.[(triple8)] The tiger is rough.[(triple9 OR ((triple6) -> rule2))] The tiger sees the cow.[(triple10)] The tiger visits the cow.[(triple11 OR ((triple2 triple1) -> rule6))] The tiger visits the squirrel.[(triple12)] @1: The cow eats the squirrel.[(((triple11) -> rule5) OR ((triple5) -> rule5) OR ((((triple2 triple1) -> rule6)) -> rule5))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple4
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple5
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple6
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
((triple6) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple11
((triple2 triple1) -> (rule6 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((triple11) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((triple5) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
((((triple2 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2