Anne is smart. Charlie is quiet. Fiona is cold. All nice people are big. If Charlie is nice then Charlie is big. Nice people are green. All big people are nice. Cold people are smart. If someone is big then they are blue.
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Charlie is nice then Charlie is big.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "big" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Anne is smart.[(triple1)] Charlie is quiet.[(triple2)] Fiona is cold.[(triple3)] @1: Fiona is smart.[(((triple3) -> rule5))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1