The mouse is big. The mouse is green. The mouse is nice. The mouse is red. The mouse is young. If the mouse is nice and the mouse is big then the mouse is green. If the mouse is big then the mouse is green. If something is green and nice then it is red. If the mouse is green and the mouse is red then the mouse is young. If something is green then it is young. If something is nice and not green then it is young.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
If the mouse is nice and the mouse is big then the mouse is green.
((("mouse" "is" "nice" "+") ("mouse" "is" "big" "+")) -> ("mouse" "is" "green" "+"))
If the mouse is big then the mouse is green.
((("mouse" "is" "big" "+")) -> ("mouse" "is" "green" "+"))
If something is green and nice then it is red.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If the mouse is green and the mouse is red then the mouse is young.
((("mouse" "is" "green" "+") ("mouse" "is" "red" "+")) -> ("mouse" "is" "young" "+"))
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is nice and not green then it is young.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "+"))
The mouse is nice.
True
1
proof
[(triple3)]
("mouse" "is" "nice" "+")
triple3
The mouse is not green.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule2) OR ((triple3 triple1) -> rule1))]
("mouse" "is" "green" "-")
triple2
((triple1) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple3 triple1) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
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 mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is green.[(triple2 OR ((triple1) -> rule2) OR ((triple3 triple1) -> rule1))] The mouse is nice.[(triple3)] The mouse is red.[(triple4 OR ((triple2 triple3) -> rule3) OR ((((triple1) -> rule2) triple3) -> rule3) OR ((((triple3 triple1) -> rule1) triple3) -> rule3))] The mouse is young.[(triple5 OR ((triple2) -> rule5) OR ((triple2 triple4) -> rule4) OR ((((triple1) -> rule2)) -> rule5) OR ((((triple3 triple1) -> rule1)) -> rule5) OR ((triple2 ((triple2 triple3) -> rule3)) -> rule4) OR ((((triple1) -> rule2) triple4) -> rule4) OR ((((triple3 triple1) -> rule1) triple4) -> rule4) OR ((((triple1) -> rule2) ((triple2 triple3) -> rule3)) -> rule4) OR ((((triple3 triple1) -> rule1) ((triple2 triple3) -> rule3)) -> rule4) OR ((triple2 ((((triple1) -> rule2) triple3) -> rule3)) -> rule4) OR ((triple2 ((((triple3 triple1) -> rule1) triple3) -> rule3)) -> rule4) OR ((((triple1) -> rule2) ((((triple1) -> rule2) triple3) -> rule3)) -> rule4) OR ((((triple1) -> rule2) ((((triple3 triple1) -> rule1) triple3) -> rule3)) -> rule4) OR ((((triple3 triple1) -> rule1) ((((triple1) -> rule2) triple3) -> rule3)) -> rule4) OR ((((triple3 triple1) -> rule1) ((((triple3 triple1) -> rule1) triple3) -> rule3)) -> rule4))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
((triple1) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple3 triple1) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
((triple2 triple3) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple1) -> (rule2 % int2)) triple3) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple3 triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple2 triple4) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((triple2 ((triple2 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((((triple1) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple3 triple1) -> (rule1 % int2)) triple4) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple2 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((triple3 triple1) -> (rule1 % int3)) ((triple2 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((triple2 ((((triple1) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((triple2 ((((triple3 triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple3 triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((triple3 triple1) -> (rule1 % int3)) ((((triple1) -> (rule2 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
((((triple3 triple1) -> (rule1 % int3)) ((((triple3 triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3