The bear eats the cat. The cat chases the rabbit. The rabbit chases the bear. If something chases the bear and the bear visits the cat then it visits the bear. If the rabbit chases the cat and the bear does not eat the rabbit then the cat eats the bear. If the cat is round then the cat is blue. If something chases the cat then the cat is round. If the rabbit chases the bear and the bear eats the cat then the bear chases the cat. If something is blue then it eats the bear.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If something chases the bear and the bear visits the cat then it visits the bear.
((("something" "chases" "bear" "+") ("bear" "visits" "cat" "+")) -> ("something" "visits" "bear" "+"))
If the rabbit chases the cat and the bear does not eat the rabbit then the cat eats the bear.
((("rabbit" "chases" "cat" "+") ("bear" "eats" "rabbit" "~")) -> ("cat" "eats" "bear" "+"))
If the cat is round then the cat is blue.
((("cat" "is" "round" "+")) -> ("cat" "is" "blue" "+"))
If something chases the cat then the cat is round.
((("something" "chases" "cat" "+")) -> ("cat" "is" "round" "+"))
If the rabbit chases the bear and the bear eats the cat then the bear chases the cat.
((("rabbit" "chases" "bear" "+") ("bear" "eats" "cat" "+")) -> ("bear" "chases" "cat" "+"))
If something is blue then it eats the bear.
((("something" "is" "blue" "+")) -> ("something" "eats" "bear" "+"))
The rabbit chases the bear.
True
1
proof
[(triple3)]
("rabbit" "chases" "bear" "+")
triple3
The bear does not eat the cat.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cat" "-")
triple1
The bear chases the cat.
True
3
proof
[(((triple3 triple1) -> rule5))]
("bear" "chases" "cat" "+")
((triple3 triple1) -> (rule5 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear does not chase the cat.
False
3
inv-proof
[(((triple3 triple1) -> rule5))]
("bear" "chases" "cat" "-")
((triple3 triple1) -> (rule5 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat is round.
True
4
proof
[(((((triple3 triple1) -> rule5)) -> rule4))]
("cat" "is" "round" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The cat is not round.
False
4
inv-proof
[(((((triple3 triple1) -> rule5)) -> rule4))]
("cat" "is" "round" "-")
((((triple3 triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The cat is blue.
True
5
proof
[(((((((triple3 triple1) -> rule5)) -> rule4)) -> rule3))]
("cat" "is" "blue" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
The cat is not blue.
False
5
inv-proof
[(((((((triple3 triple1) -> rule5)) -> rule4)) -> rule3))]
("cat" "is" "blue" "-")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "bear" "-")
The cat visits the bear.
Unknown
rconc
[@1: The cat visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "bear" "+")
The rabbit does not eat the bear.
Unknown
inv-rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "bear" "-")
The rabbit visits the bear.
Unknown
rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "bear" "+")
The bear does not chase the rabbit.
Unknown
inv-random
[@0: The bear chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "rabbit" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear eats the cat.[(triple1)] The cat chases the rabbit.[(triple2)] The rabbit chases the bear.[(triple3)] @1: The bear chases the cat.[(((triple3 triple1) -> rule5))] @2: The cat is round.[(((((triple3 triple1) -> rule5)) -> rule4))] @3: The cat is blue.[(((((((triple3 triple1) -> rule5)) -> rule4)) -> rule3))] @4: The cat eats the bear.[(((((((((triple3 triple1) -> rule5)) -> rule4)) -> rule3)) -> rule6))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple3
The bear chases the cat.
("bear" "chases" "cat" "+")
((triple3 triple1) -> (rule5 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
int3
The cat eats the bear.
("cat" "eats" "bear" "+")
((((((((triple3 triple1) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear chases the cat.
("bear" "chases" "cat" "+")
int4