The bear is green. The cow is young. The tiger sees the cow. If someone is young then they see the tiger. If someone likes the bear then the bear likes the cow. If someone sees the tiger then the tiger is young. If someone is big and they like the cow then the cow does not like the bear. If someone sees the tiger then they do not like the cow. If someone likes the cow then the cow likes the tiger.
The bear is green.
("bear" "is" "green" "+")
The cow is young.
("cow" "is" "young" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If someone is young then they see the tiger.
((("someone" "is" "young" "+")) -> ("someone" "sees" "tiger" "+"))
If someone likes the bear then the bear likes the cow.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "cow" "+"))
If someone sees the tiger then the tiger is young.
((("someone" "sees" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If someone is big and they like the cow then the cow does not like the bear.
((("someone" "is" "big" "+") ("someone" "likes" "cow" "+")) -> ("cow" "likes" "bear" "-"))
If someone sees the tiger then they do not like the cow.
((("someone" "sees" "tiger" "+")) -> ("someone" "likes" "cow" "-"))
If someone likes the cow then the cow likes the tiger.
((("someone" "likes" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
The bear is green.
True
1
proof
[(triple1)]
("bear" "is" "green" "+")
triple1
The tiger does not see the cow.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "cow" "-")
triple3
The cow sees the tiger.
True
2
proof
[(((triple2) -> rule1))]
("cow" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "sees" "tiger" "-")
((triple2) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not like the cow.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("cow" "likes" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("tiger" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger sees the tiger.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule1))]
("tiger" "sees" "tiger" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int3
The tiger does not see the tiger.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule1))]
("tiger" "sees" "tiger" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int3
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "tiger" "-")
The cow likes the tiger.
Unknown
rconc
[@2: The cow likes the tiger.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cow" "likes" "tiger" "+")
The bear does not like the cow.
Unknown
inv-rconc
[@1: The bear likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "cow" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The cow does not eat the bear.
Unknown
inv-random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "-")
The cow eats the tiger.
Unknown
random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "+")
The tiger does not eat the bear.
Unknown
inv-random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The bear is green.[(triple1)] The cow is young.[(triple2)] The tiger sees the cow.[(triple3)] @1: The cow sees the tiger.[(((triple2) -> rule1))] @2: The cow does not like the cow.[(((((triple2) -> rule1)) -> rule5))] The tiger is young.[(((((triple2) -> rule1)) -> rule3))] @3: The tiger sees the tiger.[(((((((triple2) -> rule1)) -> rule3)) -> rule1))] @4: The tiger does not like the cow.[(((((((((triple2) -> rule1)) -> rule3)) -> rule1)) -> rule5))]
The bear is green.
("bear" "is" "green" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not like the cow.
("cow" "likes" "cow" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int3
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int4