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