The mouse chases the tiger. The mouse eats the tiger. The mouse is big. The mouse is kind. The mouse is nice. The mouse is red. The mouse needs the tiger. The tiger is big. The tiger is kind. The tiger needs the mouse. If the mouse eats the tiger and the mouse chases the tiger then the mouse is rough. If someone chases the tiger and the tiger chases the mouse then the tiger needs the mouse. If someone is rough then they need the mouse. If someone is nice then they chase the mouse. If someone is nice then they chase the mouse. If someone is rough and they chase the mouse then they chase the tiger.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If the mouse eats the tiger and the mouse chases the tiger then the mouse is rough.
((("mouse" "eats" "tiger" "+") ("mouse" "chases" "tiger" "+")) -> ("mouse" "is" "rough" "+"))
If someone chases the tiger and the tiger chases the mouse then the tiger needs the mouse.
((("someone" "chases" "tiger" "+") ("tiger" "chases" "mouse" "+")) -> ("tiger" "needs" "mouse" "+"))
If someone is rough then they need the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is nice then they chase the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is nice then they chase the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is rough and they chase the mouse then they chase the tiger.
((("someone" "is" "rough" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "chases" "tiger" "+"))
The mouse needs the tiger.
True
1
proof
[(triple7)]
("mouse" "needs" "tiger" "+")
triple7
The tiger does not need the mouse.
False
1
inv-proof
[(triple10)]
("tiger" "needs" "mouse" "-")
triple10
The mouse chases the mouse.
True
2
proof
[(((triple5) -> rule4) OR ((triple5) -> rule5))]
("mouse" "chases" "mouse" "+")
((triple5) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((triple5) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is not rough.
False
3
inv-proof
[(((triple2 triple1) -> rule1))]
("mouse" "is" "rough" "-")
((triple2 triple1) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the mouse.
True
4
proof
[(((((triple2 triple1) -> rule1)) -> rule3))]
("mouse" "needs" "mouse" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not need the mouse.
False
4
inv-proof
[(((((triple2 triple1) -> rule1)) -> rule3))]
("mouse" "needs" "mouse" "-")
((((triple2 triple1) -> (rule1 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
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 tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is big.[(triple3)] The mouse is kind.[(triple4)] The mouse is nice.[(triple5)] The mouse is red.[(triple6)] The mouse needs the tiger.[(triple7)] The tiger is big.[(triple8)] The tiger is kind.[(triple9)] The tiger needs the mouse.[(triple10)] @1: The mouse chases the mouse.[(((triple5) -> rule4) OR ((triple5) -> rule5))] The mouse is rough.[(((triple2 triple1) -> rule1))] @2: The mouse needs the mouse.[(((((triple2 triple1) -> rule1)) -> rule3))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple10
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple5) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((triple5) -> (rule5 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple2 triple1) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule3 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2