The cat eats the tiger. The cat is kind. The cat is round. The cat sees the squirrel. The cat sees the tiger. The lion is round. The squirrel is big. The squirrel sees the cat. The squirrel sees the lion. The tiger sees the squirrel. If someone needs the lion and the lion eats the cat then the lion is kind. If someone is young and they eat the lion then the lion is big. If the lion needs the tiger then the tiger is cold. If someone sees the lion then they see the tiger. If someone is big and they need the cat then they see the squirrel. If someone needs the cat then the cat needs the tiger. If the tiger is young then the tiger is round. If someone is kind and they see the tiger then they need the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion is round.
("lion" "is" "round" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If someone needs the lion and the lion eats the cat then the lion is kind.
((("someone" "needs" "lion" "+") ("lion" "eats" "cat" "+")) -> ("lion" "is" "kind" "+"))
If someone is young and they eat the lion then the lion is big.
((("someone" "is" "young" "+") ("someone" "eats" "lion" "+")) -> ("lion" "is" "big" "+"))
If the lion needs the tiger then the tiger is cold.
((("lion" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If someone sees the lion then they see the tiger.
((("someone" "sees" "lion" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is big and they need the cat then they see the squirrel.
((("someone" "is" "big" "+") ("someone" "needs" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone needs the cat then the cat needs the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If the tiger is young then the tiger is round.
((("tiger" "is" "young" "+")) -> ("tiger" "is" "round" "+"))
If someone is kind and they see the tiger then they need the tiger.
((("someone" "is" "kind" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
The squirrel sees the lion.
True
1
proof
[(triple9)]
("squirrel" "sees" "lion" "+")
triple9
The cat is not kind.
False
1
inv-proof
[(triple2)]
("cat" "is" "kind" "-")
triple2
The squirrel sees the tiger.
True
2
proof
[(((triple9) -> rule4))]
("squirrel" "sees" "tiger" "+")
((triple9) -> (rule4 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The cat does not need the tiger.
False
3
inv-proof
[(((triple2 triple5) -> rule8))]
("cat" "needs" "tiger" "-")
((triple2 triple5) -> (rule8 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The lion is big.
Unknown
rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "big" "+")
The squirrel does not need the lion.
Unknown
inv-random
[@0: The squirrel needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "lion" "-")
The lion eats the tiger.
Unknown
random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "+")
@0: The cat eats the tiger.[(triple1)] The cat is kind.[(triple2)] The cat is round.[(triple3)] The cat sees the squirrel.[(triple4)] The cat sees the tiger.[(triple5)] The lion is round.[(triple6)] The squirrel is big.[(triple7)] The squirrel sees the cat.[(triple8)] The squirrel sees the lion.[(triple9)] The tiger sees the squirrel.[(triple10)] @1: The cat needs the tiger.[(((triple2 triple5) -> rule8))] The squirrel sees the tiger.[(((triple9) -> rule4))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The lion is round.
("lion" "is" "round" "+")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple10
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple2 triple5) -> (rule8 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
((triple9) -> (rule4 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1