The cat sees the squirrel. The cat visits the rabbit. The rabbit eats the squirrel. The rabbit is rough. The rabbit sees the squirrel. The squirrel eats the cat. The squirrel sees the cat. If the cat is young then the cat is not nice. If the cat sees the squirrel and the squirrel eats the cat then the squirrel is not kind. If someone is kind then they eat the squirrel. If the squirrel sees the cat and the squirrel eats the cat then the cat visits the rabbit. If someone is cold then they do not visit the squirrel. If someone visits the cat then the cat visits the squirrel. If someone visits the rabbit then they are young. If someone visits the squirrel then the squirrel does not visit the cat.
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If the cat is young then the cat is not nice.
((("cat" "is" "young" "+")) -> ("cat" "is" "nice" "-"))
If the cat sees the squirrel and the squirrel eats the cat then the squirrel is not kind.
((("cat" "sees" "squirrel" "+") ("squirrel" "eats" "cat" "+")) -> ("squirrel" "is" "kind" "-"))
If someone is kind then they eat the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "squirrel" "+"))
If the squirrel sees the cat and the squirrel eats the cat then the cat visits the rabbit.
((("squirrel" "sees" "cat" "+") ("squirrel" "eats" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If someone is cold then they do not visit the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "squirrel" "-"))
If someone visits the cat then the cat visits the squirrel.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "squirrel" "+"))
If someone visits the rabbit then they are young.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "young" "+"))
If someone visits the squirrel then the squirrel does not visit the cat.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "cat" "-"))
The rabbit is rough.
True
1
proof
[(triple4)]
("rabbit" "is" "rough" "+")
triple4
The squirrel does not see the cat.
False
1
inv-proof
[(triple7)]
("squirrel" "sees" "cat" "-")
triple7
The squirrel is not kind.
True
3
proof
[(((triple1 triple6) -> rule2))]
("squirrel" "is" "kind" "-")
((triple1 triple6) -> (rule2 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1
The cat is not young.
False
2
inv-proof
[(((triple2) -> rule7) OR ((((triple7 triple6) -> rule4)) -> rule7))]
("cat" "is" "young" "-")
((triple2) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple7 triple6) -> (rule4 % int2))) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is not nice.
True
3
proof
[(((((triple2) -> rule7)) -> rule1) OR ((((((triple7 triple6) -> rule4)) -> rule7)) -> rule1))]
("cat" "is" "nice" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple7 triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The cat is nice.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule1) OR ((((((triple7 triple6) -> rule4)) -> rule7)) -> rule1))]
("cat" "is" "nice" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple7 triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cat visits the squirrel.
Unknown
rconc
[@1: The cat visits the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "squirrel" "+")
The cat does not eat the squirrel.
Unknown
inv-rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel does not visit the rabbit.
Unknown
inv-random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "-")
The squirrel visits the cat.
Unknown
random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "+")
@0: The cat sees the squirrel.[(triple1)] The cat visits the rabbit.[(triple2 OR ((triple7 triple6) -> rule4))] The rabbit eats the squirrel.[(triple3)] The rabbit is rough.[(triple4)] The rabbit sees the squirrel.[(triple5)] The squirrel eats the cat.[(triple6)] The squirrel sees the cat.[(triple7)] @1: The cat is young.[(((triple2) -> rule7) OR ((((triple7 triple6) -> rule4)) -> rule7))] The squirrel is not kind.[(((triple1 triple6) -> rule2))] @2: The cat is not nice.[(((((triple2) -> rule7)) -> rule1) OR ((((((triple7 triple6) -> rule4)) -> rule7)) -> rule1))]
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple2
((triple7 triple6) -> (rule4 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple4
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple5
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple6
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple7
The cat is young.
("cat" "is" "young" "+")
((triple2) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple7 triple6) -> (rule4 % int2))) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The squirrel is not kind.
("squirrel" "is" "kind" "-")
((triple1 triple6) -> (rule2 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1
The cat is not nice.
("cat" "is" "nice" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((((triple7 triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3