The cat chases the rabbit. The cow does not eat the tiger. The rabbit is not red. The tiger is green. If something chases the rabbit then it eats the cow. If something chases the rabbit then it is red. If something is red then it is big.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cow does not eat the tiger.
("cow" "eats" "tiger" "-")
The rabbit is not red.
("rabbit" "is" "red" "-")
The tiger is green.
("tiger" "is" "green" "+")
If something chases the rabbit then it eats the cow.
((("something" "chases" "rabbit" "+")) -> ("something" "eats" "cow" "+"))
If something chases the rabbit then it is red.
((("something" "chases" "rabbit" "+")) -> ("something" "is" "red" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
The rabbit is not red.
True
1
proof
[(triple3)]
("rabbit" "is" "red" "-")
triple3
The cow eats the tiger.
False
1
inv-proof
[(triple2)]
("cow" "eats" "tiger" "+")
triple2
The cat is red.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "red" "-")
((triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("cat" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("cat" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "cow" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "big" "+")
The cow is not big.
Unknown
inv-rconc
[@2: The cow is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cow" "is" "big" "-")
The cow visits the tiger.
Unknown
random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "+")
The cow does not chase the tiger.
Unknown
inv-random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cat chases the rabbit.[(triple1)] The cow does not eat the tiger.[(triple2)] The rabbit is not red.[(triple3)] The tiger is green.[(triple4)] @1: The cat eats the cow.[(((triple1) -> rule1))] The cat is red.[(((triple1) -> rule2))] @2: The cat is big.[(((((triple1) -> rule2)) -> rule3))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cow does not eat the tiger.
("cow" "eats" "tiger" "-")
triple2
The rabbit is not red.
("rabbit" "is" "red" "-")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The cat eats the cow.
("cat" "eats" "cow" "+")
((triple1) -> (rule1 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2