The bear eats the cat. The cat chases the rabbit. The rabbit chases the cat. If something chases the cat then the cat eats the bear. If something chases the bear then the bear is not blue. If something eats the bear then the bear does not need the rabbit.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
If something chases the cat then the cat eats the bear.
((("something" "chases" "cat" "+")) -> ("cat" "eats" "bear" "+"))
If something chases the bear then the bear is not blue.
((("something" "chases" "bear" "+")) -> ("bear" "is" "blue" "-"))
If something eats the bear then the bear does not need the rabbit.
((("something" "eats" "bear" "+")) -> ("bear" "needs" "rabbit" "-"))
The bear eats the cat.
True
1
proof
[(triple1)]
("bear" "eats" "cat" "+")
triple1
The bear does not eat the cat.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cat" "-")
triple1
The cat eats the bear.
True
2
proof
[(((triple3) -> rule1))]
("cat" "eats" "bear" "+")
((triple3) -> (rule1 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat does not eat the bear.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "eats" "bear" "-")
((triple3) -> (rule1 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The bear does not need the rabbit.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("bear" "needs" "rabbit" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The bear needs the rabbit.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("bear" "needs" "rabbit" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The bear eats the rabbit.
Unknown
random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "+")
@0: The bear eats the cat.[(triple1)] The cat chases the rabbit.[(triple2)] The rabbit chases the cat.[(triple3)] @1: The cat eats the bear.[(((triple3) -> rule1))] @2: The bear does not need the rabbit.[(((((triple3) -> rule1)) -> rule3))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple3
The cat eats the bear.
("cat" "eats" "bear" "+")
((triple3) -> (rule1 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear does not need the rabbit.
("bear" "needs" "rabbit" "-")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2