The mouse is green. If something is rough then it is green. If something is big and young then it is green. If the mouse is young and the mouse is cold then the mouse is not green. If something is rough then it is cold. If the mouse is rough and the mouse is young then the mouse is not big. Cold things are not big. Young things are big. All green things are young.
The mouse is green.
("mouse" "is" "green" "+")
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is big and young then it is green.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If the mouse is young and the mouse is cold then the mouse is not green.
((("mouse" "is" "young" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "is" "green" "-"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If the mouse is rough and the mouse is young then the mouse is not big.
((("mouse" "is" "rough" "+") ("mouse" "is" "young" "+")) -> ("mouse" "is" "big" "-"))
Cold things are not big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "-"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
The mouse is green.
True
1
proof
[(triple1)]
("mouse" "is" "green" "+")
triple1
The mouse is not green.
False
1
inv-proof
[(triple1)]
("mouse" "is" "green" "-")
triple1
The mouse is young.
True
2
proof
[(((triple1) -> rule8))]
("mouse" "is" "young" "+")
((triple1) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple1) -> rule8))]
("mouse" "is" "young" "-")
((triple1) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is big.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("mouse" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is not big.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("mouse" "is" "big" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The mouse is green.[(triple1)] @1: The mouse is young.[(((triple1) -> rule8))] @2: The mouse is big.[(((((triple1) -> rule8)) -> rule7))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The mouse is young.
("mouse" "is" "young" "+")
((triple1) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2