Anne is big. Anne is round. Fiona is round. Smart things are big. If something is big then it is kind. Red things are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is round.
("Anne" "is" "round" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not round.
False
1
inv-proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Anne is kind.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is round.[(triple2)] Fiona is round.[(triple3)] @1: Anne is kind.[(((triple1) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1