The bear chases the mouse. The bear needs the mouse. The mouse chases the bear. The mouse is cold. The mouse is kind. The mouse is young. The mouse likes the bear. If something needs the mouse then the mouse is red. If something needs the bear then the bear chases the mouse. If something chases the mouse then it needs the bear. If something is cold and round then it needs the bear. If something is red then it chases the mouse. If something is cold and round then it does not like the bear.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If something needs the mouse then the mouse is red.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If something needs the bear then the bear chases the mouse.
((("something" "needs" "bear" "+")) -> ("bear" "chases" "mouse" "+"))
If something chases the mouse then it needs the bear.
((("something" "chases" "mouse" "+")) -> ("something" "needs" "bear" "+"))
If something is cold and round then it needs the bear.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "needs" "bear" "+"))
If something is red then it chases the mouse.
((("something" "is" "red" "+")) -> ("something" "chases" "mouse" "+"))
If something is cold and round then it does not like the bear.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "likes" "bear" "-"))
The mouse is kind.
True
1
proof
[(triple5)]
("mouse" "is" "kind" "+")
triple5
The mouse is not young.
False
1
inv-proof
[(triple6)]
("mouse" "is" "young" "-")
triple6
The mouse is red.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "is" "red" "+")
((triple2) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((((((((triple2) -> rule1)) -> rule5)) -> rule3)) -> rule2)) -> rule3))]
("bear" "needs" "bear" "-")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
((((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
The mouse chases the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("mouse" "chases" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not chase the mouse.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("mouse" "chases" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse needs the bear.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
("mouse" "needs" "bear" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse does not need the bear.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
("mouse" "needs" "bear" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the mouse.[(triple1 OR ((((((((triple2) -> rule1)) -> rule5)) -> rule3)) -> rule2))] The bear needs the mouse.[(triple2)] The mouse chases the bear.[(triple3)] The mouse is cold.[(triple4)] The mouse is kind.[(triple5)] The mouse is young.[(triple6)] The mouse likes the bear.[(triple7)] @1: The bear needs the bear.[(((triple1) -> rule3) OR ((((((((((triple2) -> rule1)) -> rule5)) -> rule3)) -> rule2)) -> rule3))] The mouse is red.[(((triple2) -> rule1))] @2: The mouse chases the mouse.[(((((triple2) -> rule1)) -> rule5))] @3: The mouse needs the bear.[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
((((((((triple2) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple7
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
((((((((((triple2) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
The mouse is red.
("mouse" "is" "red" "+")
((triple2) -> (rule1 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3