Bob is cold. Charlie is cold. Dave is cold. Harry is rough. All green, cold things are big. If Bob is rough and Bob is green then Bob is big. Blue things are big. Blue, furry things are big. All rough things are cold. All green, nice things are furry.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All green, cold things are big.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Bob is rough and Bob is green then Bob is big.
((("Bob" "is" "rough" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "big" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Blue, furry things are big.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
All green, nice things are furry.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple4)]
("Harry" "is" "rough" "-")
triple4
Harry is cold.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "cold" "-")
((triple4) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is cold.[(triple1)] Charlie is cold.[(triple2)] Dave is cold.[(triple3)] Harry is rough.[(triple4)] @1: Harry is cold.[(((triple4) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1