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