The bear is rough. The tiger eats the bear. If someone sees the bear then they do not eat the tiger. All kind people are not rough. If someone eats the tiger and they are not cold then they are not rough. If the bear is rough then the bear likes the tiger. If someone eats the bear then the bear likes the tiger. Kind people are nice. If someone is nice and blue then they see the bear. If the bear likes the tiger and the tiger eats the bear then the tiger sees the bear.
The bear is rough.
("bear" "is" "rough" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
If someone sees the bear then they do not eat the tiger.
((("someone" "sees" "bear" "+")) -> ("someone" "eats" "tiger" "-"))
All kind people are not rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "-"))
If someone eats the tiger and they are not cold then they are not rough.
((("someone" "eats" "tiger" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "-"))
If the bear is rough then the bear likes the tiger.
((("bear" "is" "rough" "+")) -> ("bear" "likes" "tiger" "+"))
If someone eats the bear then the bear likes the tiger.
((("someone" "eats" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and blue then they see the bear.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "sees" "bear" "+"))
If the bear likes the tiger and the tiger eats the bear then the tiger sees the bear.
((("bear" "likes" "tiger" "+") ("tiger" "eats" "bear" "+")) -> ("tiger" "sees" "bear" "+"))
The bear is rough.
True
1
proof
[(triple1)]
("bear" "is" "rough" "+")
triple1
The tiger does not eat the bear.
False
1
inv-proof
[(triple2)]
("tiger" "eats" "bear" "-")
triple2
The bear likes the tiger.
True
2
proof
[(((triple1) -> rule4) OR ((triple2) -> rule5))]
("bear" "likes" "tiger" "+")
((triple1) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
((triple2) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear does not like the tiger.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple2) -> rule5))]
("bear" "likes" "tiger" "-")
((triple1) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
((triple2) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The tiger sees the bear.
True
4
proof
[(((((triple1) -> rule4) triple2) -> rule8) OR ((((triple2) -> rule5) triple2) -> rule8))]
("tiger" "sees" "bear" "+")
((((triple1) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger does not see the bear.
False
4
inv-proof
[(((((triple1) -> rule4) triple2) -> rule8) OR ((((triple2) -> rule5) triple2) -> rule8))]
("tiger" "sees" "bear" "-")
((((triple1) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger does not eat the tiger.
True
5
proof
[(((((((triple1) -> rule4) triple2) -> rule8)) -> rule1) OR ((((((triple2) -> rule5) triple2) -> rule8)) -> rule1))]
("tiger" "eats" "tiger" "-")
((((((triple1) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The tiger eats the tiger.
False
5
inv-proof
[(((((((triple1) -> rule4) triple2) -> rule8)) -> rule1) OR ((((((triple2) -> rule5) triple2) -> rule8)) -> rule1))]
("tiger" "eats" "tiger" "+")
((((((triple1) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "nice" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "nice" "+")
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "sees" "bear" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The bear does not see the tiger.
Unknown
inv-random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The bear is rough.[(triple1)] The tiger eats the bear.[(triple2)] @1: The bear likes the tiger.[(((triple1) -> rule4) OR ((triple2) -> rule5))] @2: The tiger sees the bear.[(((((triple1) -> rule4) triple2) -> rule8) OR ((((triple2) -> rule5) triple2) -> rule8))] @3: The tiger does not eat the tiger.[(((((((triple1) -> rule4) triple2) -> rule8)) -> rule1) OR ((((((triple2) -> rule5) triple2) -> rule8)) -> rule1))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple1) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
((triple2) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
((((triple1) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule8 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
((((((triple1) -> (rule4 % int3)) triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
((((((triple2) -> (rule5 % int3)) triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3