The cow chases the dog. The cow chases the lion. The cow sees the dog. The cow sees the lion. The dog is blue. The dog is red. The dog is round. The dog needs the lion. The dog sees the cow. The dog sees the lion. The lion is big. The lion is blue. If something needs the cow then the cow needs the dog. If something is blue then it needs the cow. If something needs the cow and the cow needs the lion then the lion sees the dog. If something chases the lion and the lion is big then the lion chases the cow. If something sees the lion then it sees the cow. If something needs the cow and it chases the lion then the cow sees the lion. If something sees the dog then the dog chases the lion. All round things are green.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
If something needs the cow then the cow needs the dog.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "dog" "+"))
If something is blue then it needs the cow.
((("something" "is" "blue" "+")) -> ("something" "needs" "cow" "+"))
If something needs the cow and the cow needs the lion then the lion sees the dog.
((("something" "needs" "cow" "+") ("cow" "needs" "lion" "+")) -> ("lion" "sees" "dog" "+"))
If something chases the lion and the lion is big then the lion chases the cow.
((("something" "chases" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "chases" "cow" "+"))
If something sees the lion then it sees the cow.
((("something" "sees" "lion" "+")) -> ("something" "sees" "cow" "+"))
If something needs the cow and it chases the lion then the cow sees the lion.
((("something" "needs" "cow" "+") ("something" "chases" "lion" "+")) -> ("cow" "sees" "lion" "+"))
If something sees the dog then the dog chases the lion.
((("something" "sees" "dog" "+")) -> ("dog" "chases" "lion" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
The lion is big.
True
1
proof
[(triple11)]
("lion" "is" "big" "+")
triple11
The lion is not blue.
False
1
inv-proof
[(triple12)]
("lion" "is" "blue" "-")
triple12
The lion does not see the cow.
Unknown
inv-rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "cow" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow chases the dog.[(triple1)] The cow chases the lion.[(triple2)] The cow sees the dog.[(triple3)] The cow sees the lion.[(triple4 OR ((((triple5) -> rule2) ((triple3) -> rule7)) -> rule6))] The dog is blue.[(triple5)] The dog is red.[(triple6)] The dog is round.[(triple7)] The dog needs the lion.[(triple8)] The dog sees the cow.[(triple9 OR ((triple10) -> rule5))] The dog sees the lion.[(triple10)] The lion is big.[(triple11)] The lion is blue.[(triple12)] @1: The cow sees the cow.[(((triple4) -> rule5) OR ((((((triple5) -> rule2) ((triple3) -> rule7)) -> rule6)) -> rule5))] The dog chases the lion.[(((triple3) -> rule7))] The dog is green.[(((triple7) -> rule8))] The dog needs the cow.[(((triple5) -> rule2))] The lion chases the cow.[(((triple2 triple11) -> rule4) OR ((((triple3) -> rule7) triple11) -> rule4))] The lion needs the cow.[(((triple12) -> rule2))] @2: The cow needs the dog.[(((((triple12) -> rule2)) -> rule1) OR ((((triple5) -> rule2)) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow chases the lion.
("cow" "chases" "lion" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
((((triple5) -> (rule2 % int3)) ((triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The dog sees the cow.
("dog" "sees" "cow" "+")
triple9
((triple10) -> (rule5 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
triple10
The lion is big.
("lion" "is" "big" "+")
triple11
The lion is blue.
("lion" "is" "blue" "+")
triple12
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple4) -> (rule5 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
((((((triple5) -> (rule2 % int4)) ((triple3) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The dog needs the cow.
("dog" "needs" "cow" "+")
int4
The dog chases the lion.
("dog" "chases" "lion" "+")
((triple3) -> (rule7 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((triple7) -> (rule8 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
((triple5) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple2 triple11) -> (rule4 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
((((triple3) -> (rule7 % int2)) triple11) -> (rule4 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple12) -> (rule2 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
((((triple12) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2