The bear chases the lion. The bear eats the lion. The bear is big. The bear is cold. The bear is green. The bear is nice. The bear is young. The bear likes the lion. The lion chases the bear. The lion eats the bear. The lion is big. The lion is cold. The lion is green. The lion is nice. The lion is young. The lion likes the bear. If something eats the bear then it chases the lion. If something chases the bear then it eats the bear. If the lion eats the bear and the bear chases the lion then the lion likes the bear. If something is nice then it chases the bear. If something eats the lion and the lion likes the bear then it is big. If something likes the bear and the bear is nice then the bear is cold.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear eats the lion.
("bear" "eats" "lion" "+")
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 is young.
("bear" "is" "young" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
If something eats the bear then it chases the lion.
((("something" "eats" "bear" "+")) -> ("something" "chases" "lion" "+"))
If something chases the bear then it eats the bear.
((("something" "chases" "bear" "+")) -> ("something" "eats" "bear" "+"))
If the lion eats the bear and the bear chases the lion then the lion likes the bear.
((("lion" "eats" "bear" "+") ("bear" "chases" "lion" "+")) -> ("lion" "likes" "bear" "+"))
If something is nice then it chases the bear.
((("something" "is" "nice" "+")) -> ("something" "chases" "bear" "+"))
If something eats the lion and the lion likes the bear then it is big.
((("something" "eats" "lion" "+") ("lion" "likes" "bear" "+")) -> ("something" "is" "big" "+"))
If something likes the bear and the bear is nice then the bear is cold.
((("something" "likes" "bear" "+") ("bear" "is" "nice" "+")) -> ("bear" "is" "cold" "+"))
The lion is big.
True
1
proof
[(triple11)]
("lion" "is" "big" "+")
triple11
The bear does not like the lion.
False
1
inv-proof
[(triple8)]
("bear" "likes" "lion" "-")
triple8
The lion chases the lion.
True
2
proof
[(((triple10) -> rule1) OR ((((triple9) -> rule2)) -> rule1) OR ((((((triple14) -> rule4)) -> rule2)) -> rule1))]
("lion" "chases" "lion" "+")
((triple10) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
((((((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
int3
The bear does not chase the bear.
False
2
inv-proof
[(((triple6) -> rule4))]
("bear" "chases" "bear" "-")
((triple6) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear eats the bear.
True
3
proof
[(((((triple6) -> rule4)) -> rule2))]
("bear" "eats" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear does not eat the bear.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule2))]
("bear" "eats" "bear" "-")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
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 lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The bear chases the lion.[(triple1 OR ((((((triple6) -> rule4)) -> rule2)) -> rule1))] The bear eats the lion.[(triple2)] The bear is big.[(triple3 OR ((triple2 triple16) -> rule5) OR ((triple2 ((triple10 triple1) -> rule3)) -> rule5) OR ((triple2 ((((triple9) -> rule2) triple1) -> rule3)) -> rule5) OR ((triple2 ((((((triple14) -> rule4)) -> rule2) triple1) -> rule3)) -> rule5) OR ((triple2 ((triple10 ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((triple9) -> rule2) ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((((triple14) -> rule4)) -> rule2) ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3)) -> rule5))] The bear is cold.[(triple4 OR ((triple16 triple6) -> rule6) OR ((((triple10 triple1) -> rule3) triple6) -> rule6) OR ((((((triple9) -> rule2) triple1) -> rule3) triple6) -> rule6) OR ((((((((triple14) -> rule4)) -> rule2) triple1) -> rule3) triple6) -> rule6) OR ((((triple10 ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3) triple6) -> rule6) OR ((((((triple9) -> rule2) ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3) triple6) -> rule6) OR ((((((((triple14) -> rule4)) -> rule2) ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3) triple6) -> rule6))] The bear is green.[(triple5)] The bear is nice.[(triple6)] The bear is young.[(triple7)] The bear likes the lion.[(triple8)] The lion chases the bear.[(triple9 OR ((triple14) -> rule4))] The lion eats the bear.[(triple10 OR ((triple9) -> rule2) OR ((((triple14) -> rule4)) -> rule2))] The lion is big.[(triple11)] The lion is cold.[(triple12)] The lion is green.[(triple13)] The lion is nice.[(triple14)] The lion is young.[(triple15)] The lion likes the bear.[(triple16 OR ((triple10 triple1) -> rule3) OR ((((triple9) -> rule2) triple1) -> rule3) OR ((((((triple14) -> rule4)) -> rule2) triple1) -> rule3) OR ((triple10 ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3) OR ((((triple9) -> rule2) ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3) OR ((((((triple14) -> rule4)) -> rule2) ((((((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule3))] @1: The bear chases the bear.[(((triple6) -> rule4))] The lion chases the lion.[(((triple10) -> rule1) OR ((((triple9) -> rule2)) -> rule1) OR ((((((triple14) -> rule4)) -> rule2)) -> rule1))] @2: The bear eats the bear.[(((((triple6) -> rule4)) -> rule2))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
((((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
The bear eats the lion.
("bear" "eats" "lion" "+")
triple2
The bear is big.
("bear" "is" "big" "+")
triple3
((triple2 triple16) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
((triple2 ((triple10 triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
((triple2 ((((triple9) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
((triple2 ((((((triple14) -> (rule4 % int4))) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion chases the bear.
("lion" "chases" "bear" "+")
int4
((triple2 ((triple10 ((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
((triple2 ((((triple9) -> (rule2 % int6)) ((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
The lion eats the bear.
("lion" "eats" "bear" "+")
int6
((triple2 ((((((triple14) -> (rule4 % int7))) -> (rule2 % int6)) ((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
The lion eats the bear.
("lion" "eats" "bear" "+")
int6
The lion chases the bear.
("lion" "chases" "bear" "+")
int7
The bear is cold.
("bear" "is" "cold" "+")
triple4
((triple16 triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((((triple10 triple1) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
((((((triple9) -> (rule2 % int3)) triple1) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
((((((((triple14) -> (rule4 % int4))) -> (rule2 % int3)) triple1) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion chases the bear.
("lion" "chases" "bear" "+")
int4
((((triple10 ((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
((((((triple9) -> (rule2 % int6)) ((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
The lion eats the bear.
("lion" "eats" "bear" "+")
int6
((((((((triple14) -> (rule4 % int7))) -> (rule2 % int6)) ((((((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear chases the lion.
("bear" "chases" "lion" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
int4
The bear chases the bear.
("bear" "chases" "bear" "+")
int5
The lion eats the bear.
("lion" "eats" "bear" "+")
int6
The lion chases the bear.
("lion" "chases" "bear" "+")
int7
The bear is green.
("bear" "is" "green" "+")
triple5
The bear is nice.
("bear" "is" "nice" "+")
triple6
The bear is young.
("bear" "is" "young" "+")
triple7
The bear likes the lion.
("bear" "likes" "lion" "+")
triple8
The lion chases the bear.
("lion" "chases" "bear" "+")
triple9
((triple14) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
triple10
((triple9) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
triple11
The lion is cold.
("lion" "is" "cold" "+")
triple12
The lion is green.
("lion" "is" "green" "+")
triple13
The lion is nice.
("lion" "is" "nice" "+")
triple14
The lion is young.
("lion" "is" "young" "+")
triple15
The lion likes the bear.
("lion" "likes" "bear" "+")
triple16
((triple10 triple1) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
((((triple9) -> (rule2 % int2)) triple1) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
((((((triple14) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
int3
((triple10 ((((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear chases the bear.
("bear" "chases" "bear" "+")
int4
((((triple9) -> (rule2 % int5)) ((((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear chases the bear.
("bear" "chases" "bear" "+")
int4
The lion eats the bear.
("lion" "eats" "bear" "+")
int5
((((((triple14) -> (rule4 % int6))) -> (rule2 % int5)) ((((((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
int3
The bear chases the bear.
("bear" "chases" "bear" "+")
int4
The lion eats the bear.
("lion" "eats" "bear" "+")
int5
The lion chases the bear.
("lion" "chases" "bear" "+")
int6
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple6) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple10) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
((((((triple14) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
int3
The bear eats the bear.
("bear" "eats" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2