The mouse is green. The mouse is rough. The mouse needs the tiger. The tiger is red. The tiger is round. The tiger likes the mouse. The tiger sees the mouse. If the mouse needs the tiger and the tiger sees the mouse then the mouse is green. If something is red and it needs the tiger then it likes the mouse. If something sees the mouse then it is green. If something needs the tiger then the tiger is red. If something is round and it likes the mouse then it sees the tiger. If the mouse likes the tiger then the mouse is round. If something likes the mouse then the mouse is red. If the tiger is round then the tiger needs the mouse.
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the mouse needs the tiger and the tiger sees the mouse then the mouse is green.
((("mouse" "needs" "tiger" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something is red and it needs the tiger then it likes the mouse.
((("something" "is" "red" "+") ("something" "needs" "tiger" "+")) -> ("something" "likes" "mouse" "+"))
If something sees the mouse then it is green.
((("something" "sees" "mouse" "+")) -> ("something" "is" "green" "+"))
If something needs the tiger then the tiger is red.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something is round and it likes the mouse then it sees the tiger.
((("something" "is" "round" "+") ("something" "likes" "mouse" "+")) -> ("something" "sees" "tiger" "+"))
If the mouse likes the tiger then the mouse is round.
((("mouse" "likes" "tiger" "+")) -> ("mouse" "is" "round" "+"))
If something likes the mouse then the mouse is red.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If the tiger is round then the tiger needs the mouse.
((("tiger" "is" "round" "+")) -> ("tiger" "needs" "mouse" "+"))
The tiger is red.
True
1
proof
[(triple4 OR ((triple3) -> rule4))]
("tiger" "is" "red" "+")
triple4
((triple3) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The mouse is not green.
False
1
inv-proof
[(triple1 OR ((triple3 triple7) -> rule1))]
("mouse" "is" "green" "-")
triple1
((triple3 triple7) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger needs the mouse.
True
2
proof
[(((triple5) -> rule8))]
("tiger" "needs" "mouse" "+")
((triple5) -> (rule8 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple7) -> rule3))]
("tiger" "is" "green" "-")
((triple7) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The mouse likes the mouse.
True
4
proof
[(((((triple6) -> rule7) triple3) -> rule2))]
("mouse" "likes" "mouse" "+")
((((triple6) -> (rule7 % int2)) triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not like the mouse.
False
4
inv-proof
[(((((triple6) -> rule7) triple3) -> rule2))]
("mouse" "likes" "mouse" "-")
((((triple6) -> (rule7 % int2)) triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "round" "-")
The mouse sees the tiger.
Unknown
rconc
[@2: The mouse sees the tiger.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("mouse" "sees" "tiger" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The mouse is green.[(triple1 OR ((triple3 triple7) -> rule1))] The mouse is rough.[(triple2)] The mouse needs the tiger.[(triple3)] The tiger is red.[(triple4 OR ((triple3) -> rule4))] The tiger is round.[(triple5)] The tiger likes the mouse.[(triple6)] The tiger sees the mouse.[(triple7)] @1: The mouse is red.[(((triple6) -> rule7))] The tiger is green.[(((triple7) -> rule3))] The tiger needs the mouse.[(((triple5) -> rule8))] The tiger sees the tiger.[(((triple5 triple6) -> rule5))] @2: The mouse likes the mouse.[(((((triple6) -> rule7) triple3) -> rule2))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
((triple3 triple7) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
((triple3) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple5
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
((triple6) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple7) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((triple5) -> (rule8 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple5 triple6) -> (rule5 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple6) -> (rule7 % int2)) triple3) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2