The bear chases the mouse. The bear is red. The bear is young. The bear likes the mouse. The bear visits the mouse. The mouse chases the bear. The mouse is blue. The mouse is kind. The mouse is nice. The mouse is red. The mouse likes the bear. The mouse visits the bear. If something is young then it chases the mouse. If something chases the mouse then it is red. If something visits the mouse and it is kind then the mouse likes the bear. If the mouse likes the bear and the mouse is blue then the mouse visits the bear. If something chases the mouse then it chases the bear. If something likes the mouse then it is blue.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something is young then it chases the mouse.
((("something" "is" "young" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse then it is red.
((("something" "chases" "mouse" "+")) -> ("something" "is" "red" "+"))
If something visits the mouse and it is kind then the mouse likes the bear.
((("something" "visits" "mouse" "+") ("something" "is" "kind" "+")) -> ("mouse" "likes" "bear" "+"))
If the mouse likes the bear and the mouse is blue then the mouse visits the bear.
((("mouse" "likes" "bear" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "visits" "bear" "+"))
If something chases the mouse then it chases the bear.
((("something" "chases" "mouse" "+")) -> ("something" "chases" "bear" "+"))
If something likes the mouse then it is blue.
((("something" "likes" "mouse" "+")) -> ("something" "is" "blue" "+"))
The bear likes the mouse.
True
1
proof
[(triple4)]
("bear" "likes" "mouse" "+")
triple4
The mouse is not kind.
False
1
inv-proof
[(triple8)]
("mouse" "is" "kind" "-")
triple8
The bear chases the bear.
True
2
proof
[(((triple1) -> rule5) OR ((((triple3) -> rule1)) -> rule5))]
("bear" "chases" "bear" "+")
((triple1) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear does not chase the bear.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((triple3) -> rule1)) -> rule5))]
("bear" "chases" "bear" "-")
((triple1) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bear chases the mouse.[(triple1 OR ((triple3) -> rule1))] The bear is red.[(triple2 OR ((triple1) -> rule2) OR ((((triple3) -> rule1)) -> rule2))] The bear is young.[(triple3)] The bear likes the mouse.[(triple4)] The bear visits the mouse.[(triple5)] The mouse chases the bear.[(triple6)] The mouse is blue.[(triple7)] The mouse is kind.[(triple8)] The mouse is nice.[(triple9)] The mouse is red.[(triple10)] The mouse likes the bear.[(triple11)] The mouse visits the bear.[(triple12 OR ((triple11 triple7) -> rule4))] @1: The bear chases the bear.[(((triple1) -> rule5) OR ((((triple3) -> rule1)) -> rule5))] The bear is blue.[(((triple4) -> rule6))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
((triple3) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is red.
("bear" "is" "red" "+")
triple2
((triple1) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple5
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse is red.
("mouse" "is" "red" "+")
triple10
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple11
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple12
((triple11 triple7) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple1) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((triple4) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1