The bear eats the tiger. The bear likes the tiger. The bear visits the tiger. The tiger eats the bear. The tiger is not blue. The tiger is not nice. The tiger is red. If something likes the tiger and it eats the bear then it is kind. If the bear eats the tiger then the tiger does not visit the bear. If the bear likes the tiger and the tiger does not visit the bear then the bear is red.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is red.
("tiger" "is" "red" "+")
If something likes the tiger and it eats the bear then it is kind.
((("something" "likes" "tiger" "+") ("something" "eats" "bear" "+")) -> ("something" "is" "kind" "+"))
If the bear eats the tiger then the tiger does not visit the bear.
((("bear" "eats" "tiger" "+")) -> ("tiger" "visits" "bear" "-"))
If the bear likes the tiger and the tiger does not visit the bear then the bear is red.
((("bear" "likes" "tiger" "+") ("tiger" "visits" "bear" "~")) -> ("bear" "is" "red" "+"))
The bear likes the tiger.
True
1
proof
[(triple2)]
("bear" "likes" "tiger" "+")
triple2
The tiger is blue.
False
1
inv-proof
[(triple5)]
("tiger" "is" "blue" "+")
triple5
The tiger does not visit the bear.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "visits" "bear" "-")
((triple1) -> (rule2 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The tiger visits the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "visits" "bear" "+")
((triple1) -> (rule2 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The bear is red.
True
4
proof
[(((triple2 ((triple1) -> rule2)) -> rule3))]
("bear" "is" "red" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int2
The bear is not red.
False
4
inv-proof
[(((triple2 ((triple1) -> rule2)) -> rule3))]
("bear" "is" "red" "-")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int2
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "kind" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "kind" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear eats the tiger.[(triple1)] The bear likes the tiger.[(triple2)] The bear visits the tiger.[(triple3)] The tiger eats the bear.[(triple4)] The tiger is not blue.[(triple5)] The tiger is not nice.[(triple6)] The tiger is red.[(triple7)] @1: The tiger does not visit the bear.[(((triple1) -> rule2))] @2: The bear is red.[(((triple2 ((triple1) -> rule2)) -> rule3))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple4
The tiger is not blue.
("tiger" "is" "blue" "-")
triple5
The tiger is not nice.
("tiger" "is" "nice" "-")
triple6
The tiger is red.
("tiger" "is" "red" "+")
triple7
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
((triple1) -> (rule2 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The bear is red.
("bear" "is" "red" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int2