The bear is nice. The cow is nice. The tiger chases the bear. If something is round then it chases the cow. If something is round and it chases the bear then the bear chases the cow. If something chases the cow then the cow chases the bear. If something is big and it eats the cow then it eats the bear. If something is nice and it eats the cow then the cow eats the tiger. If something chases the bear then the bear eats the tiger.
The bear is nice.
("bear" "is" "nice" "+")
The cow is nice.
("cow" "is" "nice" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something is round then it chases the cow.
((("something" "is" "round" "+")) -> ("something" "chases" "cow" "+"))
If something is round and it chases the bear then the bear chases the cow.
((("something" "is" "round" "+") ("something" "chases" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If something chases the cow then the cow chases the bear.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "bear" "+"))
If something is big and it eats the cow then it eats the bear.
((("something" "is" "big" "+") ("something" "eats" "cow" "+")) -> ("something" "eats" "bear" "+"))
If something is nice and it eats the cow then the cow eats the tiger.
((("something" "is" "nice" "+") ("something" "eats" "cow" "+")) -> ("cow" "eats" "tiger" "+"))
If something chases the bear then the bear eats the tiger.
((("something" "chases" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
The cow is nice.
True
1
proof
[(triple2)]
("cow" "is" "nice" "+")
triple2
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "bear" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The bear is nice.[(triple1)] The cow is nice.[(triple2)] The tiger chases the bear.[(triple3)] @1: The bear eats the tiger.[(((triple3) -> rule6))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((triple3) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1