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