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