The bear is kind. The bear is young. The bear sees the cow. The bear visits the mouse. The cow eats the mouse. The cow eats the squirrel. The cow is young. The cow sees the bear. The cow visits the bear. The mouse eats the bear. The mouse is cold. The mouse is young. The mouse sees the squirrel. The mouse visits the bear. The squirrel sees the cow. The squirrel sees the mouse. If someone sees the mouse and they visit the squirrel then the squirrel visits the bear. If someone visits the squirrel then they see the mouse. If someone visits the bear then they are round. If someone eats the squirrel and they see the cow then the squirrel is young. If someone eats the squirrel then they visit the squirrel. If the squirrel is round and the squirrel sees the bear then the squirrel eats the cow. If someone sees the mouse then they see the bear.
The bear is kind.
("bear" "is" "kind" "+")
The bear is young.
("bear" "is" "young" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone sees the mouse and they visit the squirrel then the squirrel visits the bear.
((("someone" "sees" "mouse" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "bear" "+"))
If someone visits the squirrel then they see the mouse.
((("someone" "visits" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone visits the bear then they are round.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone eats the squirrel and they see the cow then the squirrel is young.
((("someone" "eats" "squirrel" "+") ("someone" "sees" "cow" "+")) -> ("squirrel" "is" "young" "+"))
If someone eats the squirrel then they visit the squirrel.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If the squirrel is round and the squirrel sees the bear then the squirrel eats the cow.
((("squirrel" "is" "round" "+") ("squirrel" "sees" "bear" "+")) -> ("squirrel" "eats" "cow" "+"))
If someone sees the mouse then they see the bear.
((("someone" "sees" "mouse" "+")) -> ("someone" "sees" "bear" "+"))
The bear is kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "+")
triple1
The cow does not visit the bear.
False
1
inv-proof
[(triple9)]
("cow" "visits" "bear" "-")
triple9
The cow visits the squirrel.
True
2
proof
[(((triple6) -> rule5))]
("cow" "visits" "squirrel" "+")
((triple6) -> (rule5 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The squirrel does not see the bear.
False
2
inv-proof
[(((triple16) -> rule7))]
("squirrel" "sees" "bear" "-")
((triple16) -> (rule7 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The cow sees the mouse.
True
3
proof
[(((((triple6) -> rule5)) -> rule2))]
("cow" "sees" "mouse" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow does not see the mouse.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule2))]
("cow" "sees" "mouse" "-")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The squirrel visits the bear.
True
6
proof
[(((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1))]
("squirrel" "visits" "bear" "+")
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2)) ((triple6) -> (rule5 % int3))) -> (rule1 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel does not visit the bear.
False
6
inv-proof
[(((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1))]
("squirrel" "visits" "bear" "-")
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2)) ((triple6) -> (rule5 % int3))) -> (rule1 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel is round.
True
7
proof
[(((((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1)) -> rule3))]
("squirrel" "is" "round" "+")
((((((((triple6) -> (rule5 % int4))) -> (rule2 % int3)) ((triple6) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int4
The squirrel is not round.
False
7
inv-proof
[(((((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1)) -> rule3))]
("squirrel" "is" "round" "-")
((((((((triple6) -> (rule5 % int4))) -> (rule2 % int3)) ((triple6) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int4
The squirrel eats the cow.
True
10
proof
[(((((((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1)) -> rule3) ((triple16) -> rule7)) -> rule6))]
("squirrel" "eats" "cow" "+")
((((((((((triple6) -> (rule5 % int6))) -> (rule2 % int5)) ((triple6) -> (rule5 % int6))) -> (rule1 % int4))) -> (rule3 % int3)) ((triple16) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int5
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int6
The squirrel does not eat the cow.
False
10
inv-proof
[(((((((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1)) -> rule3) ((triple16) -> rule7)) -> rule6))]
("squirrel" "eats" "cow" "-")
((((((((((triple6) -> (rule5 % int6))) -> (rule2 % int5)) ((triple6) -> (rule5 % int6))) -> (rule1 % int4))) -> (rule3 % int3)) ((triple16) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int5
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int6
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The bear sees the bear.
Unknown
rconc
[@3: The bear sees the bear.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule5 <- FAIL)]]
("bear" "sees" "bear" "+")
The mouse does not visit the squirrel.
Unknown
inv-rconc
[@1: The mouse visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "squirrel" "-")
The mouse sees the bear.
Unknown
rconc
[@3: The mouse sees the bear.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule5 <- FAIL)]]
("mouse" "sees" "bear" "+")
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "round" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "young" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The mouse visits the cow.
Unknown
random
[@0: The mouse visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cow" "+")
@0: The bear is kind.[(triple1)] The bear is young.[(triple2)] The bear sees the cow.[(triple3)] The bear visits the mouse.[(triple4)] The cow eats the mouse.[(triple5)] The cow eats the squirrel.[(triple6)] The cow is young.[(triple7)] The cow sees the bear.[(triple8 OR ((((((triple6) -> rule5)) -> rule2)) -> rule7))] The cow visits the bear.[(triple9)] The mouse eats the bear.[(triple10)] The mouse is cold.[(triple11)] The mouse is young.[(triple12)] The mouse sees the squirrel.[(triple13)] The mouse visits the bear.[(triple14)] The squirrel sees the cow.[(triple15)] The squirrel sees the mouse.[(triple16)] @1: The cow is round.[(((triple9) -> rule3))] The cow visits the squirrel.[(((triple6) -> rule5))] The mouse is round.[(((triple14) -> rule3))] The squirrel sees the bear.[(((triple16) -> rule7))] @2: The cow sees the mouse.[(((((triple6) -> rule5)) -> rule2))] @3: The squirrel visits the bear.[(((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1))] @4: The squirrel is round.[(((((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1)) -> rule3))] @5: The squirrel eats the cow.[(((((((((((triple6) -> rule5)) -> rule2) ((triple6) -> rule5)) -> rule1)) -> rule3) ((triple16) -> rule7)) -> rule6))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple4
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple5
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple6
The cow is young.
("cow" "is" "young" "+")
triple7
The cow sees the bear.
("cow" "sees" "bear" "+")
triple8
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The cow visits the bear.
("cow" "visits" "bear" "+")
triple9
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple13
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple14
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple15
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple16
The cow is round.
("cow" "is" "round" "+")
((triple9) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((triple6) -> (rule5 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple14) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((triple16) -> (rule7 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2)) ((triple6) -> (rule5 % int3))) -> (rule1 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
((((((((triple6) -> (rule5 % int4))) -> (rule2 % int3)) ((triple6) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int2
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int4
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((((((((((triple6) -> (rule5 % int6))) -> (rule2 % int5)) ((triple6) -> (rule5 % int6))) -> (rule1 % int4))) -> (rule3 % int3)) ((triple16) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int5
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int6