The bear eats the tiger. The bear is nice. The bear is red. The bear sees the tiger. The tiger is big. The tiger needs the bear. The tiger sees the bear. If something needs the bear then it eats the bear. If something eats the tiger and it sees the bear then the tiger is young. If something is big then it needs the tiger. If something eats the bear and the bear is nice then it eats the tiger. If something is nice and it needs the tiger then it eats the bear. If something eats the tiger and the tiger is big then the tiger needs the bear.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something needs the bear then it eats the bear.
((("something" "needs" "bear" "+")) -> ("something" "eats" "bear" "+"))
If something eats the tiger and it sees the bear then the tiger is young.
((("something" "eats" "tiger" "+") ("something" "sees" "bear" "+")) -> ("tiger" "is" "young" "+"))
If something is big then it needs the tiger.
((("something" "is" "big" "+")) -> ("something" "needs" "tiger" "+"))
If something eats the bear and the bear is nice then it eats the tiger.
((("something" "eats" "bear" "+") ("bear" "is" "nice" "+")) -> ("something" "eats" "tiger" "+"))
If something is nice and it needs the tiger then it eats the bear.
((("something" "is" "nice" "+") ("something" "needs" "tiger" "+")) -> ("something" "eats" "bear" "+"))
If something eats the tiger and the tiger is big then the tiger needs the bear.
((("something" "eats" "tiger" "+") ("tiger" "is" "big" "+")) -> ("tiger" "needs" "bear" "+"))
The tiger sees the bear.
True
1
proof
[(triple7)]
("tiger" "sees" "bear" "+")
triple7
The tiger does not need the bear.
False
1
inv-proof
[(triple6 OR ((triple1 triple5) -> rule6))]
("tiger" "needs" "bear" "-")
triple6
((triple1 triple5) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the tiger.
True
2
proof
[(((triple5) -> rule3))]
("tiger" "needs" "tiger" "+")
((triple5) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
False
2
inv-proof
[(((triple5) -> rule3))]
("tiger" "needs" "tiger" "-")
((triple5) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger eats the tiger.
True
4
proof
[(((((triple6) -> rule1) triple2) -> rule4) OR ((((((triple1 triple5) -> rule6)) -> rule1) triple2) -> rule4))]
("tiger" "eats" "tiger" "+")
((((triple6) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
((((((triple1 triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The tiger does not eat the tiger.
False
4
inv-proof
[(((((triple6) -> rule1) triple2) -> rule4) OR ((((((triple1 triple5) -> rule6)) -> rule1) triple2) -> rule4))]
("tiger" "eats" "tiger" "-")
((((triple6) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
((((((triple1 triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@2: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear needs the tiger.
Unknown
rconc
[@1: The bear needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
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 is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear eats the tiger.[(triple1)] The bear is nice.[(triple2)] The bear is red.[(triple3)] The bear sees the tiger.[(triple4)] The tiger is big.[(triple5)] The tiger needs the bear.[(triple6 OR ((triple1 triple5) -> rule6))] The tiger sees the bear.[(triple7)] @1: The tiger eats the bear.[(((triple6) -> rule1) OR ((((triple1 triple5) -> rule6)) -> rule1))] The tiger needs the tiger.[(((triple5) -> rule3))] @2: The tiger eats the tiger.[(((((triple6) -> rule1) triple2) -> rule4) OR ((((((triple1 triple5) -> rule6)) -> rule1) triple2) -> rule4))] @3: The tiger is young.[(((((((triple6) -> rule1) triple2) -> rule4) triple7) -> rule2) OR ((((((((triple1 triple5) -> rule6)) -> rule1) triple2) -> rule4) triple7) -> rule2))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple6
((triple1 triple5) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple7
The tiger eats the bear.
("tiger" "eats" "bear" "+")
((triple6) -> (rule1 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
((((triple1 triple5) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple5) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple6) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
((((((triple1 triple5) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
((((((triple6) -> (rule1 % int3)) triple2) -> (rule4 % int2)) triple7) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int3
((((((((triple1 triple5) -> (rule6 % int4))) -> (rule1 % int3)) triple2) -> (rule4 % int2)) triple7) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4