The bear is cold. The bear sees the lion. The bear sees the mouse. The cat chases the mouse. The cat is big. The cat is kind. The cat likes the bear. The cat sees the lion. The lion chases the cat. The lion is kind. The lion likes the bear. The lion likes the mouse. The lion sees the bear. The lion sees the cat. The lion sees the mouse. The mouse sees the cat. If something sees the lion and it sees the cat then the cat chases the mouse. If something sees the cat then it is big. If something sees the bear then it chases the cat. If something sees the cat and it is nice then it chases the bear. If something likes the cat then it is nice. If the bear sees the cat and the cat chases the mouse then the cat chases the lion. If something is kind then it likes the lion. If something is kind then it likes the cat.
The bear is cold.
("bear" "is" "cold" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something sees the lion and it sees the cat then the cat chases the mouse.
((("something" "sees" "lion" "+") ("something" "sees" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If something sees the cat then it is big.
((("something" "sees" "cat" "+")) -> ("something" "is" "big" "+"))
If something sees the bear then it chases the cat.
((("something" "sees" "bear" "+")) -> ("something" "chases" "cat" "+"))
If something sees the cat and it is nice then it chases the bear.
((("something" "sees" "cat" "+") ("something" "is" "nice" "+")) -> ("something" "chases" "bear" "+"))
If something likes the cat then it is nice.
((("something" "likes" "cat" "+")) -> ("something" "is" "nice" "+"))
If the bear sees the cat and the cat chases the mouse then the cat chases the lion.
((("bear" "sees" "cat" "+") ("cat" "chases" "mouse" "+")) -> ("cat" "chases" "lion" "+"))
If something is kind then it likes the lion.
((("something" "is" "kind" "+")) -> ("something" "likes" "lion" "+"))
If something is kind then it likes the cat.
((("something" "is" "kind" "+")) -> ("something" "likes" "cat" "+"))
The lion sees the cat.
True
1
proof
[(triple14)]
("lion" "sees" "cat" "+")
triple14
The lion does not like the mouse.
False
1
inv-proof
[(triple12)]
("lion" "likes" "mouse" "-")
triple12
The cat likes the lion.
True
2
proof
[(((triple6) -> rule7))]
("cat" "likes" "lion" "+")
((triple6) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple6) -> rule8))]
("cat" "likes" "cat" "-")
((triple6) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion is nice.
True
3
proof
[(((((triple10) -> rule8)) -> rule5))]
("lion" "is" "nice" "+")
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion is not nice.
False
3
inv-proof
[(((((triple10) -> rule8)) -> rule5))]
("lion" "is" "nice" "-")
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion chases the bear.
True
5
proof
[(((triple14 ((((triple10) -> rule8)) -> rule5)) -> rule4))]
("lion" "chases" "bear" "+")
((triple14 ((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion likes the cat.
("lion" "likes" "cat" "+")
int3
The lion does not chase the bear.
False
5
inv-proof
[(((triple14 ((((triple10) -> rule8)) -> rule5)) -> rule4))]
("lion" "chases" "bear" "-")
((triple14 ((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion likes the cat.
("lion" "likes" "cat" "+")
int3
The bear does not like the lion.
Unknown
inv-rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "lion" "-")
The mouse is nice.
Unknown
rconc
[@2: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("mouse" "is" "nice" "+")
The mouse does not chase the bear.
Unknown
inv-rconc
[@3: The mouse chases the bear.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule8 <- FAIL)]]
("mouse" "chases" "bear" "-")
The cat chases the bear.
Unknown
rconc
[@1: The cat chases the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "bear" "+")
The mouse does not see the bear.
Unknown
inv-random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bear is cold.[(triple1)] The bear sees the lion.[(triple2)] The bear sees the mouse.[(triple3)] The cat chases the mouse.[(triple4)] The cat is big.[(triple5)] The cat is kind.[(triple6)] The cat likes the bear.[(triple7)] The cat sees the lion.[(triple8)] The lion chases the cat.[(triple9 OR ((triple13) -> rule3))] The lion is kind.[(triple10)] The lion likes the bear.[(triple11)] The lion likes the mouse.[(triple12)] The lion sees the bear.[(triple13)] The lion sees the cat.[(triple14)] The lion sees the mouse.[(triple15)] The mouse sees the cat.[(triple16)] @1: The cat likes the cat.[(((triple6) -> rule8))] The cat likes the lion.[(((triple6) -> rule7))] The lion is big.[(((triple14) -> rule2))] The lion likes the cat.[(((triple10) -> rule8))] The lion likes the lion.[(((triple10) -> rule7))] The mouse is big.[(((triple16) -> rule2))] @2: The cat is nice.[(((((triple6) -> rule8)) -> rule5))] The lion is nice.[(((((triple10) -> rule8)) -> rule5))] @3: The lion chases the bear.[(((triple14 ((((triple10) -> rule8)) -> rule5)) -> rule4))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The cat is kind.
("cat" "is" "kind" "+")
triple6
The cat likes the bear.
("cat" "likes" "bear" "+")
triple7
The cat sees the lion.
("cat" "sees" "lion" "+")
triple8
The lion chases the cat.
("lion" "chases" "cat" "+")
triple9
((triple13) -> (rule3 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple10
The lion likes the bear.
("lion" "likes" "bear" "+")
triple11
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple12
The lion sees the bear.
("lion" "sees" "bear" "+")
triple13
The lion sees the cat.
("lion" "sees" "cat" "+")
triple14
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple15
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple16
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple6) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
((triple6) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((triple14) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
((triple10) -> (rule8 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple10) -> (rule7 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple16) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((((triple6) -> (rule8 % int2))) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((((triple10) -> (rule8 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion chases the bear.
("lion" "chases" "bear" "+")
((triple14 ((((triple10) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion likes the cat.
("lion" "likes" "cat" "+")
int3