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