The bear chases the mouse. The bear is cold. The bear is nice. The bear needs the mouse. The bear sees the mouse. The mouse chases the bear. The mouse is cold. The mouse is green. The mouse is nice. The mouse is young. The mouse needs the bear. The mouse sees the bear. If something sees the bear then it chases the bear. If something is rough and it sees the mouse then the mouse is cold. If something is young then it sees the bear. If something needs the mouse then the mouse chases the bear. If something needs the mouse then it is young. If something sees the bear then it is green. If something sees the mouse then it chases the mouse. All young, nice things are green.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If something sees the bear then it chases the bear.
((("something" "sees" "bear" "+")) -> ("something" "chases" "bear" "+"))
If something is rough and it sees the mouse then the mouse is cold.
((("something" "is" "rough" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something is young then it sees the bear.
((("something" "is" "young" "+")) -> ("something" "sees" "bear" "+"))
If something needs the mouse then the mouse chases the bear.
((("something" "needs" "mouse" "+")) -> ("mouse" "chases" "bear" "+"))
If something needs the mouse then it is young.
((("something" "needs" "mouse" "+")) -> ("something" "is" "young" "+"))
If something sees the bear then it is green.
((("something" "sees" "bear" "+")) -> ("something" "is" "green" "+"))
If something sees the mouse then it chases the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
All young, nice things are green.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
The mouse sees the bear.
True
1
proof
[(triple12 OR ((triple10) -> rule3))]
("mouse" "sees" "bear" "+")
triple12
((triple10) -> (rule3 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The mouse is not young.
False
1
inv-proof
[(triple10)]
("mouse" "is" "young" "-")
triple10
The bear is young.
True
2
proof
[(((triple4) -> rule5))]
("bear" "is" "young" "+")
((triple4) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple4) -> rule5))]
("bear" "is" "young" "-")
((triple4) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the bear.
True
3
proof
[(((((triple4) -> rule5)) -> rule3))]
("bear" "sees" "bear" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not green.
False
4
inv-proof
[(((((triple4) -> rule5) triple3) -> rule8) OR ((((((triple4) -> rule5)) -> rule3)) -> rule6))]
("bear" "is" "green" "-")
((((triple4) -> (rule5 % int2)) triple3) -> (rule8 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear chases the bear.
True
4
proof
[(((((((triple4) -> rule5)) -> rule3)) -> rule1))]
("bear" "chases" "bear" "+")
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear does not chase the bear.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule3)) -> rule1))]
("bear" "chases" "bear" "-")
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
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 rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The bear chases the mouse.[(triple1 OR ((triple5) -> rule7))] The bear is cold.[(triple2)] The bear is nice.[(triple3)] The bear needs the mouse.[(triple4)] The bear sees the mouse.[(triple5)] The mouse chases the bear.[(triple6 OR ((triple12) -> rule1) OR ((triple4) -> rule4) OR ((((triple10) -> rule3)) -> rule1))] The mouse is cold.[(triple7)] The mouse is green.[(triple8 OR ((triple12) -> rule6) OR ((triple10 triple9) -> rule8) OR ((((triple10) -> rule3)) -> rule6))] The mouse is nice.[(triple9)] The mouse is young.[(triple10)] The mouse needs the bear.[(triple11)] The mouse sees the bear.[(triple12 OR ((triple10) -> rule3))] @1: The bear is young.[(((triple4) -> rule5))] @2: The bear is green.[(((((triple4) -> rule5) triple3) -> rule8) OR ((((((triple4) -> rule5)) -> rule3)) -> rule6))] The bear sees the bear.[(((((triple4) -> rule5)) -> rule3))] @3: The bear chases the bear.[(((((((triple4) -> rule5)) -> rule3)) -> rule1))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
((triple5) -> (rule7 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple5
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple6
((triple12) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
((triple4) -> (rule4 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
((triple12) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple10 triple9) -> (rule8 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple11
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple12
((triple10) -> (rule3 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((triple4) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple4) -> (rule5 % int2)) triple3) -> (rule8 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear sees the bear.
("bear" "sees" "bear" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
((((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3