The bear chases the cat. The cat chases the bear. The cat eats the bear. The cat needs the bear. The lion chases the mouse. The lion eats the cat. The mouse chases the lion. The mouse is green. The mouse needs the bear. The mouse needs the lion. If someone is young then they eat the lion. If the bear eats the mouse then the mouse chases the cat. If someone is young and they need the cat then they eat the lion. If someone eats the lion then the lion needs the bear. If someone needs the bear and the bear is big then they chase the bear. If someone chases the lion then they are young.
The bear chases the cat.
("bear" "chases" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If someone is young then they eat the lion.
((("someone" "is" "young" "+")) -> ("someone" "eats" "lion" "+"))
If the bear eats the mouse then the mouse chases the cat.
((("bear" "eats" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
If someone is young and they need the cat then they eat the lion.
((("someone" "is" "young" "+") ("someone" "needs" "cat" "+")) -> ("someone" "eats" "lion" "+"))
If someone eats the lion then the lion needs the bear.
((("someone" "eats" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If someone needs the bear and the bear is big then they chase the bear.
((("someone" "needs" "bear" "+") ("bear" "is" "big" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the lion then they are young.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "young" "+"))
The lion eats the cat.
True
1
proof
[(triple6)]
("lion" "eats" "cat" "+")
triple6
The lion does not chase the mouse.
False
1
inv-proof
[(triple5)]
("lion" "chases" "mouse" "-")
triple5
The mouse is young.
True
2
proof
[(((triple7) -> rule6))]
("mouse" "is" "young" "+")
((triple7) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple7) -> rule6))]
("mouse" "is" "young" "-")
((triple7) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the lion.
True
3
proof
[(((((triple7) -> rule6)) -> rule1))]
("mouse" "eats" "lion" "+")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not eat the lion.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule1))]
("mouse" "eats" "lion" "-")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The lion needs the bear.
True
4
proof
[(((((((triple7) -> rule6)) -> rule1)) -> rule4))]
("lion" "needs" "bear" "+")
((((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The lion does not need the bear.
False
4
inv-proof
[(((((((triple7) -> rule6)) -> rule1)) -> rule4))]
("lion" "needs" "bear" "-")
((((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "young" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear does not eat the lion.
Unknown
inv-rconc
[@2: The bear eats the lion.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("bear" "eats" "lion" "-")
The lion chases the bear.
Unknown
rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "bear" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear needs the cat.
Unknown
random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The bear chases the lion.
Unknown
random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "+")
@0: The bear chases the cat.[(triple1)] The cat chases the bear.[(triple2)] The cat eats the bear.[(triple3)] The cat needs the bear.[(triple4)] The lion chases the mouse.[(triple5)] The lion eats the cat.[(triple6)] The mouse chases the lion.[(triple7)] The mouse is green.[(triple8)] The mouse needs the bear.[(triple9)] The mouse needs the lion.[(triple10)] @1: The mouse is young.[(((triple7) -> rule6))] @2: The mouse eats the lion.[(((((triple7) -> rule6)) -> rule1))] @3: The lion needs the bear.[(((((((triple7) -> rule6)) -> rule1)) -> rule4))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The cat needs the bear.
("cat" "needs" "bear" "+")
triple4
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple5
The lion eats the cat.
("lion" "eats" "cat" "+")
triple6
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple9
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple10
The mouse is young.
("mouse" "is" "young" "+")
((triple7) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
((((((triple7) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3