The cat is young. The squirrel eats the cat. The squirrel is young. If something is nice then it chases the cat. If something is young and it eats the cat then the cat is round. If something is round then it likes the squirrel.
The cat is young.
("cat" "is" "young" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something is nice then it chases the cat.
((("something" "is" "nice" "+")) -> ("something" "chases" "cat" "+"))
If something is young and it eats the cat then the cat is round.
((("something" "is" "young" "+") ("something" "eats" "cat" "+")) -> ("cat" "is" "round" "+"))
If something is round then it likes the squirrel.
((("something" "is" "round" "+")) -> ("something" "likes" "squirrel" "+"))
The squirrel eats the cat.
True
1
proof
[(triple2)]
("squirrel" "eats" "cat" "+")
triple2
The cat is not young.
False
1
inv-proof
[(triple1)]
("cat" "is" "young" "-")
triple1
The cat is round.
True
3
proof
[(((triple3 triple2) -> rule2))]
("cat" "is" "round" "+")
((triple3 triple2) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
3
inv-proof
[(((triple3 triple2) -> rule2))]
("cat" "is" "round" "-")
((triple3 triple2) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the squirrel.
True
4
proof
[(((((triple3 triple2) -> rule2)) -> rule3))]
("cat" "likes" "squirrel" "+")
((((triple3 triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not like the squirrel.
False
4
inv-proof
[(((((triple3 triple2) -> rule2)) -> rule3))]
("cat" "likes" "squirrel" "-")
((((triple3 triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "-")
The squirrel chases the cat.
Unknown
rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "cat" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is young.[(triple1)] The squirrel eats the cat.[(triple2)] The squirrel is young.[(triple3)] @1: The cat is round.[(((triple3 triple2) -> rule2))] @2: The cat likes the squirrel.[(((((triple3 triple2) -> rule2)) -> rule3))]
The cat is young.
("cat" "is" "young" "+")
triple1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
((triple3 triple2) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((((triple3 triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2