The bear chases the mouse. The bear is cold. The bear is kind. The bear is nice. The bear is red. The bear is round. The bear likes the mouse. The bear sees the mouse. The mouse chases the bear. The mouse is round. The mouse likes the bear. The mouse sees the bear. If someone likes the bear and the bear sees the mouse then the bear chases the mouse. If someone sees the mouse then the mouse is cold. If someone chases the mouse and the mouse sees the bear then the bear sees the mouse. If someone chases the bear then the bear is red. If someone likes the mouse then they are round. If someone is nice and they chase the mouse then they are cold. If someone sees the bear and they are cold then they see the mouse. If someone sees the mouse and they see the bear then they are kind.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If someone likes the bear and the bear sees the mouse then the bear chases the mouse.
((("someone" "likes" "bear" "+") ("bear" "sees" "mouse" "+")) -> ("bear" "chases" "mouse" "+"))
If someone sees the mouse then the mouse is cold.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If someone chases the mouse and the mouse sees the bear then the bear sees the mouse.
((("someone" "chases" "mouse" "+") ("mouse" "sees" "bear" "+")) -> ("bear" "sees" "mouse" "+"))
If someone chases the bear then the bear is red.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "red" "+"))
If someone likes the mouse then they are round.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and they chase the mouse then they are cold.
((("someone" "is" "nice" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the bear and they are cold then they see the mouse.
((("someone" "sees" "bear" "+") ("someone" "is" "cold" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse and they see the bear then they are kind.
((("someone" "sees" "mouse" "+") ("someone" "sees" "bear" "+")) -> ("someone" "is" "kind" "+"))
The mouse likes the bear.
True
1
proof
[(triple11)]
("mouse" "likes" "bear" "+")
triple11
The bear is not red.
False
1
inv-proof
[(triple5 OR ((triple9) -> rule4))]
("bear" "is" "red" "-")
triple5
((triple9) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The mouse is cold.
True
2
proof
[(((triple8) -> rule2) OR ((((triple1 triple12) -> rule3)) -> rule2))]
("mouse" "is" "cold" "+")
((triple8) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((((triple1 triple12) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The mouse is not cold.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple1 triple12) -> rule3)) -> rule2))]
("mouse" "is" "cold" "-")
((triple8) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((((triple1 triple12) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The mouse sees the mouse.
True
4
proof
[(((triple12 ((triple8) -> rule2)) -> rule7) OR ((triple12 ((((triple1 triple12) -> rule3)) -> rule2)) -> rule7))]
("mouse" "sees" "mouse" "+")
((triple12 ((triple8) -> (rule2 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((triple12 ((((triple1 triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The mouse does not see the mouse.
False
4
inv-proof
[(((triple12 ((triple8) -> rule2)) -> rule7) OR ((triple12 ((((triple1 triple12) -> rule3)) -> rule2)) -> rule7))]
("mouse" "sees" "mouse" "-")
((triple12 ((triple8) -> (rule2 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((triple12 ((((triple1 triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The mouse is kind.
True
6
proof
[(((((triple12 ((triple8) -> rule2)) -> rule7) triple12) -> rule8) OR ((((triple12 ((((triple1 triple12) -> rule3)) -> rule2)) -> rule7) triple12) -> rule8))]
("mouse" "is" "kind" "+")
((((triple12 ((triple8) -> (rule2 % int3))) -> (rule7 % int2)) triple12) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((((triple12 ((((triple1 triple12) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple12) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The mouse is not kind.
False
6
inv-proof
[(((((triple12 ((triple8) -> rule2)) -> rule7) triple12) -> rule8) OR ((((triple12 ((((triple1 triple12) -> rule3)) -> rule2)) -> rule7) triple12) -> rule8))]
("mouse" "is" "kind" "-")
((((triple12 ((triple8) -> (rule2 % int3))) -> (rule7 % int2)) triple12) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((((triple12 ((((triple1 triple12) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple12) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear chases the mouse.[(triple1 OR ((triple11 triple8) -> rule1))] The bear is cold.[(triple2 OR ((triple4 triple1) -> rule6) OR ((triple4 ((triple11 triple8) -> rule1)) -> rule6))] The bear is kind.[(triple3)] The bear is nice.[(triple4)] The bear is red.[(triple5 OR ((triple9) -> rule4))] The bear is round.[(triple6 OR ((triple7) -> rule5))] The bear likes the mouse.[(triple7)] The bear sees the mouse.[(triple8 OR ((triple1 triple12) -> rule3))] The mouse chases the bear.[(triple9)] The mouse is round.[(triple10)] The mouse likes the bear.[(triple11)] The mouse sees the bear.[(triple12)] @1: The mouse is cold.[(((triple8) -> rule2) OR ((((triple1 triple12) -> rule3)) -> rule2))] @2: The mouse sees the mouse.[(((triple12 ((triple8) -> rule2)) -> rule7) OR ((triple12 ((((triple1 triple12) -> rule3)) -> rule2)) -> rule7))] @3: The mouse is kind.[(((((triple12 ((triple8) -> rule2)) -> rule7) triple12) -> rule8) OR ((((triple12 ((((triple1 triple12) -> rule3)) -> rule2)) -> rule7) triple12) -> rule8))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
((triple11 triple8) -> (rule1 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple4 ((triple11 triple8) -> (rule1 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
triple5
((triple9) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple6
((triple7) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple7
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple8
((triple1 triple12) -> (rule3 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple11
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple12
The mouse is cold.
("mouse" "is" "cold" "+")
((triple8) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((((triple1 triple12) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple12 ((triple8) -> (rule2 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((triple12 ((((triple1 triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple12 ((triple8) -> (rule2 % int3))) -> (rule7 % int2)) triple12) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
((((triple12 ((((triple1 triple12) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple12) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int4