The mouse chases the tiger. The mouse eats the tiger. The mouse is nice. The mouse is round. The mouse likes the tiger. The tiger is kind. The tiger likes the mouse. If someone is nice and they do not chase the tiger then the tiger is not kind. If someone chases the tiger then the tiger is green. If the mouse likes the tiger then the mouse is kind. If the tiger is rough then the tiger chases the mouse. If someone is rough then they like the mouse. Kind people are rough. If someone likes the mouse and they are not green then they are kind. If someone eats the tiger then they are kind.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If someone is nice and they do not chase the tiger then the tiger is not kind.
((("someone" "is" "nice" "+") ("someone" "chases" "tiger" "~")) -> ("tiger" "is" "kind" "-"))
If someone chases the tiger then the tiger is green.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If the mouse likes the tiger then the mouse is kind.
((("mouse" "likes" "tiger" "+")) -> ("mouse" "is" "kind" "+"))
If the tiger is rough then the tiger chases the mouse.
((("tiger" "is" "rough" "+")) -> ("tiger" "chases" "mouse" "+"))
If someone is rough then they like the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "mouse" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the mouse and they are not green then they are kind.
((("someone" "likes" "mouse" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
If someone eats the tiger then they are kind.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "kind" "+"))
The mouse eats the tiger.
True
1
proof
[(triple2)]
("mouse" "eats" "tiger" "+")
triple2
The mouse is not nice.
False
1
inv-proof
[(triple3)]
("mouse" "is" "nice" "-")
triple3
The tiger is green.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "is" "green" "+")
((triple1) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "is" "green" "-")
((triple1) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger chases the mouse.
True
3
proof
[(((((triple6) -> rule6)) -> rule4))]
("tiger" "chases" "mouse" "+")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger does not chase the mouse.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule4))]
("tiger" "chases" "mouse" "-")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The mouse likes the mouse.
True
4
proof
[(((((((triple2) -> rule8)) -> rule6)) -> rule5) OR ((((((triple5) -> rule3)) -> rule6)) -> rule5))]
("mouse" "likes" "mouse" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse does not like the mouse.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule6)) -> rule5) OR ((((((triple5) -> rule3)) -> rule6)) -> rule5))]
("mouse" "likes" "mouse" "-")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
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 tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger does not eat the mouse.
Unknown
inv-random
[@0: The tiger eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "mouse" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is nice.[(triple3)] The mouse is round.[(triple4)] The mouse likes the tiger.[(triple5)] The tiger is kind.[(triple6)] The tiger likes the mouse.[(triple7 OR ((((triple6) -> rule6)) -> rule5))] @1: The mouse is kind.[(((triple2) -> rule8) OR ((triple5) -> rule3))] The tiger is green.[(((triple1) -> rule2))] The tiger is rough.[(((triple6) -> rule6))] @2: The mouse is rough.[(((((triple2) -> rule8)) -> rule6) OR ((((triple5) -> rule3)) -> rule6))] The tiger chases the mouse.[(((((triple6) -> rule6)) -> rule4))] @3: The mouse likes the mouse.[(((((((triple2) -> rule8)) -> rule6)) -> rule5) OR ((((((triple5) -> rule3)) -> rule6)) -> rule5))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple7
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((triple5) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple1) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple6) -> (rule6 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3