The bear is blue. The bear is young. The bear does not need the lion. The bear visits the lion. The cat is blue. The cat visits the cow. The cow chases the lion. The cow is blue. The cow does not need the lion. The lion chases the cow. The lion is green. The lion is round. The lion needs the cat. The lion needs the cow. The lion visits the cat. The lion does not visit the cow. If something visits the lion then the lion is not blue. All big things are not young.
The bear is blue.
("bear" "is" "blue" "+")
The bear is young.
("bear" "is" "young" "+")
The bear does not need the lion.
("bear" "needs" "lion" "-")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow does not need the lion.
("cow" "needs" "lion" "-")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion does not visit the cow.
("lion" "visits" "cow" "-")
If something visits the lion then the lion is not blue.
((("something" "visits" "lion" "+")) -> ("lion" "is" "blue" "-"))
All big things are not young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
The cow does not need the lion.
True
1
proof
[(triple9)]
("cow" "needs" "lion" "-")
triple9
The cat is not blue.
False
1
inv-proof
[(triple5)]
("cat" "is" "blue" "-")
triple5
The bear does not need the cow.
Unknown
inv-random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "-")
The cow visits the cat.
Unknown
random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "+")
@0: The bear does not need the lion.[(triple3)] The bear is blue.[(triple1)] The bear is young.[(triple2)] The bear visits the lion.[(triple4)] The cat is blue.[(triple5)] The cat visits the cow.[(triple6)] The cow chases the lion.[(triple7)] The cow does not need the lion.[(triple9)] The cow is blue.[(triple8)] The lion chases the cow.[(triple10)] The lion does not visit the cow.[(triple16)] The lion is green.[(triple11)] The lion is round.[(triple12)] The lion needs the cat.[(triple13)] The lion needs the cow.[(triple14)] The lion visits the cat.[(triple15)] @1: The lion is not blue.[(((triple4) -> rule1))]
The bear does not need the lion.
("bear" "needs" "lion" "-")
triple3
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple4
The cat is blue.
("cat" "is" "blue" "+")
triple5
The cat visits the cow.
("cat" "visits" "cow" "+")
triple6
The cow chases the lion.
("cow" "chases" "lion" "+")
triple7
The cow does not need the lion.
("cow" "needs" "lion" "-")
triple9
The cow is blue.
("cow" "is" "blue" "+")
triple8
The lion chases the cow.
("lion" "chases" "cow" "+")
triple10
The lion does not visit the cow.
("lion" "visits" "cow" "-")
triple16
The lion is green.
("lion" "is" "green" "+")
triple11
The lion is round.
("lion" "is" "round" "+")
triple12
The lion needs the cat.
("lion" "needs" "cat" "+")
triple13
The lion needs the cow.
("lion" "needs" "cow" "+")
triple14
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The lion is not blue.
("lion" "is" "blue" "-")
((triple4) -> (rule1 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1