The cat visits the squirrel. The lion visits the squirrel. The squirrel visits the cat. If someone visits the lion then the lion is red. If someone is red then they eat the cat. If the squirrel visits the cat then the squirrel chases the cat. If the lion is rough and the lion does not eat the squirrel then the lion chases the squirrel. If someone visits the cat then the cat is young. If someone chases the cat then the cat is red.
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone visits the lion then the lion is red.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "red" "+"))
If someone is red then they eat the cat.
((("someone" "is" "red" "+")) -> ("someone" "eats" "cat" "+"))
If the squirrel visits the cat then the squirrel chases the cat.
((("squirrel" "visits" "cat" "+")) -> ("squirrel" "chases" "cat" "+"))
If the lion is rough and the lion does not eat the squirrel then the lion chases the squirrel.
((("lion" "is" "rough" "+") ("lion" "eats" "squirrel" "~")) -> ("lion" "chases" "squirrel" "+"))
If someone visits the cat then the cat is young.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "young" "+"))
If someone chases the cat then the cat is red.
((("someone" "chases" "cat" "+")) -> ("cat" "is" "red" "+"))
The cat visits the squirrel.
True
1
proof
[(triple1)]
("cat" "visits" "squirrel" "+")
triple1
The squirrel does not visit the cat.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "cat" "-")
triple3
The squirrel chases the cat.
True
2
proof
[(((triple3) -> rule3))]
("squirrel" "chases" "cat" "+")
((triple3) -> (rule3 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel does not chase the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "chases" "cat" "-")
((triple3) -> (rule3 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat is red.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("cat" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat is not red.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("cat" "is" "red" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat eats the cat.
True
4
proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("cat" "eats" "cat" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The cat does not eat the cat.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("cat" "eats" "cat" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "red" "-")
The lion eats the cat.
Unknown
rconc
[@2: The lion eats the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("lion" "eats" "cat" "+")
The lion does not chase the squirrel.
Unknown
inv-rconc
[@1: The lion chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "squirrel" "-")
The squirrel eats the cat.
Unknown
rconc
[@1: The squirrel eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "cat" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The squirrel does not visit the lion.
Unknown
inv-random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "-")
The cat chases the squirrel.
Unknown
random
[@0: The cat chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "squirrel" "+")
@0: The cat visits the squirrel.[(triple1)] The lion visits the squirrel.[(triple2)] The squirrel visits the cat.[(triple3)] @1: The cat is young.[(((triple3) -> rule5))] The squirrel chases the cat.[(((triple3) -> rule3))] @2: The cat is red.[(((((triple3) -> rule3)) -> rule6))] @3: The cat eats the cat.[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
((triple3) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((triple3) -> (rule3 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int3