Anne is cold. Anne is furry. Anne is green. Dave is blue. Dave is cold. Dave is furry. Dave is nice. Dave is quiet. Dave is red. Erin is not blue. Erin is cold. Erin is green. Erin is quiet. Fiona is nice. Fiona is quiet. Cold, furry things are red. All furry, green things are red. All furry things are green. All cold things are green. Furry things are blue. If Anne is not cold then Anne is blue.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Cold, furry things are red.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All furry, green things are red.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If Anne is not cold then Anne is blue.
((("Anne" "is" "cold" "~")) -> ("Anne" "is" "blue" "+"))
Dave is cold.
True
1
proof
[(triple5)]
("Dave" "is" "cold" "+")
triple5
Erin is blue.
False
1
inv-proof
[(triple10)]
("Erin" "is" "blue" "+")
triple10
Anne is blue.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not red.
False
3
inv-proof
[(((triple1 triple2) -> rule1) OR ((triple2 triple3) -> rule2) OR ((triple2 ((triple1) -> rule4)) -> rule2) OR ((triple2 ((triple2) -> rule3)) -> rule2))]
("Anne" "is" "red" "-")
((triple1 triple2) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple3) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3 OR ((triple1) -> rule4) OR ((triple2) -> rule3))] Dave is blue.[(triple4 OR ((triple6) -> rule5))] Dave is cold.[(triple5)] Dave is furry.[(triple6)] Dave is nice.[(triple7)] Dave is quiet.[(triple8)] Dave is red.[(triple9 OR ((triple5 triple6) -> rule1) OR ((triple6 ((triple5) -> rule4)) -> rule2) OR ((triple6 ((triple6) -> rule3)) -> rule2))] Erin is cold.[(triple11)] Erin is green.[(triple12 OR ((triple11) -> rule4))] Erin is not blue.[(triple10)] Erin is quiet.[(triple13)] Fiona is nice.[(triple14)] Fiona is quiet.[(triple15)] @1: Anne is blue.[(((triple2) -> rule5))] Anne is red.[(((triple1 triple2) -> rule1) OR ((triple2 triple3) -> rule2) OR ((triple2 ((triple1) -> rule4)) -> rule2) OR ((triple2 ((triple2) -> rule3)) -> rule2))] Dave is green.[(((triple5) -> rule4) OR ((triple6) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple6) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple5 triple6) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple6 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple11
Erin is green.
("Erin" "is" "green" "+")
triple12
((triple11) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple13
Fiona is nice.
("Fiona" "is" "nice" "+")
triple14
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple15
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1 triple2) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple3) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple2 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple6) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1