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