The cat likes the tiger. The cat does not see the tiger. The mouse is not kind. The squirrel likes the mouse. The tiger likes the mouse. The tiger likes the squirrel. The tiger sees the mouse. If someone likes the mouse then the mouse visits the squirrel. If someone visits the squirrel and the squirrel visits the cat then the cat is kind. If the mouse visits the squirrel then the mouse likes the tiger. If the mouse likes the tiger then the mouse is green. If someone visits the mouse then they see the cat. If the mouse is kind then the mouse likes the squirrel. If someone likes the squirrel and they like the mouse then the squirrel sees the cat. If the squirrel sees the cat and the squirrel is kind then the squirrel is not rough.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The mouse is not kind.
("mouse" "is" "kind" "-")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone likes the mouse then the mouse visits the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If someone visits the squirrel and the squirrel visits the cat then the cat is kind.
((("someone" "visits" "squirrel" "+") ("squirrel" "visits" "cat" "+")) -> ("cat" "is" "kind" "+"))
If the mouse visits the squirrel then the mouse likes the tiger.
((("mouse" "visits" "squirrel" "+")) -> ("mouse" "likes" "tiger" "+"))
If the mouse likes the tiger then the mouse is green.
((("mouse" "likes" "tiger" "+")) -> ("mouse" "is" "green" "+"))
If someone visits the mouse then they see the cat.
((("someone" "visits" "mouse" "+")) -> ("someone" "sees" "cat" "+"))
If the mouse is kind then the mouse likes the squirrel.
((("mouse" "is" "kind" "+")) -> ("mouse" "likes" "squirrel" "+"))
If someone likes the squirrel and they like the mouse then the squirrel sees the cat.
((("someone" "likes" "squirrel" "+") ("someone" "likes" "mouse" "+")) -> ("squirrel" "sees" "cat" "+"))
If the squirrel sees the cat and the squirrel is kind then the squirrel is not rough.
((("squirrel" "sees" "cat" "+") ("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "rough" "-"))
The tiger sees the mouse.
True
1
proof
[(triple7)]
("tiger" "sees" "mouse" "+")
triple7
The tiger does not like the mouse.
False
1
inv-proof
[(triple5)]
("tiger" "likes" "mouse" "-")
triple5
The squirrel sees the cat.
True
3
proof
[(((triple6 triple5) -> rule7))]
("squirrel" "sees" "cat" "+")
((triple6 triple5) -> (rule7 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The mouse does not visit the squirrel.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple5) -> rule1))]
("mouse" "visits" "squirrel" "-")
((triple4) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
((triple5) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse likes the tiger.
True
3
proof
[(((((triple4) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
("mouse" "likes" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse does not like the tiger.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
("mouse" "likes" "tiger" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is green.
True
4
proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule4) OR ((((((triple5) -> rule1)) -> rule3)) -> rule4))]
("mouse" "is" "green" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The mouse is not green.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule4) OR ((((((triple5) -> rule1)) -> rule3)) -> rule4))]
("mouse" "is" "green" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "cat" "-")
The mouse sees the cat.
Unknown
rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "cat" "+")
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The tiger sees the cat.
Unknown
rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "cat" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat does not see the tiger.[(triple2)] The cat likes the tiger.[(triple1)] The mouse is not kind.[(triple3)] The squirrel likes the mouse.[(triple4)] The tiger likes the mouse.[(triple5)] The tiger likes the squirrel.[(triple6)] The tiger sees the mouse.[(triple7)] @1: The mouse visits the squirrel.[(((triple4) -> rule1) OR ((triple5) -> rule1))] The squirrel sees the cat.[(((triple6 triple5) -> rule7))] @2: The mouse likes the tiger.[(((((triple4) -> rule1)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))] @3: The mouse is green.[(((((((triple4) -> rule1)) -> rule3)) -> rule4) OR ((((((triple5) -> rule1)) -> rule3)) -> rule4))]
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
The mouse is not kind.
("mouse" "is" "kind" "-")
triple3
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple4
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple5
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple4) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
((triple5) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple6 triple5) -> (rule7 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int3