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