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