The cat chases the squirrel. The cat eats the squirrel. The cat is kind. The cat is red. The cat is not round. The cat does not see the squirrel. The squirrel chases the cat. The squirrel eats the cat. The squirrel is big. The squirrel is rough. The squirrel is round. The squirrel sees the cat. If the cat is red then the cat is rough. If someone is red and they see the cat then they are not round. All round people are big. If someone is rough then they chase the cat. If the cat is round then the cat does not chase the squirrel. If the squirrel does not see the cat then the squirrel chases the cat. If the squirrel eats the cat then the cat does not see the squirrel. If the cat does not chase the squirrel then the cat sees the squirrel.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If the cat is red then the cat is rough.
((("cat" "is" "red" "+")) -> ("cat" "is" "rough" "+"))
If someone is red and they see the cat then they are not round.
((("someone" "is" "red" "+") ("someone" "sees" "cat" "+")) -> ("someone" "is" "round" "-"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is rough then they chase the cat.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "cat" "+"))
If the cat is round then the cat does not chase the squirrel.
((("cat" "is" "round" "+")) -> ("cat" "chases" "squirrel" "-"))
If the squirrel does not see the cat then the squirrel chases the cat.
((("squirrel" "sees" "cat" "~")) -> ("squirrel" "chases" "cat" "+"))
If the squirrel eats the cat then the cat does not see the squirrel.
((("squirrel" "eats" "cat" "+")) -> ("cat" "sees" "squirrel" "-"))
If the cat does not chase the squirrel then the cat sees the squirrel.
((("cat" "chases" "squirrel" "~")) -> ("cat" "sees" "squirrel" "+"))
The squirrel sees the cat.
True
1
proof
[(triple12)]
("squirrel" "sees" "cat" "+")
triple12
The cat is not kind.
False
1
inv-proof
[(triple3)]
("cat" "is" "kind" "-")
triple3
The cat is rough.
True
2
proof
[(((triple4) -> rule1))]
("cat" "is" "rough" "+")
((triple4) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple4) -> rule1))]
("cat" "is" "rough" "-")
((triple4) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat chases the cat.
True
3
proof
[(((((triple4) -> rule1)) -> rule4))]
("cat" "chases" "cat" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat does not chase the cat.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("cat" "chases" "cat" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "big" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The cat chases the squirrel.[(triple1)] The cat does not see the squirrel.[(triple6 OR ((triple8) -> rule7))] The cat eats the squirrel.[(triple2)] The cat is kind.[(triple3)] The cat is not round.[(triple5)] The cat is red.[(triple4)] The squirrel chases the cat.[(triple7 OR ((triple10) -> rule4))] The squirrel eats the cat.[(triple8)] The squirrel is big.[(triple9 OR ((triple11) -> rule3))] The squirrel is rough.[(triple10)] The squirrel is round.[(triple11)] The squirrel sees the cat.[(triple12)] @1: The cat is rough.[(((triple4) -> rule1))] @2: The cat chases the cat.[(((((triple4) -> rule1)) -> rule4))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
triple6
((triple8) -> (rule7 % int1))
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is not round.
("cat" "is" "round" "-")
triple5
The cat is red.
("cat" "is" "red" "+")
triple4
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple7
((triple10) -> (rule4 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
((triple11) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple12
The cat is rough.
("cat" "is" "rough" "+")
((triple4) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2