The cat eats the rabbit. The cat is big. The cat is round. The rabbit eats the tiger. The rabbit is green. The rabbit is red. The rabbit needs the tiger. The rabbit visits the tiger. The tiger does not eat the cat. The tiger is round. If the cat is green and the cat is round then the cat does not need the rabbit. If the cat needs the rabbit then the cat does not visit the tiger. If someone visits the rabbit then they visit the cat. If someone is green then they visit the cat. If someone needs the rabbit and they eat the rabbit then the rabbit needs the tiger. If someone eats the cat then the cat eats the tiger. If someone visits the cat and they visit the rabbit then they eat the rabbit. If someone visits the cat then they visit the rabbit.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
The tiger is round.
("tiger" "is" "round" "+")
If the cat is green and the cat is round then the cat does not need the rabbit.
((("cat" "is" "green" "+") ("cat" "is" "round" "+")) -> ("cat" "needs" "rabbit" "-"))
If the cat needs the rabbit then the cat does not visit the tiger.
((("cat" "needs" "rabbit" "+")) -> ("cat" "visits" "tiger" "-"))
If someone visits the rabbit then they visit the cat.
((("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "cat" "+"))
If someone is green then they visit the cat.
((("someone" "is" "green" "+")) -> ("someone" "visits" "cat" "+"))
If someone needs the rabbit and they eat the rabbit then the rabbit needs the tiger.
((("someone" "needs" "rabbit" "+") ("someone" "eats" "rabbit" "+")) -> ("rabbit" "needs" "tiger" "+"))
If someone eats the cat then the cat eats the tiger.
((("someone" "eats" "cat" "+")) -> ("cat" "eats" "tiger" "+"))
If someone visits the cat and they visit the rabbit then they eat the rabbit.
((("someone" "visits" "cat" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone visits the cat then they visit the rabbit.
((("someone" "visits" "cat" "+")) -> ("someone" "visits" "rabbit" "+"))
The rabbit eats the tiger.
True
1
proof
[(triple4)]
("rabbit" "eats" "tiger" "+")
triple4
The cat does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "eats" "rabbit" "-")
triple1
The rabbit visits the cat.
True
2
proof
[(((triple5) -> rule4))]
("rabbit" "visits" "cat" "+")
((triple5) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit does not visit the cat.
False
2
inv-proof
[(((triple5) -> rule4))]
("rabbit" "visits" "cat" "-")
((triple5) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit visits the rabbit.
True
3
proof
[(((((triple5) -> rule4)) -> rule8))]
("rabbit" "visits" "rabbit" "+")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule8))]
("rabbit" "visits" "rabbit" "-")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit eats the rabbit.
True
6
proof
[(((((triple5) -> rule4) ((((triple5) -> rule4)) -> rule8)) -> rule7))]
("rabbit" "eats" "rabbit" "+")
((((triple5) -> (rule4 % int3)) ((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3
The rabbit does not eat the rabbit.
False
6
inv-proof
[(((((triple5) -> rule4) ((((triple5) -> rule4)) -> rule8)) -> rule7))]
("rabbit" "eats" "rabbit" "-")
((((triple5) -> (rule4 % int3)) ((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3
The tiger does not visit the rabbit.
Unknown
inv-rconc
[@2: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("tiger" "visits" "rabbit" "-")
The cat eats the tiger.
Unknown
rconc
[@1: The cat eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "eats" "tiger" "+")
The tiger does not visit the cat.
Unknown
inv-rconc
[@3: The tiger visits the cat.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule4 <- FAIL)]]
("tiger" "visits" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@3: The cat visits the cat.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule4 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit needs the cat.
Unknown
random
[@0: The rabbit needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cat is big.[(triple2)] The cat is round.[(triple3)] The rabbit eats the tiger.[(triple4)] The rabbit is green.[(triple5)] The rabbit is red.[(triple6)] The rabbit needs the tiger.[(triple7)] The rabbit visits the tiger.[(triple8)] The tiger does not eat the cat.[(triple9)] The tiger is round.[(triple10)] @1: The rabbit visits the cat.[(((triple5) -> rule4))] @2: The rabbit visits the rabbit.[(((((triple5) -> rule4)) -> rule8))] @3: The rabbit eats the rabbit.[(((((triple5) -> rule4) ((((triple5) -> rule4)) -> rule8)) -> rule7))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple4
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple7
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple8
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple5) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple5) -> (rule4 % int3)) ((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int3