Dave is smart. Erin is rough. Fiona is rough. Harry is smart. If Harry is cold then Harry is rough. All rough things are quiet.
Dave is smart.
("Dave" "is" "smart" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is cold then Harry is rough.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "rough" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Harry is smart.
True
1
proof
[(triple4)]
("Harry" "is" "smart" "+")
triple4
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Erin is quiet.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
@0: Dave is smart.[(triple1)] Erin is rough.[(triple2)] Fiona is rough.[(triple3)] Harry is smart.[(triple4)] @1: Erin is quiet.[(((triple2) -> rule2))] Fiona is quiet.[(((triple3) -> rule2))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1