The bear is green. The bear is young. The bear likes the tiger. The tiger eats the bear. The tiger is cold. The tiger is green. The tiger is nice. The tiger is young. The tiger likes the bear. The tiger sees the bear. If the tiger likes the bear and the bear is young then the tiger is cold. If someone is cold and young then they eat the tiger. If the bear sees the tiger then the bear eats the tiger. If someone eats the tiger and they eat the bear then they are round. If someone eats the bear then the bear likes the tiger. If someone is round then they like the tiger.
The bear is green.
("bear" "is" "green" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If the tiger likes the bear and the bear is young then the tiger is cold.
((("tiger" "likes" "bear" "+") ("bear" "is" "young" "+")) -> ("tiger" "is" "cold" "+"))
If someone is cold and young then they eat the tiger.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "eats" "tiger" "+"))
If the bear sees the tiger then the bear eats the tiger.
((("bear" "sees" "tiger" "+")) -> ("bear" "eats" "tiger" "+"))
If someone eats the tiger and they eat the bear then they are round.
((("someone" "eats" "tiger" "+") ("someone" "eats" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone eats the bear then the bear likes the tiger.
((("someone" "eats" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
If someone is round then they like the tiger.
((("someone" "is" "round" "+")) -> ("someone" "likes" "tiger" "+"))
The tiger is young.
True
1
proof
[(triple8)]
("tiger" "is" "young" "+")
triple8
The bear is not green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The tiger eats the tiger.
True
3
proof
[(((triple5 triple8) -> rule2) OR ((((triple9 triple2) -> rule1) triple8) -> rule2))]
("tiger" "eats" "tiger" "+")
((triple5 triple8) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
((((triple9 triple2) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger does not eat the tiger.
False
3
inv-proof
[(((triple5 triple8) -> rule2) OR ((((triple9 triple2) -> rule1) triple8) -> rule2))]
("tiger" "eats" "tiger" "-")
((triple5 triple8) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
((((triple9 triple2) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is round.
True
5
proof
[(((((triple5 triple8) -> rule2) triple4) -> rule4) OR ((((((triple9 triple2) -> rule1) triple8) -> rule2) triple4) -> rule4))]
("tiger" "is" "round" "+")
((((triple5 triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((((triple9 triple2) -> (rule1 % int3)) triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger is not round.
False
5
inv-proof
[(((((triple5 triple8) -> rule2) triple4) -> rule4) OR ((((((triple9 triple2) -> rule1) triple8) -> rule2) triple4) -> rule4))]
("tiger" "is" "round" "-")
((((triple5 triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((((triple9 triple2) -> (rule1 % int3)) triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger likes the tiger.
True
6
proof
[(((((((triple5 triple8) -> rule2) triple4) -> rule4)) -> rule6) OR ((((((((triple9 triple2) -> rule1) triple8) -> rule2) triple4) -> rule4)) -> rule6))]
("tiger" "likes" "tiger" "+")
((((((triple5 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((((triple9 triple2) -> (rule1 % int4)) triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The tiger does not like the tiger.
False
6
inv-proof
[(((((((triple5 triple8) -> rule2) triple4) -> rule4)) -> rule6) OR ((((((((triple9 triple2) -> rule1) triple8) -> rule2) triple4) -> rule4)) -> rule6))]
("tiger" "likes" "tiger" "-")
((((((triple5 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((((triple9 triple2) -> (rule1 % int4)) triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "tiger" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "round" "+")
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 sees the tiger.
Unknown
random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is green.[(triple1)] The bear is young.[(triple2)] The bear likes the tiger.[(triple3 OR ((triple4) -> rule5))] The tiger eats the bear.[(triple4)] The tiger is cold.[(triple5 OR ((triple9 triple2) -> rule1))] The tiger is green.[(triple6)] The tiger is nice.[(triple7)] The tiger is young.[(triple8)] The tiger likes the bear.[(triple9)] The tiger sees the bear.[(triple10)] @1: The tiger eats the tiger.[(((triple5 triple8) -> rule2) OR ((((triple9 triple2) -> rule1) triple8) -> rule2))] @2: The tiger is round.[(((((triple5 triple8) -> rule2) triple4) -> rule4) OR ((((((triple9 triple2) -> rule1) triple8) -> rule2) triple4) -> rule4))] @3: The tiger likes the tiger.[(((((((triple5 triple8) -> rule2) triple4) -> rule4)) -> rule6) OR ((((((((triple9 triple2) -> rule1) triple8) -> rule2) triple4) -> rule4)) -> rule6))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple3
((triple4) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
((triple9 triple2) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple9
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple10
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple5 triple8) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
((((triple9 triple2) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((triple5 triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((((triple9 triple2) -> (rule1 % int3)) triple8) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple5 triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
((((((((triple9 triple2) -> (rule1 % int4)) triple8) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4