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