The bear is young. The bear sees the cow. The bear sees the lion. The bear sees the mouse. The cow chases the bear. The cow is young. The cow needs the bear. The cow sees the bear. The cow sees the lion. The lion chases the cow. The lion chases the mouse. The lion sees the mouse. The mouse chases the cow. The mouse needs the cow. The mouse needs the lion. If something sees the lion then the lion sees the cow. If something is blue and it sees the bear then the bear chases the cow. If something needs the bear and it sees the mouse then the mouse chases the lion. If something sees the lion then the lion needs the bear. If something sees the bear and the bear sees the cow then the bear is young. If something chases the lion and the lion sees the cow then it is big.
The bear is young.
("bear" "is" "young" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If something sees the lion then the lion sees the cow.
((("something" "sees" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If something is blue and it sees the bear then the bear chases the cow.
((("something" "is" "blue" "+") ("something" "sees" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If something needs the bear and it sees the mouse then the mouse chases the lion.
((("something" "needs" "bear" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If something sees the lion then the lion needs the bear.
((("something" "sees" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something sees the bear and the bear sees the cow then the bear is young.
((("something" "sees" "bear" "+") ("bear" "sees" "cow" "+")) -> ("bear" "is" "young" "+"))
If something chases the lion and the lion sees the cow then it is big.
((("something" "chases" "lion" "+") ("lion" "sees" "cow" "+")) -> ("something" "is" "big" "+"))
The lion chases the cow.
True
1
proof
[(triple10)]
("lion" "chases" "cow" "+")
triple10
The mouse does not chase the cow.
False
1
inv-proof
[(triple13)]
("mouse" "chases" "cow" "-")
triple13
The lion needs the bear.
True
2
proof
[(((triple3) -> rule4) OR ((triple9) -> rule4))]
("lion" "needs" "bear" "+")
((triple3) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
((triple9) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion does not see the cow.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple9) -> rule1))]
("lion" "sees" "cow" "-")
((triple3) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
((triple9) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The mouse chases the lion.
True
4
proof
[(((((triple3) -> rule4) triple12) -> rule3) OR ((((triple9) -> rule4) triple12) -> rule3))]
("mouse" "chases" "lion" "+")
((((triple3) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
((((triple9) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The mouse does not chase the lion.
False
4
inv-proof
[(((((triple3) -> rule4) triple12) -> rule3) OR ((((triple9) -> rule4) triple12) -> rule3))]
("mouse" "chases" "lion" "-")
((((triple3) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
((((triple9) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The mouse is big.
True
7
proof
[(((((((triple3) -> rule4) triple12) -> rule3) ((triple3) -> rule1)) -> rule6) OR ((((((triple3) -> rule4) triple12) -> rule3) ((triple9) -> rule1)) -> rule6) OR ((((((triple9) -> rule4) triple12) -> rule3) ((triple3) -> rule1)) -> rule6) OR ((((((triple9) -> rule4) triple12) -> rule3) ((triple9) -> rule1)) -> rule6))]
("mouse" "is" "big" "+")
((((((triple3) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple3) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
The mouse is not big.
False
7
inv-proof
[(((((((triple3) -> rule4) triple12) -> rule3) ((triple3) -> rule1)) -> rule6) OR ((((((triple3) -> rule4) triple12) -> rule3) ((triple9) -> rule1)) -> rule6) OR ((((((triple9) -> rule4) triple12) -> rule3) ((triple3) -> rule1)) -> rule6) OR ((((((triple9) -> rule4) triple12) -> rule3) ((triple9) -> rule1)) -> rule6))]
("mouse" "is" "big" "-")
((((((triple3) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple3) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "big" "-")
The bear chases the cow.
Unknown
rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "cow" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "big" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "big" "+")
The bear does not need the lion.
Unknown
inv-random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow does not need the mouse.
Unknown
inv-random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear is young.[(triple1 OR ((triple8 triple2) -> rule5))] The bear sees the cow.[(triple2)] The bear sees the lion.[(triple3)] The bear sees the mouse.[(triple4)] The cow chases the bear.[(triple5)] The cow is young.[(triple6)] The cow needs the bear.[(triple7)] The cow sees the bear.[(triple8)] The cow sees the lion.[(triple9)] The lion chases the cow.[(triple10)] The lion chases the mouse.[(triple11)] The lion sees the mouse.[(triple12)] The mouse chases the cow.[(triple13)] The mouse needs the cow.[(triple14)] The mouse needs the lion.[(triple15)] @1: The lion needs the bear.[(((triple3) -> rule4) OR ((triple9) -> rule4))] The lion sees the cow.[(((triple3) -> rule1) OR ((triple9) -> rule1))] @2: The mouse chases the lion.[(((((triple3) -> rule4) triple12) -> rule3) OR ((((triple9) -> rule4) triple12) -> rule3))] @3: The mouse is big.[(((((((triple3) -> rule4) triple12) -> rule3) ((triple3) -> rule1)) -> rule6) OR ((((((triple3) -> rule4) triple12) -> rule3) ((triple9) -> rule1)) -> rule6) OR ((((((triple9) -> rule4) triple12) -> rule3) ((triple3) -> rule1)) -> rule6) OR ((((((triple9) -> rule4) triple12) -> rule3) ((triple9) -> rule1)) -> rule6))]
The bear is young.
("bear" "is" "young" "+")
triple1
((triple8 triple2) -> (rule5 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
triple2
The bear sees the lion.
("bear" "sees" "lion" "+")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The cow chases the bear.
("cow" "chases" "bear" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The cow sees the bear.
("cow" "sees" "bear" "+")
triple8
The cow sees the lion.
("cow" "sees" "lion" "+")
triple9
The lion chases the cow.
("lion" "chases" "cow" "+")
triple10
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple11
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple12
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple13
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple14
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple15
The lion needs the bear.
("lion" "needs" "bear" "+")
((triple3) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
((triple9) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple3) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
((triple9) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((((triple3) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
((((triple9) -> (rule4 % int2)) triple12) -> (rule3 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((((triple3) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple3) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
((((((triple9) -> (rule4 % int4)) triple12) -> (rule3 % int3)) ((triple9) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4