The bear likes the tiger. The cow needs the bear. The tiger sees the cow. If something is kind then it likes the bear. If something likes the tiger and it sees the cow then it is nice. If something needs the bear then it is kind. If something likes the bear then it is cold. If something is nice and it sees the bear then the bear needs the tiger. If the cow needs the bear then the cow is red.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something is kind then it likes the bear.
((("something" "is" "kind" "+")) -> ("something" "likes" "bear" "+"))
If something likes the tiger and it sees the cow then it is nice.
((("something" "likes" "tiger" "+") ("something" "sees" "cow" "+")) -> ("something" "is" "nice" "+"))
If something needs the bear then it is kind.
((("something" "needs" "bear" "+")) -> ("something" "is" "kind" "+"))
If something likes the bear then it is cold.
((("something" "likes" "bear" "+")) -> ("something" "is" "cold" "+"))
If something is nice and it sees the bear then the bear needs the tiger.
((("something" "is" "nice" "+") ("something" "sees" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If the cow needs the bear then the cow is red.
((("cow" "needs" "bear" "+")) -> ("cow" "is" "red" "+"))
The cow needs the bear.
True
1
proof
[(triple2)]
("cow" "needs" "bear" "+")
triple2
The bear does not like the tiger.
False
1
inv-proof
[(triple1)]
("bear" "likes" "tiger" "-")
triple1
The cow is red.
True
2
proof
[(((triple2) -> rule6))]
("cow" "is" "red" "+")
((triple2) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple2) -> rule6))]
("cow" "is" "red" "-")
((triple2) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the bear.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("cow" "likes" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow does not like the bear.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("cow" "likes" "bear" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The bear does not like the bear.
Unknown
inv-rconc
[@2: The bear likes the bear.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("bear" "likes" "bear" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "nice" "+")
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "nice" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The bear likes the tiger.[(triple1)] The cow needs the bear.[(triple2)] The tiger sees the cow.[(triple3)] @1: The cow is kind.[(((triple2) -> rule3))] The cow is red.[(((triple2) -> rule6))] @2: The cow likes the bear.[(((((triple2) -> rule3)) -> rule1))] @3: The cow is cold.[(((((((triple2) -> rule3)) -> rule1)) -> rule4))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The cow needs the bear.
("cow" "needs" "bear" "+")
triple2
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
((triple2) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((triple2) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3