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