The cat needs the rabbit. The lion is nice. The rabbit needs the cat. If something needs the cat and it eats the cat then it sees the lion. If something needs the rabbit then the rabbit sees the cat. If something eats the lion then the lion is big. If something sees the rabbit and it is young then the rabbit needs the cat. If something needs the lion then the lion is blue. If the rabbit sees the cat then the cat needs the lion. If something eats the rabbit then the rabbit is big. If the lion needs the cat and the lion needs the rabbit then the lion is big.
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The lion is nice.
("lion" "is" "nice" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something needs the cat and it eats the cat then it sees the lion.
((("something" "needs" "cat" "+") ("something" "eats" "cat" "+")) -> ("something" "sees" "lion" "+"))
If something needs the rabbit then the rabbit sees the cat.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If something eats the lion then the lion is big.
((("something" "eats" "lion" "+")) -> ("lion" "is" "big" "+"))
If something sees the rabbit and it is young then the rabbit needs the cat.
((("something" "sees" "rabbit" "+") ("something" "is" "young" "+")) -> ("rabbit" "needs" "cat" "+"))
If something needs the lion then the lion is blue.
((("something" "needs" "lion" "+")) -> ("lion" "is" "blue" "+"))
If the rabbit sees the cat then the cat needs the lion.
((("rabbit" "sees" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If something eats the rabbit then the rabbit is big.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If the lion needs the cat and the lion needs the rabbit then the lion is big.
((("lion" "needs" "cat" "+") ("lion" "needs" "rabbit" "+")) -> ("lion" "is" "big" "+"))
The lion is nice.
True
1
proof
[(triple2)]
("lion" "is" "nice" "+")
triple2
The lion is not nice.
False
1
inv-proof
[(triple2)]
("lion" "is" "nice" "-")
triple2
The rabbit sees the cat.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "sees" "cat" "+")
((triple1) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit does not see the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "sees" "cat" "-")
((triple1) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The cat needs the lion.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "needs" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "needs" "lion" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The lion is blue.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule5))]
("lion" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The lion is not blue.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule5))]
("lion" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "big" "-")
The rabbit sees the lion.
Unknown
rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "lion" "+")
The cat does not see the lion.
Unknown
inv-rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "lion" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "big" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The lion does not need the rabbit.
Unknown
inv-random
[@0: The lion needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "rabbit" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cat needs the rabbit.[(triple1)] The lion is nice.[(triple2)] The rabbit needs the cat.[(triple3)] @1: The rabbit sees the cat.[(((triple1) -> rule2))] @2: The cat needs the lion.[(((((triple1) -> rule2)) -> rule6))] @3: The lion is blue.[(((((((triple1) -> rule2)) -> rule6)) -> rule5))]
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple1) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int3