Charlie is smart. Erin is quiet. If something is quiet then it is blue. If something is rough then it is quiet. Round things are smart. If something is rough then it is quiet. Furry, rough things are smart. If Charlie is furry and Charlie is smart then Charlie is blue.
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Furry, rough things are smart.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Charlie is furry and Charlie is smart then Charlie is blue.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "blue" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple2)]
("Erin" "is" "quiet" "-")
triple2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "smart" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is smart.[(triple1)] Erin is quiet.[(triple2)] @1: Erin is blue.[(((triple2) -> rule1))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1