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