The cow is not big. The dog chases the lion. The lion chases the dog. If something chases the dog and it does not eat the dog then it is not kind. If something needs the dog then the dog eats the cow. If something chases the lion then the lion is green. If the dog eats the lion then the dog chases the cow. If something is kind and green then it eats the cow. If something chases the lion then it does not need the lion. Blue things are big. If something is big and it eats the cow then the cow chases the dog.
The cow is not big.
("cow" "is" "big" "-")
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
If something chases the dog and it does not eat the dog then it is not kind.
((("something" "chases" "dog" "+") ("something" "eats" "dog" "~")) -> ("something" "is" "kind" "-"))
If something needs the dog then the dog eats the cow.
((("something" "needs" "dog" "+")) -> ("dog" "eats" "cow" "+"))
If something chases the lion then the lion is green.
((("something" "chases" "lion" "+")) -> ("lion" "is" "green" "+"))
If the dog eats the lion then the dog chases the cow.
((("dog" "eats" "lion" "+")) -> ("dog" "chases" "cow" "+"))
If something is kind and green then it eats the cow.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "eats" "cow" "+"))
If something chases the lion then it does not need the lion.
((("something" "chases" "lion" "+")) -> ("something" "needs" "lion" "-"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is big and it eats the cow then the cow chases the dog.
((("something" "is" "big" "+") ("something" "eats" "cow" "+")) -> ("cow" "chases" "dog" "+"))
The lion chases the dog.
True
1
proof
[(triple3)]
("lion" "chases" "dog" "+")
triple3
The cow is big.
False
1
inv-proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The dog does not need the lion.
True
2
proof
[(((triple2) -> rule6))]
("dog" "needs" "lion" "-")
((triple2) -> (rule6 % int1))
The dog does not need the lion.
("dog" "needs" "lion" "-")
int1
The lion is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("lion" "is" "green" "-")
((triple2) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "big" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "cow" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion chases the cow.
Unknown
random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "+")
@0: The cow is not big.[(triple1)] The dog chases the lion.[(triple2)] The lion chases the dog.[(triple3)] @1: The dog does not need the lion.[(((triple2) -> rule6))] The lion is green.[(((triple2) -> rule3))]
The cow is not big.
("cow" "is" "big" "-")
triple1
The dog chases the lion.
("dog" "chases" "lion" "+")
triple2
The lion chases the dog.
("lion" "chases" "dog" "+")
triple3
The dog does not need the lion.
("dog" "needs" "lion" "-")
((triple2) -> (rule6 % int1))
The dog does not need the lion.
("dog" "needs" "lion" "-")
int1
The lion is green.
("lion" "is" "green" "+")
((triple2) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1