The lion chases the rabbit. The lion is cold. The lion is kind. The lion sees the rabbit. The rabbit chases the lion. The rabbit eats the lion. The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is kind. The rabbit is round. The rabbit sees the lion. If someone sees the rabbit and they chase the lion then the lion is blue. If someone is blue then they eat the lion. If someone is round then they see the rabbit.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone sees the rabbit and they chase the lion then the lion is blue.
((("someone" "sees" "rabbit" "+") ("someone" "chases" "lion" "+")) -> ("lion" "is" "blue" "+"))
If someone is blue then they eat the lion.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "lion" "+"))
If someone is round then they see the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "sees" "rabbit" "+"))
The lion chases the rabbit.
True
1
proof
[(triple1)]
("lion" "chases" "rabbit" "+")
triple1
The rabbit is not blue.
False
1
inv-proof
[(triple8)]
("rabbit" "is" "blue" "-")
triple8
The rabbit sees the rabbit.
True
2
proof
[(((triple11) -> rule3))]
("rabbit" "sees" "rabbit" "+")
((triple11) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple11) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((triple11) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The lion is blue.
True
4
proof
[(((((triple11) -> rule3) triple5) -> rule1))]
("lion" "is" "blue" "+")
((((triple11) -> (rule3 % int2)) triple5) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The lion is not blue.
False
4
inv-proof
[(((((triple11) -> rule3) triple5) -> rule1))]
("lion" "is" "blue" "-")
((((triple11) -> (rule3 % int2)) triple5) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The lion eats the lion.
True
5
proof
[(((((((triple11) -> rule3) triple5) -> rule1)) -> rule2))]
("lion" "eats" "lion" "+")
((((((triple11) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The lion does not eat the lion.
False
5
inv-proof
[(((((((triple11) -> rule3) triple5) -> rule1)) -> rule2))]
("lion" "eats" "lion" "-")
((((((triple11) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion eats the rabbit.
Unknown
random
[@0: The lion eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "rabbit" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple3)] The lion sees the rabbit.[(triple4)] The rabbit chases the lion.[(triple5)] The rabbit eats the lion.[(triple6 OR ((triple8) -> rule2))] The rabbit is big.[(triple7)] The rabbit is blue.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is kind.[(triple10)] The rabbit is round.[(triple11)] The rabbit sees the lion.[(triple12)] @1: The rabbit sees the rabbit.[(((triple11) -> rule3))] @2: The lion is blue.[(((((triple11) -> rule3) triple5) -> rule1))] @3: The lion eats the lion.[(((((((triple11) -> rule3) triple5) -> rule1)) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple5
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
((triple8) -> (rule2 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple11) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((((triple11) -> (rule3 % int2)) triple5) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((triple11) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3