The cow is kind. The cow is red. The cow likes the dog. The cow likes the squirrel. The dog is kind. The lion is not green. The lion likes the squirrel. The squirrel chases the dog. The squirrel is not big. The squirrel is not red. The squirrel likes the cow. The squirrel needs the dog. If someone likes the dog then the dog does not like the squirrel. If someone likes the dog then the dog does not need the cow. If someone chases the dog then the dog is red. If the lion likes the cow and the cow needs the dog then the cow is green. If someone likes the squirrel then they are rough. If the lion does not need the cow then the lion chases the squirrel. If someone chases the dog and the dog does not need the cow then the dog is big. If someone is big then they chase the lion.
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The dog is kind.
("dog" "is" "kind" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If someone likes the dog then the dog does not like the squirrel.
((("someone" "likes" "dog" "+")) -> ("dog" "likes" "squirrel" "-"))
If someone likes the dog then the dog does not need the cow.
((("someone" "likes" "dog" "+")) -> ("dog" "needs" "cow" "-"))
If someone chases the dog then the dog is red.
((("someone" "chases" "dog" "+")) -> ("dog" "is" "red" "+"))
If the lion likes the cow and the cow needs the dog then the cow is green.
((("lion" "likes" "cow" "+") ("cow" "needs" "dog" "+")) -> ("cow" "is" "green" "+"))
If someone likes the squirrel then they are rough.
((("someone" "likes" "squirrel" "+")) -> ("someone" "is" "rough" "+"))
If the lion does not need the cow then the lion chases the squirrel.
((("lion" "needs" "cow" "~")) -> ("lion" "chases" "squirrel" "+"))
If someone chases the dog and the dog does not need the cow then the dog is big.
((("someone" "chases" "dog" "+") ("dog" "needs" "cow" "~")) -> ("dog" "is" "big" "+"))
If someone is big then they chase the lion.
((("someone" "is" "big" "+")) -> ("someone" "chases" "lion" "+"))
The cow is kind.
True
1
proof
[(triple1)]
("cow" "is" "kind" "+")
triple1
The squirrel does not need the dog.
False
1
inv-proof
[(triple12)]
("squirrel" "needs" "dog" "-")
triple12
The dog does not need the cow.
True
2
proof
[(((triple3) -> rule2))]
("dog" "needs" "cow" "-")
((triple3) -> (rule2 % int1))
The dog does not need the cow.
("dog" "needs" "cow" "-")
int1
The lion is not rough.
False
2
inv-proof
[(((triple7) -> rule5))]
("lion" "is" "rough" "-")
((triple7) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "rough" "-")
The cow is green.
Unknown
rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "green" "+")
The dog does not chase the squirrel.
Unknown
inv-random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The cow is kind.[(triple1)] The cow is red.[(triple2)] The cow likes the dog.[(triple3)] The cow likes the squirrel.[(triple4)] The dog is kind.[(triple5)] The lion is not green.[(triple6)] The lion likes the squirrel.[(triple7)] The squirrel chases the dog.[(triple8)] The squirrel is not big.[(triple9)] The squirrel is not red.[(triple10)] The squirrel likes the cow.[(triple11)] The squirrel needs the dog.[(triple12)] @1: The cow is rough.[(((triple4) -> rule5))] The dog does not like the squirrel.[(((triple3) -> rule1))] The dog does not need the cow.[(((triple3) -> rule2))] The dog is red.[(((triple8) -> rule3))] The lion is rough.[(((triple7) -> rule5))] @2: The dog is big.[(((triple8 ((triple3) -> rule2)) -> rule7))] @3: The dog chases the lion.[(((((triple8 ((triple3) -> rule2)) -> rule7)) -> rule8))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The lion is not green.
("lion" "is" "green" "-")
triple6
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple7
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple8
The squirrel is not big.
("squirrel" "is" "big" "-")
triple9
The squirrel is not red.
("squirrel" "is" "red" "-")
triple10
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple11
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple12
The cow is rough.
("cow" "is" "rough" "+")
((triple4) -> (rule5 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The dog does not like the squirrel.
("dog" "likes" "squirrel" "-")
((triple3) -> (rule1 % int1))
The dog does not like the squirrel.
("dog" "likes" "squirrel" "-")
int1
The dog does not need the cow.
("dog" "needs" "cow" "-")
((triple3) -> (rule2 % int1))
The dog does not need the cow.
("dog" "needs" "cow" "-")
int1
The dog is red.
("dog" "is" "red" "+")
((triple8) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple7) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((triple8 ((triple3) -> (rule2 % int2))) -> (rule7 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog does not need the cow.
("dog" "needs" "cow" "-")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
((((triple8 ((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog does not need the cow.
("dog" "needs" "cow" "-")
int3