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