The mouse is blue. The mouse is green. The mouse is kind. The mouse is rough. The mouse is young. All kind people are green. All kind people are young. If the mouse is kind then the mouse is rough. If the mouse is kind and the mouse is young then the mouse is blue. Green people are young. Green, blue people are kind. If the mouse is green then the mouse is rough. If the mouse is green then the mouse is blue.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If the mouse is kind then the mouse is rough.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "rough" "+"))
If the mouse is kind and the mouse is young then the mouse is blue.
((("mouse" "is" "kind" "+") ("mouse" "is" "young" "+")) -> ("mouse" "is" "blue" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Green, blue people are kind.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If the mouse is green then the mouse is rough.
((("mouse" "is" "green" "+")) -> ("mouse" "is" "rough" "+"))
If the mouse is green then the mouse is blue.
((("mouse" "is" "green" "+")) -> ("mouse" "is" "blue" "+"))
The mouse is young.
True
1
proof
[(triple5 OR ((triple2) -> rule5) OR ((triple3) -> rule2) OR ((((triple3) -> rule1)) -> rule5) OR ((((triple2 triple1) -> rule6)) -> rule2) OR ((((triple2 ((triple2) -> rule8)) -> rule6)) -> rule2))]
("mouse" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple2 triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse is not kind.
False
1
inv-proof
[(triple3 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule8)) -> rule6))]
("mouse" "is" "kind" "-")
triple3
((triple2 triple1) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is blue.[(triple1 OR ((triple2) -> rule8) OR ((triple3 triple5) -> rule4) OR ((((triple3) -> rule1)) -> rule8) OR ((triple3 ((triple2) -> rule5)) -> rule4) OR ((triple3 ((triple3) -> rule2)) -> rule4) OR ((triple3 ((((triple3) -> rule1)) -> rule5)) -> rule4))] The mouse is green.[(triple2 OR ((triple3) -> rule1))] The mouse is kind.[(triple3 OR ((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule8)) -> rule6))] The mouse is rough.[(triple4 OR ((triple2) -> rule7) OR ((triple3) -> rule3) OR ((((triple3) -> rule1)) -> rule7) OR ((((triple2 triple1) -> rule6)) -> rule3) OR ((((triple2 ((triple2) -> rule8)) -> rule6)) -> rule3))] The mouse is young.[(triple5 OR ((triple2) -> rule5) OR ((triple3) -> rule2) OR ((((triple3) -> rule1)) -> rule5) OR ((((triple2 triple1) -> rule6)) -> rule2) OR ((((triple2 ((triple2) -> rule8)) -> rule6)) -> rule2))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
((triple2) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple3 triple5) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple3 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((triple3 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((triple3 ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is green.
("mouse" "is" "green" "+")
triple2
((triple3) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
((triple2 triple1) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
((triple2) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple3) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple2 triple1) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple2 triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3