Anne is not blue. Dave is big. Dave is blue. Dave is kind. Dave is not nice. Gary is not blue. Gary is cold. Gary is furry. Gary is red. Harry is not red. Furry, nice people are not blue. If someone is big and not nice then they are blue. If someone is red and cold then they are furry. All kind people are red. If Harry is furry then Harry is not blue. All blue, furry people are cold. All red, big people are not cold. Blue people are big.
Anne is not blue.
("Anne" "is" "blue" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is not red.
("Harry" "is" "red" "-")
Furry, nice people are not blue.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "-"))
If someone is big and not nice then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "blue" "+"))
If someone is red and cold then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Harry is furry then Harry is not blue.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "blue" "-"))
All blue, furry people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All red, big people are not cold.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple2 OR ((triple3) -> rule8))]
("Dave" "is" "big" "+")
triple2
((triple3) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is not red.
False
1
inv-proof
[(triple9)]
("Gary" "is" "red" "-")
triple9
Dave is red.
True
2
proof
[(((triple4) -> rule4))]
("Dave" "is" "red" "+")
((triple4) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple4) -> rule4))]
("Dave" "is" "red" "-")
((triple4) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not cold.
True
4
proof
[(((((triple4) -> rule4) triple2) -> rule7) OR ((((triple4) -> rule4) ((triple3) -> rule8)) -> rule7))]
("Dave" "is" "cold" "-")
((((triple4) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple4) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is cold.
False
4
inv-proof
[(((((triple4) -> rule4) triple2) -> rule7) OR ((((triple4) -> rule4) ((triple3) -> rule8)) -> rule7))]
("Dave" "is" "cold" "+")
((((triple4) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple4) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is not blue.[(triple1)] Dave is big.[(triple2 OR ((triple3) -> rule8))] Dave is blue.[(triple3 OR ((triple2 triple5) -> rule2))] Dave is kind.[(triple4)] Dave is not nice.[(triple5)] Gary is cold.[(triple7)] Gary is furry.[(triple8 OR ((triple9 triple7) -> rule3))] Gary is not blue.[(triple6)] Gary is red.[(triple9)] Harry is not red.[(triple10)] @1: Dave is red.[(((triple4) -> rule4))] @2: Dave is not cold.[(((((triple4) -> rule4) triple2) -> rule7) OR ((((triple4) -> rule4) ((triple3) -> rule8)) -> rule7))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
((triple3) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple3
((triple2 triple5) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is not nice.
("Dave" "is" "nice" "-")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple9 triple7) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple9
Harry is not red.
("Harry" "is" "red" "-")
triple10
Dave is red.
("Dave" "is" "red" "+")
((triple4) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
((((triple4) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple4) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3