The lion chases the rabbit. The lion is big. The lion is blue. The lion is cold. The lion is red. The lion is round. The lion needs the rabbit. The lion sees the rabbit. The rabbit chases the lion. The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is red. The rabbit is round. The rabbit needs the lion. The rabbit does not see the lion. If something needs the rabbit then it needs the lion.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "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 red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
If something needs the rabbit then it needs the lion.
((("something" "needs" "rabbit" "+")) -> ("something" "needs" "lion" "+"))
The lion is blue.
True
1
proof
[(triple3)]
("lion" "is" "blue" "+")
triple3
The rabbit is not cold.
False
1
inv-proof
[(triple12)]
("rabbit" "is" "cold" "-")
triple12
The lion needs the lion.
True
2
proof
[(((triple7) -> rule1))]
("lion" "needs" "lion" "+")
((triple7) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "needs" "lion" "-")
((triple7) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
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 lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
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 lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion is cold.[(triple4)] The lion is red.[(triple5)] The lion is round.[(triple6)] The lion needs the rabbit.[(triple7)] The lion sees the rabbit.[(triple8)] The rabbit chases the lion.[(triple9)] The rabbit does not see the lion.[(triple16)] The rabbit is big.[(triple10)] The rabbit is blue.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is red.[(triple13)] The rabbit is round.[(triple14)] The rabbit needs the lion.[(triple15)] @1: The lion needs the lion.[(((triple7) -> rule1))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion is round.
("lion" "is" "round" "+")
triple6
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple7
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple8
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple9
The rabbit does not see the lion.
("rabbit" "sees" "lion" "-")
triple16
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple13
The rabbit is round.
("rabbit" "is" "round" "+")
triple14
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple7) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1