The cat eats the tiger. The cat is red. The mouse eats the tiger. The mouse is nice. The mouse needs the squirrel. The mouse sees the cat. The mouse sees the tiger. The squirrel eats the mouse. The squirrel is nice. The squirrel is red. The squirrel sees the tiger. The tiger eats the cat. The tiger eats the mouse. The tiger is green. The tiger is nice. The tiger needs the squirrel. If someone needs the mouse and the mouse sees the tiger then they are nice. If someone sees the tiger and they eat the tiger then they see the squirrel. If the mouse is green and the mouse needs the tiger then the tiger eats the cat. If someone needs the cat then the cat sees the squirrel. If someone sees the squirrel then they see the mouse. If someone sees the mouse and they see the cat then the cat sees the tiger. If someone eats the tiger then the tiger eats the mouse.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is red.
("cat" "is" "red" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If someone needs the mouse and the mouse sees the tiger then they are nice.
((("someone" "needs" "mouse" "+") ("mouse" "sees" "tiger" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the tiger and they eat the tiger then they see the squirrel.
((("someone" "sees" "tiger" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "sees" "squirrel" "+"))
If the mouse is green and the mouse needs the tiger then the tiger eats the cat.
((("mouse" "is" "green" "+") ("mouse" "needs" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If someone needs the cat then the cat sees the squirrel.
((("someone" "needs" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If someone sees the squirrel then they see the mouse.
((("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse and they see the cat then the cat sees the tiger.
((("someone" "sees" "mouse" "+") ("someone" "sees" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If someone eats the tiger then the tiger eats the mouse.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
The mouse needs the squirrel.
True
1
proof
[(triple5)]
("mouse" "needs" "squirrel" "+")
triple5
The squirrel is not nice.
False
1
inv-proof
[(triple9)]
("squirrel" "is" "nice" "-")
triple9
The mouse sees the squirrel.
True
3
proof
[(((triple7 triple3) -> rule2))]
("mouse" "sees" "squirrel" "+")
((triple7 triple3) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
3
inv-proof
[(((triple7 triple3) -> rule2))]
("mouse" "sees" "squirrel" "-")
((triple7 triple3) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse sees the mouse.
True
4
proof
[(((((triple7 triple3) -> rule2)) -> rule5))]
("mouse" "sees" "mouse" "+")
((((triple7 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse does not see the mouse.
False
4
inv-proof
[(((((triple7 triple3) -> rule2)) -> rule5))]
("mouse" "sees" "mouse" "-")
((((triple7 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The cat sees the tiger.
True
6
proof
[(((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6))]
("cat" "sees" "tiger" "+")
((((((triple7 triple3) -> (rule2 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The cat does not see the tiger.
False
6
inv-proof
[(((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6))]
("cat" "sees" "tiger" "-")
((((((triple7 triple3) -> (rule2 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The cat sees the squirrel.
True
8
proof
[(((((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6) triple1) -> rule2))]
("cat" "sees" "squirrel" "+")
((((((((triple7 triple3) -> (rule2 % int4))) -> (rule5 % int3)) triple6) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int4
The cat does not see the squirrel.
False
8
inv-proof
[(((((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6) triple1) -> rule2))]
("cat" "sees" "squirrel" "-")
((((((((triple7 triple3) -> (rule2 % int4))) -> (rule5 % int3)) triple6) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int4
The cat sees the mouse.
True
9
proof
[(((((((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6) triple1) -> rule2)) -> rule5))]
("cat" "sees" "mouse" "+")
((((((((((triple7 triple3) -> (rule2 % int5))) -> (rule5 % int4)) triple6) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int5
The cat does not see the mouse.
False
9
inv-proof
[(((((((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6) triple1) -> rule2)) -> rule5))]
("cat" "sees" "mouse" "-")
((((((((((triple7 triple3) -> (rule2 % int5))) -> (rule5 % int4)) triple6) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int5
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The tiger sees the squirrel.
Unknown
rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The squirrel does not see the mouse.
Unknown
inv-rconc
[@2: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("squirrel" "sees" "mouse" "-")
The tiger sees the mouse.
Unknown
rconc
[@2: The tiger sees the mouse.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("tiger" "sees" "mouse" "+")
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not eat the cat.
Unknown
inv-random
[@0: The mouse eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat eats the tiger.[(triple1)] The cat is red.[(triple2)] The mouse eats the tiger.[(triple3)] The mouse is nice.[(triple4)] The mouse needs the squirrel.[(triple5)] The mouse sees the cat.[(triple6)] The mouse sees the tiger.[(triple7)] The squirrel eats the mouse.[(triple8)] The squirrel is nice.[(triple9)] The squirrel is red.[(triple10)] The squirrel sees the tiger.[(triple11)] The tiger eats the cat.[(triple12)] The tiger eats the mouse.[(triple13 OR ((triple1) -> rule7) OR ((triple3) -> rule7))] The tiger is green.[(triple14)] The tiger is nice.[(triple15)] The tiger needs the squirrel.[(triple16)] @1: The mouse sees the squirrel.[(((triple7 triple3) -> rule2))] @2: The mouse sees the mouse.[(((((triple7 triple3) -> rule2)) -> rule5))] @3: The cat sees the tiger.[(((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6))] @4: The cat sees the squirrel.[(((((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6) triple1) -> rule2))] @5: The cat sees the mouse.[(((((((((((triple7 triple3) -> rule2)) -> rule5) triple6) -> rule6) triple1) -> rule2)) -> rule5))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple5
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel is red.
("squirrel" "is" "red" "+")
triple10
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple11
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
((triple1) -> (rule7 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
((triple3) -> (rule7 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple15
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple16
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple7 triple3) -> (rule2 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple7 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((((((triple7 triple3) -> (rule2 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((((((triple7 triple3) -> (rule2 % int4))) -> (rule5 % int3)) triple6) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((((((((triple7 triple3) -> (rule2 % int5))) -> (rule5 % int4)) triple6) -> (rule6 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int5