The cat needs the tiger. The squirrel needs the cat. The tiger needs the squirrel. If someone likes the cat then they chase the cat. If someone chases the squirrel and the squirrel needs the cat then the squirrel likes the tiger. If someone needs the cat then the cat chases the squirrel. If someone needs the cat and they like the cat then they like the tiger. If someone needs the cat and they like the cat then they are red. If the tiger needs the cat then the tiger chases the cat.
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If someone likes the cat then they chase the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the squirrel and the squirrel needs the cat then the squirrel likes the tiger.
((("someone" "chases" "squirrel" "+") ("squirrel" "needs" "cat" "+")) -> ("squirrel" "likes" "tiger" "+"))
If someone needs the cat then the cat chases the squirrel.
((("someone" "needs" "cat" "+")) -> ("cat" "chases" "squirrel" "+"))
If someone needs the cat and they like the cat then they like the tiger.
((("someone" "needs" "cat" "+") ("someone" "likes" "cat" "+")) -> ("someone" "likes" "tiger" "+"))
If someone needs the cat and they like the cat then they are red.
((("someone" "needs" "cat" "+") ("someone" "likes" "cat" "+")) -> ("someone" "is" "red" "+"))
If the tiger needs the cat then the tiger chases the cat.
((("tiger" "needs" "cat" "+")) -> ("tiger" "chases" "cat" "+"))
The cat needs the tiger.
True
1
proof
[(triple1)]
("cat" "needs" "tiger" "+")
triple1
The tiger does not need the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "needs" "squirrel" "-")
triple3
The cat chases the squirrel.
True
2
proof
[(((triple2) -> rule3))]
("cat" "chases" "squirrel" "+")
((triple2) -> (rule3 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The cat does not chase the squirrel.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "chases" "squirrel" "-")
((triple2) -> (rule3 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The squirrel likes the tiger.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("squirrel" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
The squirrel does not like the tiger.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("squirrel" "likes" "tiger" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "red" "-")
The squirrel chases the cat.
Unknown
rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "cat" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "red" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The tiger chases the squirrel.
Unknown
random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "+")
@0: The cat needs the tiger.[(triple1)] The squirrel needs the cat.[(triple2)] The tiger needs the squirrel.[(triple3)] @1: The cat chases the squirrel.[(((triple2) -> rule3))] @2: The squirrel likes the tiger.[(((((triple2) -> rule3) triple2) -> rule2))]
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple2
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple3
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
((triple2) -> (rule3 % int1))
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
int2