The lion likes the tiger. The rabbit needs the tiger. The squirrel needs the rabbit. The tiger is nice. If something likes the tiger then it is blue. Nice, blue things are kind. If something sees the lion and the lion needs the squirrel then it likes the tiger. If something likes the lion and it needs the tiger then the tiger is green. If something is green then it needs the tiger. If something is blue and kind then it likes the rabbit. If the lion is blue then the lion is green. If something is blue and young then it sees the rabbit.
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something likes the tiger then it is blue.
((("something" "likes" "tiger" "+")) -> ("something" "is" "blue" "+"))
Nice, blue things are kind.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something sees the lion and the lion needs the squirrel then it likes the tiger.
((("something" "sees" "lion" "+") ("lion" "needs" "squirrel" "+")) -> ("something" "likes" "tiger" "+"))
If something likes the lion and it needs the tiger then the tiger is green.
((("something" "likes" "lion" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something is green then it needs the tiger.
((("something" "is" "green" "+")) -> ("something" "needs" "tiger" "+"))
If something is blue and kind then it likes the rabbit.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "likes" "rabbit" "+"))
If the lion is blue then the lion is green.
((("lion" "is" "blue" "+")) -> ("lion" "is" "green" "+"))
If something is blue and young then it sees the rabbit.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "sees" "rabbit" "+"))
The tiger is nice.
True
1
proof
[(triple4)]
("tiger" "is" "nice" "+")
triple4
The squirrel does not need the rabbit.
False
1
inv-proof
[(triple3)]
("squirrel" "needs" "rabbit" "-")
triple3
The lion is blue.
True
2
proof
[(((triple1) -> rule1))]
("lion" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("lion" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("lion" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion needs the tiger.
True
4
proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule5))]
("lion" "needs" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion does not need the tiger.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule5))]
("lion" "needs" "tiger" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The squirrel is not blue.
Unknown
inv-rconc
[@2: The squirrel is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel does not like the tiger.
Unknown
inv-rconc
[@1: The squirrel likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "likes" "tiger" "-")
The rabbit is kind.
Unknown
rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "kind" "+")
The lion does not see the tiger.
Unknown
inv-random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The squirrel likes the lion.
Unknown
random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "+")
@0: The lion likes the tiger.[(triple1)] The rabbit needs the tiger.[(triple2)] The squirrel needs the rabbit.[(triple3)] The tiger is nice.[(triple4)] @1: The lion is blue.[(((triple1) -> rule1))] @2: The lion is green.[(((((triple1) -> rule1)) -> rule7))] @3: The lion needs the tiger.[(((((((triple1) -> rule1)) -> rule7)) -> rule5))]
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3