The bear sees the squirrel. The cat is nice. The rabbit chases the cat. The squirrel sees the cat. If the cat sees the rabbit then the cat is kind. If something is nice and it sees the cat then it does not see the squirrel. If something is round then it does not see the bear. If something chases the rabbit then it is nice. If something is nice then it chases the rabbit. If something sees the rabbit and it does not eat the rabbit then it chases the rabbit. If the cat chases the rabbit then the cat does not see the squirrel. If something sees the squirrel then it is round.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat is nice.
("cat" "is" "nice" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If the cat sees the rabbit then the cat is kind.
((("cat" "sees" "rabbit" "+")) -> ("cat" "is" "kind" "+"))
If something is nice and it sees the cat then it does not see the squirrel.
((("something" "is" "nice" "+") ("something" "sees" "cat" "+")) -> ("something" "sees" "squirrel" "-"))
If something is round then it does not see the bear.
((("something" "is" "round" "+")) -> ("something" "sees" "bear" "-"))
If something chases the rabbit then it is nice.
((("something" "chases" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it chases the rabbit.
((("something" "is" "nice" "+")) -> ("something" "chases" "rabbit" "+"))
If something sees the rabbit and it does not eat the rabbit then it chases the rabbit.
((("something" "sees" "rabbit" "+") ("something" "eats" "rabbit" "~")) -> ("something" "chases" "rabbit" "+"))
If the cat chases the rabbit then the cat does not see the squirrel.
((("cat" "chases" "rabbit" "+")) -> ("cat" "sees" "squirrel" "-"))
If something sees the squirrel then it is round.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "round" "+"))
The cat is nice.
True
1
proof
[(triple2)]
("cat" "is" "nice" "+")
triple2
The rabbit does not chase the cat.
False
1
inv-proof
[(triple3)]
("rabbit" "chases" "cat" "-")
triple3
The cat chases the rabbit.
True
2
proof
[(((triple2) -> rule5))]
("cat" "chases" "rabbit" "+")
((triple2) -> (rule5 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The bear is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("bear" "is" "round" "-")
((triple1) -> (rule8 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The cat does not see the squirrel.
True
3
proof
[(((((triple2) -> rule5)) -> rule7))]
("cat" "sees" "squirrel" "-")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat sees the squirrel.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule7))]
("cat" "sees" "squirrel" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "round" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@3: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule6 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "round" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The bear does not eat the squirrel.
Unknown
inv-random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "-")
The bear chases the squirrel.
Unknown
random
[@0: The bear chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "squirrel" "+")
@0: The bear sees the squirrel.[(triple1)] The cat is nice.[(triple2)] The rabbit chases the cat.[(triple3)] The squirrel sees the cat.[(triple4)] @1: The bear is round.[(((triple1) -> rule8))] The cat chases the rabbit.[(((triple2) -> rule5))] @2: The bear does not see the bear.[(((((triple1) -> rule8)) -> rule3))] The cat does not see the squirrel.[(((((triple2) -> rule5)) -> rule7))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple3
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple4
The bear is round.
("bear" "is" "round" "+")
((triple1) -> (rule8 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple2) -> (rule5 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The bear does not see the bear.
("bear" "sees" "bear" "-")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The bear does not see the bear.
("bear" "sees" "bear" "-")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2