The bear is cold. The cat is red. The cow needs the bear. The cow visits the bear. The cow visits the cat. The tiger is green. The tiger likes the cat. If the cow likes the cat then the cat likes the bear. If someone is cold then they need the tiger. If someone likes the bear then the bear needs the cow. If someone needs the tiger then the tiger likes the bear. If someone likes the tiger and they visit the cow then they need the cat. If someone is red and green then they visit the bear.
The bear is cold.
("bear" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If the cow likes the cat then the cat likes the bear.
((("cow" "likes" "cat" "+")) -> ("cat" "likes" "bear" "+"))
If someone is cold then they need the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "tiger" "+"))
If someone likes the bear then the bear needs the cow.
((("someone" "likes" "bear" "+")) -> ("bear" "needs" "cow" "+"))
If someone needs the tiger then the tiger likes the bear.
((("someone" "needs" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
If someone likes the tiger and they visit the cow then they need the cat.
((("someone" "likes" "tiger" "+") ("someone" "visits" "cow" "+")) -> ("someone" "needs" "cat" "+"))
If someone is red and green then they visit the bear.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "visits" "bear" "+"))
The cat is red.
True
1
proof
[(triple2)]
("cat" "is" "red" "+")
triple2
The tiger is not green.
False
1
inv-proof
[(triple6)]
("tiger" "is" "green" "-")
triple6
The bear needs the tiger.
True
2
proof
[(((triple1) -> rule2))]
("bear" "needs" "tiger" "+")
((triple1) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "needs" "tiger" "-")
((triple1) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger likes the bear.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("tiger" "likes" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger does not like the bear.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("tiger" "likes" "bear" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the cow.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule3))]
("bear" "needs" "cow" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The bear does not need the cow.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule3))]
("bear" "needs" "cow" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The cat does not like the bear.
Unknown
inv-rconc
[@1: The cat likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "bear" "-")
The cow needs the tiger.
Unknown
rconc
[@1: The cow needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "tiger" "+")
The cat does not visit the bear.
Unknown
inv-rconc
[@1: The cat visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "bear" "-")
The tiger visits the bear.
Unknown
rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "bear" "+")
The cow does not like the bear.
Unknown
inv-random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The cat does not need the bear.
Unknown
inv-random
[@0: The cat needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear is cold.[(triple1)] The cat is red.[(triple2)] The cow needs the bear.[(triple3)] The cow visits the bear.[(triple4)] The cow visits the cat.[(triple5)] The tiger is green.[(triple6)] The tiger likes the cat.[(triple7)] @1: The bear needs the tiger.[(((triple1) -> rule2))] @2: The tiger likes the bear.[(((((triple1) -> rule2)) -> rule4))] @3: The bear needs the cow.[(((((((triple1) -> rule2)) -> rule4)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cow needs the bear.
("cow" "needs" "bear" "+")
triple3
The cow visits the bear.
("cow" "visits" "bear" "+")
triple4
The cow visits the cat.
("cow" "visits" "cat" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple1) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3