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