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