The cat is red. The lion eats the tiger. The tiger is red. If something is blue then it eats the tiger. If something eats the lion then the lion eats the cat. If the cat chases the tiger and the tiger eats the cat then the cat is blue. If something is red then it eats the lion. If something is round and it eats the tiger then it needs the lion. If something eats the cat then the cat eats the tiger.
The cat is red.
("cat" "is" "red" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something is blue then it eats the tiger.
((("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the lion then the lion eats the cat.
((("something" "eats" "lion" "+")) -> ("lion" "eats" "cat" "+"))
If the cat chases the tiger and the tiger eats the cat then the cat is blue.
((("cat" "chases" "tiger" "+") ("tiger" "eats" "cat" "+")) -> ("cat" "is" "blue" "+"))
If something is red then it eats the lion.
((("something" "is" "red" "+")) -> ("something" "eats" "lion" "+"))
If something is round and it eats the tiger then it needs the lion.
((("something" "is" "round" "+") ("something" "eats" "tiger" "+")) -> ("something" "needs" "lion" "+"))
If something eats the cat then the cat eats the tiger.
((("something" "eats" "cat" "+")) -> ("cat" "eats" "tiger" "+"))
The cat is red.
True
1
proof
[(triple1)]
("cat" "is" "red" "+")
triple1
The tiger is not red.
False
1
inv-proof
[(triple3)]
("tiger" "is" "red" "-")
triple3
The tiger eats the lion.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "eats" "lion" "+")
((triple3) -> (rule4 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger does not eat the lion.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "eats" "lion" "-")
((triple3) -> (rule4 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion eats the cat.
True
3
proof
[(((((triple1) -> rule4)) -> rule2) OR ((((triple3) -> rule4)) -> rule2))]
("lion" "eats" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion does not eat the cat.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2) OR ((((triple3) -> rule4)) -> rule2))]
("lion" "eats" "cat" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The cat eats the tiger.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6) OR ((((((triple3) -> rule4)) -> rule2)) -> rule6))]
("cat" "eats" "tiger" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int3
The cat does not eat the tiger.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6) OR ((((((triple3) -> rule4)) -> rule2)) -> rule6))]
("cat" "eats" "tiger" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int3
The tiger does not need the lion.
Unknown
inv-rconc
[@1: The tiger needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "lion" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "lion" "+")
The cat does not need the lion.
Unknown
inv-rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "lion" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
@0: The cat is red.[(triple1)] The lion eats the tiger.[(triple2)] The tiger is red.[(triple3)] @1: The cat eats the lion.[(((triple1) -> rule4))] The tiger eats the lion.[(((triple3) -> rule4))] @2: The lion eats the cat.[(((((triple1) -> rule4)) -> rule2) OR ((((triple3) -> rule4)) -> rule2))] @3: The cat eats the tiger.[(((((((triple1) -> rule4)) -> rule2)) -> rule6) OR ((((((triple3) -> rule4)) -> rule2)) -> rule6))]
The cat is red.
("cat" "is" "red" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The tiger is red.
("tiger" "is" "red" "+")
triple3
The cat eats the lion.
("cat" "eats" "lion" "+")
((triple1) -> (rule4 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((triple3) -> (rule4 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The cat eats the tiger.
("cat" "eats" "tiger" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int3