The bear chases the cat. The bear chases the mouse. The bear eats the mouse. The bear is nice. The bear needs the mouse. The cat chases the mouse. The cat eats the mouse. The cat is blue. The cat is not green. The cat needs the bear. The lion needs the cat. The mouse chases the bear. The mouse chases the lion. The mouse eats the lion. The mouse is big. The mouse is not cold. If someone is cold then they eat the cat. If someone needs the mouse and they are cold then the mouse chases the cat. If someone eats the bear and they need the lion then they chase the cat. If someone eats the lion then they eat the bear. If someone eats the bear then they do not need the mouse. If someone needs the lion then the lion does not eat the cat. If someone chases the bear and they do not need the mouse then they need the cat. If someone needs the mouse and the mouse does not need the cat then the mouse is blue.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat needs the bear.
("cat" "needs" "bear" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
If someone is cold then they eat the cat.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "cat" "+"))
If someone needs the mouse and they are cold then the mouse chases the cat.
((("someone" "needs" "mouse" "+") ("someone" "is" "cold" "+")) -> ("mouse" "chases" "cat" "+"))
If someone eats the bear and they need the lion then they chase the cat.
((("someone" "eats" "bear" "+") ("someone" "needs" "lion" "+")) -> ("someone" "chases" "cat" "+"))
If someone eats the lion then they eat the bear.
((("someone" "eats" "lion" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the bear then they do not need the mouse.
((("someone" "eats" "bear" "+")) -> ("someone" "needs" "mouse" "-"))
If someone needs the lion then the lion does not eat the cat.
((("someone" "needs" "lion" "+")) -> ("lion" "eats" "cat" "-"))
If someone chases the bear and they do not need the mouse then they need the cat.
((("someone" "chases" "bear" "+") ("someone" "needs" "mouse" "~")) -> ("someone" "needs" "cat" "+"))
If someone needs the mouse and the mouse does not need the cat then the mouse is blue.
((("someone" "needs" "mouse" "+") ("mouse" "needs" "cat" "~")) -> ("mouse" "is" "blue" "+"))
The cat eats the mouse.
True
1
proof
[(triple7)]
("cat" "eats" "mouse" "+")
triple7
The mouse does not eat the lion.
False
1
inv-proof
[(triple14)]
("mouse" "eats" "lion" "-")
triple14
The mouse eats the bear.
True
2
proof
[(((triple14) -> rule4))]
("mouse" "eats" "bear" "+")
((triple14) -> (rule4 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not eat the bear.
False
2
inv-proof
[(((triple14) -> rule4))]
("mouse" "eats" "bear" "-")
((triple14) -> (rule4 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not need the mouse.
True
3
proof
[(((((triple14) -> rule4)) -> rule5))]
("mouse" "needs" "mouse" "-")
((((triple14) -> (rule4 % int2))) -> (rule5 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The mouse needs the mouse.
False
3
inv-proof
[(((((triple14) -> rule4)) -> rule5))]
("mouse" "needs" "mouse" "+")
((((triple14) -> (rule4 % int2))) -> (rule5 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The mouse needs the cat.
True
5
proof
[(((triple12 ((((triple14) -> rule4)) -> rule5)) -> rule7))]
("mouse" "needs" "cat" "+")
((triple12 ((((triple14) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The mouse does not need the cat.
False
5
inv-proof
[(((triple12 ((((triple14) -> rule4)) -> rule5)) -> rule7))]
("mouse" "needs" "cat" "-")
((triple12 ((((triple14) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3
The lion does not eat the cat.
Unknown
inv-rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "cat" "-")
The mouse chases the cat.
Unknown
rconc
[@1: The mouse chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "cat" "+")
The lion does not chase the cat.
Unknown
inv-rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "cat" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "blue" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear chases the lion.
Unknown
random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the mouse.[(triple2)] The bear eats the mouse.[(triple3)] The bear is nice.[(triple4)] The bear needs the mouse.[(triple5)] The cat chases the mouse.[(triple6)] The cat eats the mouse.[(triple7)] The cat is blue.[(triple8)] The cat is not green.[(triple9)] The cat needs the bear.[(triple10)] The lion needs the cat.[(triple11)] The mouse chases the bear.[(triple12)] The mouse chases the lion.[(triple13)] The mouse eats the lion.[(triple14)] The mouse is big.[(triple15)] The mouse is not cold.[(triple16)] @1: The mouse eats the bear.[(((triple14) -> rule4))] @2: The mouse does not need the mouse.[(((((triple14) -> rule4)) -> rule5))] @3: The mouse needs the cat.[(((triple12 ((((triple14) -> rule4)) -> rule5)) -> rule7))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple2
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple5
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple6
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
triple8
The cat is not green.
("cat" "is" "green" "-")
triple9
The cat needs the bear.
("cat" "needs" "bear" "+")
triple10
The lion needs the cat.
("lion" "needs" "cat" "+")
triple11
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple12
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple13
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple14
The mouse is big.
("mouse" "is" "big" "+")
triple15
The mouse is not cold.
("mouse" "is" "cold" "-")
triple16
The mouse eats the bear.
("mouse" "eats" "bear" "+")
((triple14) -> (rule4 % int1))
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
((((triple14) -> (rule4 % int2))) -> (rule5 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int2
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple12 ((((triple14) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
int3