The bear is big. The bear needs the cow. The bear sees the cow. The cow chases the bear. The cow chases the dog. The cow sees the bear. The cow sees the dog. The dog chases the cow. The mouse is blue. The mouse sees the cow. If something is nice then it needs the bear. If something sees the dog then it is nice. If the mouse needs the dog then the dog chases the mouse. If something sees the mouse and it is not blue then it is red. If something is rough and it sees the dog then it chases the dog. If something chases the dog then the dog does not need the mouse. If something sees the dog then the dog is nice. If the mouse does not chase the dog and the dog does not see the cow then the dog sees the bear.
The bear is big.
("bear" "is" "big" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something is nice then it needs the bear.
((("something" "is" "nice" "+")) -> ("something" "needs" "bear" "+"))
If something sees the dog then it is nice.
((("something" "sees" "dog" "+")) -> ("something" "is" "nice" "+"))
If the mouse needs the dog then the dog chases the mouse.
((("mouse" "needs" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If something sees the mouse and it is not blue then it is red.
((("something" "sees" "mouse" "+") ("something" "is" "blue" "~")) -> ("something" "is" "red" "+"))
If something is rough and it sees the dog then it chases the dog.
((("something" "is" "rough" "+") ("something" "sees" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something chases the dog then the dog does not need the mouse.
((("something" "chases" "dog" "+")) -> ("dog" "needs" "mouse" "-"))
If something sees the dog then the dog is nice.
((("something" "sees" "dog" "+")) -> ("dog" "is" "nice" "+"))
If the mouse does not chase the dog and the dog does not see the cow then the dog sees the bear.
((("mouse" "chases" "dog" "~") ("dog" "sees" "cow" "~")) -> ("dog" "sees" "bear" "+"))
The mouse is blue.
True
1
proof
[(triple9)]
("mouse" "is" "blue" "+")
triple9
The cow does not see the bear.
False
1
inv-proof
[(triple6)]
("cow" "sees" "bear" "-")
triple6
The dog is nice.
True
2
proof
[(((triple7) -> rule7))]
("dog" "is" "nice" "+")
((triple7) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple7) -> rule2))]
("cow" "is" "nice" "-")
((triple7) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow needs the bear.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("cow" "needs" "bear" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow does not need the bear.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("cow" "needs" "bear" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The mouse does not chase the dog.
Unknown
inv-rconc
[@1: The mouse chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "dog" "-")
The dog sees the bear.
Unknown
rconc
[@1: The dog sees the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "sees" "bear" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "dog" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The bear chases the mouse.
Unknown
random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "+")
@0: The bear is big.[(triple1)] The bear needs the cow.[(triple2)] The bear sees the cow.[(triple3)] The cow chases the bear.[(triple4)] The cow chases the dog.[(triple5)] The cow sees the bear.[(triple6)] The cow sees the dog.[(triple7)] The dog chases the cow.[(triple8)] The mouse is blue.[(triple9)] The mouse sees the cow.[(triple10)] @1: The cow is nice.[(((triple7) -> rule2))] The dog does not need the mouse.[(((triple5) -> rule6))] The dog is nice.[(((triple7) -> rule7))] @2: The cow needs the bear.[(((((triple7) -> rule2)) -> rule1))] The dog needs the bear.[(((((triple7) -> rule7)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple2
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple4
The cow chases the dog.
("cow" "chases" "dog" "+")
triple5
The cow sees the bear.
("cow" "sees" "bear" "+")
triple6
The cow sees the dog.
("cow" "sees" "dog" "+")
triple7
The dog chases the cow.
("dog" "chases" "cow" "+")
triple8
The mouse is blue.
("mouse" "is" "blue" "+")
triple9
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
The cow is nice.
("cow" "is" "nice" "+")
((triple7) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The dog does not need the mouse.
("dog" "needs" "mouse" "-")
((triple5) -> (rule6 % int1))
The dog does not need the mouse.
("dog" "needs" "mouse" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple7) -> (rule7 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The dog needs the bear.
("dog" "needs" "bear" "+")
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2