Charlie is kind. Erin is cold. Fiona is quiet. If someone is green and furry then they are kind. If Fiona is round then Fiona is quiet. Furry, round people are blue. If someone is green then they are blue. Cold, quiet people are round. All kind people are round. All quiet, cold people are blue. If Charlie is blue and Charlie is green then Charlie is cold.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is green and furry then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is round then Fiona is quiet.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "quiet" "+"))
Furry, round people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Cold, quiet people are round.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All quiet, cold people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is blue and Charlie is green then Charlie is cold.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "cold" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "round" "+")
((triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "round" "-")
((triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "blue" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Charlie is kind.[(triple1)] Erin is cold.[(triple2)] Fiona is quiet.[(triple3)] @1: Charlie is round.[(((triple1) -> rule6))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1