Anne is smart. All big things are not white. If something is nice and not big then it is white. If something is blue then it is not round. Smart things are blue. Round things are nice. If Anne is blue and Anne is not nice then Anne is white.
Anne is smart.
("Anne" "is" "smart" "+")
All big things are not white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
If something is nice and not big then it is white.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "white" "+"))
If something is blue then it is not round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "-"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Anne is blue and Anne is not nice then Anne is white.
((("Anne" "is" "blue" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "white" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Anne is blue.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not round.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "round" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is smart.[(triple1)] @1: Anne is blue.[(((triple1) -> rule4))] @2: Anne is not round.[(((((triple1) -> rule4)) -> rule3))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not round.
("Anne" "is" "round" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2