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