Anne is furry. Harry is green. Harry is white. All smart, furry people are rough. If Anne is not smart then Anne is blue. Blue people are not furry. If Harry is furry and Harry is rough then Harry is smart. Furry people are green. Furry, green people are not cold. If Anne is rough and Anne is white then Anne is cold. If someone is furry and not rough then they are white.
Anne is furry.
("Anne" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, furry people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Anne is not smart then Anne is blue.
((("Anne" "is" "smart" "~")) -> ("Anne" "is" "blue" "+"))
Blue people are not furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "-"))
If Harry is furry and Harry is rough then Harry is smart.
((("Harry" "is" "furry" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "smart" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Furry, green people are not cold.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
If Anne is rough and Anne is white then Anne is cold.
((("Anne" "is" "rough" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "cold" "+"))
If someone is furry and not rough then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "white" "+"))
Harry is green.
True
1
proof
[(triple2)]
("Harry" "is" "green" "+")
triple2
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is green.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "green" "-")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not cold.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "cold" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "cold" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is furry.[(triple1)] Harry is green.[(triple2)] Harry is white.[(triple3)] @1: Anne is green.[(((triple1) -> rule5))] @2: Anne is not cold.[(((triple1 ((triple1) -> rule5)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
int2