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