The bear is cold. The mouse chases the bear. The mouse likes the bear. If the bear likes the mouse and the mouse chases the bear then the bear needs the mouse. If someone likes the mouse then they like the bear. Rough people are kind. If the mouse likes the bear and the bear needs the mouse then the mouse is rough. If someone chases the bear then they like the mouse. If someone chases the bear and the bear is rough then the bear chases the mouse. If someone likes the bear and the bear likes the mouse then they chase the mouse. If the bear is cold then the bear needs the mouse.
The bear is cold.
("bear" "is" "cold" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If the bear likes the mouse and the mouse chases the bear then the bear needs the mouse.
((("bear" "likes" "mouse" "+") ("mouse" "chases" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If someone likes the mouse then they like the bear.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "bear" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If the mouse likes the bear and the bear needs the mouse then the mouse is rough.
((("mouse" "likes" "bear" "+") ("bear" "needs" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If someone chases the bear then they like the mouse.
((("someone" "chases" "bear" "+")) -> ("someone" "likes" "mouse" "+"))
If someone chases the bear and the bear is rough then the bear chases the mouse.
((("someone" "chases" "bear" "+") ("bear" "is" "rough" "+")) -> ("bear" "chases" "mouse" "+"))
If someone likes the bear and the bear likes the mouse then they chase the mouse.
((("someone" "likes" "bear" "+") ("bear" "likes" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If the bear is cold then the bear needs the mouse.
((("bear" "is" "cold" "+")) -> ("bear" "needs" "mouse" "+"))
The mouse likes the bear.
True
1
proof
[(triple3 OR ((((triple2) -> rule5)) -> rule2))]
("mouse" "likes" "bear" "+")
triple3
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The bear is not cold.
False
1
inv-proof
[(triple1)]
("bear" "is" "cold" "-")
triple1
The bear needs the mouse.
True
2
proof
[(((triple1) -> rule8))]
("bear" "needs" "mouse" "+")
((triple1) -> (rule8 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not need the mouse.
False
2
inv-proof
[(((triple1) -> rule8))]
("bear" "needs" "mouse" "-")
((triple1) -> (rule8 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse is rough.
True
4
proof
[(((triple3 ((triple1) -> rule8)) -> rule4) OR ((((((triple2) -> rule5)) -> rule2) ((triple1) -> rule8)) -> rule4))]
("mouse" "is" "rough" "+")
((triple3 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((((triple2) -> (rule5 % int4))) -> (rule2 % int3)) ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse is not rough.
False
4
inv-proof
[(((triple3 ((triple1) -> rule8)) -> rule4) OR ((((((triple2) -> rule5)) -> rule2) ((triple1) -> rule8)) -> rule4))]
("mouse" "is" "rough" "-")
((triple3 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((((triple2) -> (rule5 % int4))) -> (rule2 % int3)) ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse is kind.
True
5
proof
[(((((triple3 ((triple1) -> rule8)) -> rule4)) -> rule3) OR ((((((((triple2) -> rule5)) -> rule2) ((triple1) -> rule8)) -> rule4)) -> rule3))]
("mouse" "is" "kind" "+")
((((triple3 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int4
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int5
The mouse is not kind.
False
5
inv-proof
[(((((triple3 ((triple1) -> rule8)) -> rule4)) -> rule3) OR ((((((((triple2) -> rule5)) -> rule2) ((triple1) -> rule8)) -> rule4)) -> rule3))]
("mouse" "is" "kind" "-")
((((triple3 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int4
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int5
The mouse does not chase the mouse.
Unknown
inv-rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "kind" "+")
The bear does not chase the mouse.
Unknown
inv-rconc
[@2: The bear chases the mouse.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("bear" "chases" "mouse" "-")
The bear likes the bear.
Unknown
rconc
[@2: The bear likes the bear.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("bear" "likes" "bear" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The bear is cold.[(triple1)] The mouse chases the bear.[(triple2)] The mouse likes the bear.[(triple3 OR ((((triple2) -> rule5)) -> rule2))] @1: The bear needs the mouse.[(((triple1) -> rule8))] The mouse likes the mouse.[(((triple2) -> rule5))] @2: The mouse is rough.[(((triple3 ((triple1) -> rule8)) -> rule4) OR ((((((triple2) -> rule5)) -> rule2) ((triple1) -> rule8)) -> rule4))] @3: The mouse is kind.[(((((triple3 ((triple1) -> rule8)) -> rule4)) -> rule3) OR ((((((((triple2) -> rule5)) -> rule2) ((triple1) -> rule8)) -> rule4)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple3
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple1) -> (rule8 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple2) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
((((((triple2) -> (rule5 % int4))) -> (rule2 % int3)) ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple3 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4)) ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int4
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int5