The cow likes the squirrel. The squirrel sees the tiger. The tiger is big. If the tiger is big then the tiger visits the squirrel. If someone likes the squirrel and the squirrel visits the tiger then the tiger visits the squirrel. If someone visits the squirrel then they are kind. If someone likes the squirrel then they like the tiger. If someone likes the cow then they like the tiger. If someone is green then they like the squirrel.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
If the tiger is big then the tiger visits the squirrel.
((("tiger" "is" "big" "+")) -> ("tiger" "visits" "squirrel" "+"))
If someone likes the squirrel and the squirrel visits the tiger then the tiger visits the squirrel.
((("someone" "likes" "squirrel" "+") ("squirrel" "visits" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
If someone visits the squirrel then they are kind.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the squirrel then they like the tiger.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the cow then they like the tiger.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is green then they like the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "likes" "squirrel" "+"))
The cow likes the squirrel.
True
1
proof
[(triple1)]
("cow" "likes" "squirrel" "+")
triple1
The cow does not like the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "likes" "squirrel" "-")
triple1
The tiger visits the squirrel.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "visits" "squirrel" "+")
((triple3) -> (rule1 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The cow does not like the tiger.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "likes" "tiger" "-")
((triple1) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("tiger" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is not kind.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("tiger" "is" "kind" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "kind" "+")
The tiger does not like the squirrel.
Unknown
inv-rconc
[@1: The tiger likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "squirrel" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The tiger does not visit the cow.
Unknown
inv-random
[@0: The tiger visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cow" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The cow likes the squirrel.[(triple1)] The squirrel sees the tiger.[(triple2)] The tiger is big.[(triple3)] @1: The cow likes the tiger.[(((triple1) -> rule4))] The tiger visits the squirrel.[(((triple3) -> rule1))] @2: The tiger is kind.[(((((triple3) -> rule1)) -> rule3))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple1) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((triple3) -> (rule1 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2