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