The cat sees the rabbit. The rabbit eats the squirrel. The rabbit is big. The rabbit is kind. The rabbit is red. The rabbit sees the squirrel. The squirrel eats the rabbit. The squirrel is big. The squirrel is blue. The squirrel sees the rabbit. If something sees the cat and the cat eats the rabbit then it is rough. If the cat is red then the cat chases the squirrel. If something is red then it sees the cat. If something sees the cat and the cat is red then the cat sees the squirrel. If something sees the cat then it chases the squirrel. If something is blue and it chases the squirrel then the squirrel chases the cat. If something chases the rabbit and it eats the cat then the rabbit sees the squirrel. If something eats the rabbit and it eats the squirrel then it is big.
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something sees the cat and the cat eats the rabbit then it is rough.
((("something" "sees" "cat" "+") ("cat" "eats" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If the cat is red then the cat chases the squirrel.
((("cat" "is" "red" "+")) -> ("cat" "chases" "squirrel" "+"))
If something is red then it sees the cat.
((("something" "is" "red" "+")) -> ("something" "sees" "cat" "+"))
If something sees the cat and the cat is red then the cat sees the squirrel.
((("something" "sees" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "sees" "squirrel" "+"))
If something sees the cat then it chases the squirrel.
((("something" "sees" "cat" "+")) -> ("something" "chases" "squirrel" "+"))
If something is blue and it chases the squirrel then the squirrel chases the cat.
((("something" "is" "blue" "+") ("something" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cat" "+"))
If something chases the rabbit and it eats the cat then the rabbit sees the squirrel.
((("something" "chases" "rabbit" "+") ("something" "eats" "cat" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If something eats the rabbit and it eats the squirrel then it is big.
((("something" "eats" "rabbit" "+") ("something" "eats" "squirrel" "+")) -> ("something" "is" "big" "+"))
The rabbit is big.
True
1
proof
[(triple3)]
("rabbit" "is" "big" "+")
triple3
The squirrel is not blue.
False
1
inv-proof
[(triple9)]
("squirrel" "is" "blue" "-")
triple9
The rabbit sees the cat.
True
2
proof
[(((triple5) -> rule3))]
("rabbit" "sees" "cat" "+")
((triple5) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit does not see the cat.
False
2
inv-proof
[(((triple5) -> rule3))]
("rabbit" "sees" "cat" "-")
((triple5) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit chases the squirrel.
True
3
proof
[(((((triple5) -> rule3)) -> rule5))]
("rabbit" "chases" "squirrel" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit does not chase the squirrel.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule5))]
("rabbit" "chases" "squirrel" "-")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "rough" "+")
The cat does not chase the squirrel.
Unknown
inv-rconc
[@2: The cat chases the squirrel.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("cat" "chases" "squirrel" "-")
The cat eats the rabbit.
Unknown
random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The squirrel eats the cat.
Unknown
random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "+")
@0: The cat sees the rabbit.[(triple1)] The rabbit eats the squirrel.[(triple2)] The rabbit is big.[(triple3)] The rabbit is kind.[(triple4)] The rabbit is red.[(triple5)] The rabbit sees the squirrel.[(triple6)] The squirrel eats the rabbit.[(triple7)] The squirrel is big.[(triple8)] The squirrel is blue.[(triple9)] The squirrel sees the rabbit.[(triple10)] @1: The rabbit sees the cat.[(((triple5) -> rule3))] @2: The rabbit chases the squirrel.[(((((triple5) -> rule3)) -> rule5))]
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple6
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple10
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple5) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2