The rabbit does not chase the squirrel. The squirrel chases the tiger. The squirrel is blue. The squirrel is red. The squirrel visits the tiger. The tiger chases the rabbit. The tiger is green. If someone is green then they are kind. If someone visits the squirrel and the squirrel visits the rabbit then they visit the tiger. If someone visits the tiger then they chase the squirrel. If the rabbit visits the squirrel and the rabbit is not green then the squirrel chases the rabbit. If someone chases the squirrel then the squirrel likes the tiger. If someone likes the tiger and the tiger chases the rabbit then the rabbit is red.
The rabbit does not chase the squirrel.
("rabbit" "chases" "squirrel" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone visits the squirrel and the squirrel visits the rabbit then they visit the tiger.
((("someone" "visits" "squirrel" "+") ("squirrel" "visits" "rabbit" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the tiger then they chase the squirrel.
((("someone" "visits" "tiger" "+")) -> ("someone" "chases" "squirrel" "+"))
If the rabbit visits the squirrel and the rabbit is not green then the squirrel chases the rabbit.
((("rabbit" "visits" "squirrel" "+") ("rabbit" "is" "green" "~")) -> ("squirrel" "chases" "rabbit" "+"))
If someone chases the squirrel then the squirrel likes the tiger.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "likes" "tiger" "+"))
If someone likes the tiger and the tiger chases the rabbit then the rabbit is red.
((("someone" "likes" "tiger" "+") ("tiger" "chases" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
The tiger is green.
True
1
proof
[(triple7)]
("tiger" "is" "green" "+")
triple7
The squirrel does not chase the tiger.
False
1
inv-proof
[(triple2)]
("squirrel" "chases" "tiger" "-")
triple2
The tiger is kind.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "is" "kind" "+")
((triple7) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "is" "kind" "-")
((triple7) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel likes the tiger.
True
3
proof
[(((((triple5) -> rule3)) -> rule5))]
("squirrel" "likes" "tiger" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel does not like the tiger.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule5))]
("squirrel" "likes" "tiger" "-")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The rabbit is red.
True
5
proof
[(((((((triple5) -> rule3)) -> rule5) triple6) -> rule6))]
("rabbit" "is" "red" "+")
((((((triple5) -> (rule3 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The rabbit is not red.
False
5
inv-proof
[(((((((triple5) -> rule3)) -> rule5) triple6) -> rule6))]
("rabbit" "is" "red" "-")
((((((triple5) -> (rule3 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The rabbit does not visit the tiger.
Unknown
inv-rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "kind" "-")
The tiger chases the squirrel.
Unknown
rconc
[@2: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("tiger" "chases" "squirrel" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The rabbit does not chase the squirrel.[(triple1)] The squirrel chases the tiger.[(triple2)] The squirrel is blue.[(triple3)] The squirrel is red.[(triple4)] The squirrel visits the tiger.[(triple5)] The tiger chases the rabbit.[(triple6)] The tiger is green.[(triple7)] @1: The squirrel chases the squirrel.[(((triple5) -> rule3))] The tiger is kind.[(((triple7) -> rule1))] @2: The squirrel likes the tiger.[(((((triple5) -> rule3)) -> rule5))] @3: The rabbit is red.[(((((((triple5) -> rule3)) -> rule5) triple6) -> rule6))]
The rabbit does not chase the squirrel.
("rabbit" "chases" "squirrel" "-")
triple1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple2
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple5
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple5) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple7) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((((triple5) -> (rule3 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3