The bear chases the lion. The bear is round. The cat is not cold. The cat needs the mouse. The lion is rough. The mouse chases the bear. The mouse is red. If something needs the lion and it is not blue then it does not need the mouse. If something chases the bear then the bear does not need the lion. If the lion likes the mouse then the mouse is cold. If something is cold then it does not chase the cat. If something is rough then it likes the mouse. If the bear chases the lion and the lion does not need the cat then the lion does not chase the mouse. If something likes the cat and it is not cold then it is not round. Red things are round.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is round.
("bear" "is" "round" "+")
The cat is not cold.
("cat" "is" "cold" "-")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is red.
("mouse" "is" "red" "+")
If something needs the lion and it is not blue then it does not need the mouse.
((("something" "needs" "lion" "+") ("something" "is" "blue" "~")) -> ("something" "needs" "mouse" "-"))
If something chases the bear then the bear does not need the lion.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "lion" "-"))
If the lion likes the mouse then the mouse is cold.
((("lion" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something is cold then it does not chase the cat.
((("something" "is" "cold" "+")) -> ("something" "chases" "cat" "-"))
If something is rough then it likes the mouse.
((("something" "is" "rough" "+")) -> ("something" "likes" "mouse" "+"))
If the bear chases the lion and the lion does not need the cat then the lion does not chase the mouse.
((("bear" "chases" "lion" "+") ("lion" "needs" "cat" "~")) -> ("lion" "chases" "mouse" "-"))
If something likes the cat and it is not cold then it is not round.
((("something" "likes" "cat" "+") ("something" "is" "cold" "~")) -> ("something" "is" "round" "-"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
The bear is round.
True
1
proof
[(triple2)]
("bear" "is" "round" "+")
triple2
The bear is not round.
False
1
inv-proof
[(triple2)]
("bear" "is" "round" "-")
triple2
The mouse is round.
True
2
proof
[(((triple7) -> rule8))]
("mouse" "is" "round" "+")
((triple7) -> (rule8 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The lion does not like the mouse.
False
2
inv-proof
[(((triple5) -> rule5))]
("lion" "likes" "mouse" "-")
((triple5) -> (rule5 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse is cold.
True
3
proof
[(((((triple5) -> rule5)) -> rule3))]
("mouse" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse is not cold.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule3))]
("mouse" "is" "cold" "-")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse does not chase the cat.
True
4
proof
[(((((((triple5) -> rule5)) -> rule3)) -> rule4))]
("mouse" "chases" "cat" "-")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse chases the cat.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule3)) -> rule4))]
("mouse" "chases" "cat" "+")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "mouse" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "round" "+")
The cat does not like the mouse.
Unknown
inv-rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The lion likes the bear.
Unknown
random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "+")
@0: The bear chases the lion.[(triple1)] The bear is round.[(triple2)] The cat is not cold.[(triple3)] The cat needs the mouse.[(triple4)] The lion is rough.[(triple5)] The mouse chases the bear.[(triple6)] The mouse is red.[(triple7)] @1: The bear does not need the lion.[(((triple6) -> rule2))] The lion likes the mouse.[(((triple5) -> rule5))] The mouse is round.[(((triple7) -> rule8))] @2: The mouse is cold.[(((((triple5) -> rule5)) -> rule3))] @3: The mouse does not chase the cat.[(((((((triple5) -> rule5)) -> rule3)) -> rule4))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The cat is not cold.
("cat" "is" "cold" "-")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The bear does not need the lion.
("bear" "needs" "lion" "-")
((triple6) -> (rule2 % int1))
The bear does not need the lion.
("bear" "needs" "lion" "-")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((triple5) -> (rule5 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple7) -> (rule8 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3