The cat eats the tiger. The dog is not big. The lion likes the cat. The tiger is blue. If something eats the cat and the cat eats the dog then the cat is not nice. If something eats the cat and it does not like the dog then the cat eats the lion. If something eats the tiger then it sees the tiger. If something is blue then it eats the tiger. If something eats the dog and it likes the lion then it is blue. If something is cold and it sees the tiger then it is not blue. If something sees the tiger then it eats the cat. If something likes the dog and the dog sees the tiger then the dog likes the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The dog is not big.
("dog" "is" "big" "-")
The lion likes the cat.
("lion" "likes" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something eats the cat and the cat eats the dog then the cat is not nice.
((("something" "eats" "cat" "+") ("cat" "eats" "dog" "+")) -> ("cat" "is" "nice" "-"))
If something eats the cat and it does not like the dog then the cat eats the lion.
((("something" "eats" "cat" "+") ("something" "likes" "dog" "~")) -> ("cat" "eats" "lion" "+"))
If something eats the tiger then it sees the tiger.
((("something" "eats" "tiger" "+")) -> ("something" "sees" "tiger" "+"))
If something is blue then it eats the tiger.
((("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the dog and it likes the lion then it is blue.
((("something" "eats" "dog" "+") ("something" "likes" "lion" "+")) -> ("something" "is" "blue" "+"))
If something is cold and it sees the tiger then it is not blue.
((("something" "is" "cold" "+") ("something" "sees" "tiger" "+")) -> ("something" "is" "blue" "-"))
If something sees the tiger then it eats the cat.
((("something" "sees" "tiger" "+")) -> ("something" "eats" "cat" "+"))
If something likes the dog and the dog sees the tiger then the dog likes the tiger.
((("something" "likes" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("dog" "likes" "tiger" "+"))
The tiger is blue.
True
1
proof
[(triple4)]
("tiger" "is" "blue" "+")
triple4
The tiger is not blue.
False
1
inv-proof
[(triple4)]
("tiger" "is" "blue" "-")
triple4
The cat sees the tiger.
True
2
proof
[(((triple1) -> rule3))]
("cat" "sees" "tiger" "+")
((triple1) -> (rule3 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple4) -> rule4))]
("tiger" "eats" "tiger" "-")
((triple4) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cat eats the cat.
True
3
proof
[(((((triple1) -> rule3)) -> rule7))]
("cat" "eats" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("tiger" "sees" "tiger" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger eats the cat.
True
4
proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule7))]
("tiger" "eats" "cat" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The tiger does not eat the cat.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule3)) -> rule7))]
("tiger" "eats" "cat" "-")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The cat does not eat the lion.
Unknown
inv-rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "lion" "-")
The cat is blue.
Unknown
rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "blue" "+")
The lion does not see the tiger.
Unknown
inv-rconc
[@3: The lion sees the tiger.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- FAIL)]]
("lion" "sees" "tiger" "-")
The dog likes the tiger.
Unknown
rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "likes" "tiger" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The tiger likes the dog.
Unknown
random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "+")
The dog does not see the lion.
Unknown
inv-random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "lion" "-")
The dog eats the lion.
Unknown
random
[@0: The dog eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "lion" "+")
@0: The cat eats the tiger.[(triple1)] The dog is not big.[(triple2)] The lion likes the cat.[(triple3)] The tiger is blue.[(triple4)] @1: The cat sees the tiger.[(((triple1) -> rule3))] The tiger eats the tiger.[(((triple4) -> rule4))] @2: The cat eats the cat.[(((((triple1) -> rule3)) -> rule7))] The tiger sees the tiger.[(((((triple4) -> rule4)) -> rule3))] @3: The tiger eats the cat.[(((((((triple4) -> rule4)) -> rule3)) -> rule7))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The dog is not big.
("dog" "is" "big" "-")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((triple1) -> (rule3 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple4) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((((((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3