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