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