Anne is round. Dave is furry. Fiona is furry. Harry is furry. All nice things are cold. Furry things are cold. All green things are cold. If something is green and not round then it is furry. Green things are not furry. If Fiona is green and Fiona is cold then Fiona is smart. If something is nice then it is green. Cold, furry things are not nice.
Anne is round.
("Anne" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is green and not round then it is furry.
((("something" "is" "green" "+") ("something" "is" "round" "~")) -> ("something" "is" "furry" "+"))
Green things are not furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "-"))
If Fiona is green and Fiona is cold then Fiona is smart.
((("Fiona" "is" "green" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "smart" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Cold, furry things are not nice.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "-"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Fiona is not furry.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "furry" "-")
triple3
Dave is cold.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is not nice.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule8))]
("Dave" "is" "nice" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Harry is nice.
False
4
inv-proof
[(((((triple4) -> rule2) triple4) -> rule8))]
("Harry" "is" "nice" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule8 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Fiona" "is" "smart" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "green" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is round.[(triple1)] Dave is furry.[(triple2)] Fiona is furry.[(triple3)] Harry is furry.[(triple4)] @1: Dave is cold.[(((triple2) -> rule2))] Fiona is cold.[(((triple3) -> rule2))] Harry is cold.[(((triple4) -> rule2))] @2: Dave is not nice.[(((((triple2) -> rule2) triple2) -> rule8))] Fiona is not nice.[(((((triple3) -> rule2) triple3) -> rule8))] Harry is not nice.[(((((triple4) -> rule2) triple4) -> rule8))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule8 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((((triple4) -> (rule2 % int2)) triple4) -> (rule8 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2