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