The lion is green. The lion is kind. The lion needs the tiger. The lion visits the tiger. The mouse needs the tiger. The mouse sees the tiger. The tiger is cold. The tiger is not kind. The tiger does not need the mouse. The tiger sees the lion. The tiger sees the mouse. The tiger does not visit the mouse. If the mouse visits the tiger then the mouse is cold. All cold people are blue. If someone is round then they see the tiger. If someone visits the lion then they do not need the tiger. If someone sees the tiger and they visit the lion then they see the lion. If someone sees the tiger then they visit the tiger. If someone visits the mouse and they are blue then the mouse visits the tiger. If the lion does not need the mouse then the lion does not need the tiger.
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
If the mouse visits the tiger then the mouse is cold.
((("mouse" "visits" "tiger" "+")) -> ("mouse" "is" "cold" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is round then they see the tiger.
((("someone" "is" "round" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the lion then they do not need the tiger.
((("someone" "visits" "lion" "+")) -> ("someone" "needs" "tiger" "-"))
If someone sees the tiger and they visit the lion then they see the lion.
((("someone" "sees" "tiger" "+") ("someone" "visits" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the tiger then they visit the tiger.
((("someone" "sees" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the mouse and they are blue then the mouse visits the tiger.
((("someone" "visits" "mouse" "+") ("someone" "is" "blue" "+")) -> ("mouse" "visits" "tiger" "+"))
If the lion does not need the mouse then the lion does not need the tiger.
((("lion" "needs" "mouse" "~")) -> ("lion" "needs" "tiger" "-"))
The lion is green.
True
1
proof
[(triple1)]
("lion" "is" "green" "+")
triple1
The lion does not need the tiger.
False
1
inv-proof
[(triple3)]
("lion" "needs" "tiger" "-")
triple3
The tiger is blue.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "is" "blue" "+")
((triple7) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple7) -> rule2))]
("tiger" "is" "blue" "-")
((triple7) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The mouse is cold.
True
3
proof
[(((((triple6) -> rule6)) -> rule1))]
("mouse" "is" "cold" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is not cold.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule1))]
("mouse" "is" "cold" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is blue.
True
4
proof
[(((((((triple6) -> rule6)) -> rule1)) -> rule2))]
("mouse" "is" "blue" "+")
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The mouse is not blue.
False
4
inv-proof
[(((((((triple6) -> rule6)) -> rule1)) -> rule2))]
("mouse" "is" "blue" "-")
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "lion" "-")
The tiger visits the tiger.
Unknown
rconc
[@2: The tiger visits the tiger.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The lion does not see the tiger.
Unknown
inv-rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "tiger" "-")
The mouse sees the lion.
Unknown
rconc
[@1: The mouse sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "lion" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The lion does not visit the mouse.
Unknown
inv-random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The lion is green.[(triple1)] The lion is kind.[(triple2)] The lion needs the tiger.[(triple3)] The lion visits the tiger.[(triple4)] The mouse needs the tiger.[(triple5)] The mouse sees the tiger.[(triple6)] The tiger does not need the mouse.[(triple9)] The tiger does not visit the mouse.[(triple12)] The tiger is cold.[(triple7)] The tiger is not kind.[(triple8)] The tiger sees the lion.[(triple10)] The tiger sees the mouse.[(triple11)] @1: The mouse visits the tiger.[(((triple6) -> rule6))] The tiger is blue.[(((triple7) -> rule2))] @2: The mouse is cold.[(((((triple6) -> rule6)) -> rule1))] @3: The mouse is blue.[(((((((triple6) -> rule6)) -> rule1)) -> rule2))]
The lion is green.
("lion" "is" "green" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple4
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
triple9
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
triple12
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is not kind.
("tiger" "is" "kind" "-")
triple8
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple10
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple11
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple6) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple7) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3