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