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