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