The mouse chases the tiger. The mouse needs the tiger. The mouse visits the tiger. The tiger chases the mouse. The tiger is rough. The tiger needs the mouse. The tiger visits the mouse. If someone visits the mouse then the mouse visits the tiger. If the tiger is kind then the tiger needs the mouse. If the tiger is rough then the tiger visits the mouse. If someone visits the mouse then they are green. If someone is kind then they need the mouse. If the mouse needs the tiger then the tiger chases the mouse. If someone needs the mouse then the mouse is green. If someone visits the tiger and they chase the mouse then the tiger is young.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone visits the mouse then the mouse visits the tiger.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If the tiger is kind then the tiger needs the mouse.
((("tiger" "is" "kind" "+")) -> ("tiger" "needs" "mouse" "+"))
If the tiger is rough then the tiger visits the mouse.
((("tiger" "is" "rough" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone visits the mouse then they are green.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "green" "+"))
If someone is kind then they need the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "mouse" "+"))
If the mouse needs the tiger then the tiger chases the mouse.
((("mouse" "needs" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone needs the mouse then the mouse is green.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If someone visits the tiger and they chase the mouse then the tiger is young.
((("someone" "visits" "tiger" "+") ("someone" "chases" "mouse" "+")) -> ("tiger" "is" "young" "+"))
The mouse needs the tiger.
True
1
proof
[(triple2)]
("mouse" "needs" "tiger" "+")
triple2
The mouse does not need the tiger.
False
1
inv-proof
[(triple2)]
("mouse" "needs" "tiger" "-")
triple2
The mouse is green.
True
2
proof
[(((triple6) -> rule7))]
("mouse" "is" "green" "+")
((triple6) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple7) -> rule4) OR ((((triple5) -> rule3)) -> rule4))]
("tiger" "is" "green" "-")
((triple7) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "young" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse needs the tiger.[(triple2)] The mouse visits the tiger.[(triple3 OR ((triple7) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] The tiger chases the mouse.[(triple4 OR ((triple2) -> rule6))] The tiger is rough.[(triple5)] The tiger needs the mouse.[(triple6)] The tiger visits the mouse.[(triple7 OR ((triple5) -> rule3))] @1: The mouse is green.[(((triple6) -> rule7))] The tiger is green.[(((triple7) -> rule4) OR ((((triple5) -> rule3)) -> rule4))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
((triple7) -> (rule1 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple4
((triple2) -> (rule6 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
triple5
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
((triple5) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((triple6) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple7) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2