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