Anne is big. If something is rough then it is round. If something is green and rough then it is big. All big things are cold. Cold things are not green. If Anne is not round then Anne is cold. All big things are nice. If something is round and not green then it is nice. Nice, green things are not smart.
Anne is big.
("Anne" "is" "big" "+")
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is green and rough then it is big.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Cold things are not green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "-"))
If Anne is not round then Anne is cold.
((("Anne" "is" "round" "~")) -> ("Anne" "is" "cold" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is round and not green then it is nice.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "nice" "+"))
Nice, green things are not smart.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is nice.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not green.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is big.[(triple1)] @1: Anne is cold.[(((triple1) -> rule3))] Anne is nice.[(((triple1) -> rule6))] @2: Anne is not green.[(((((triple1) -> rule3)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2