Anne is cold. Anne is nice. Anne is smart. Anne is white. Bob is not big. Bob is blue. Bob is kind. Bob is nice. Bob is smart. Dave is blue. Dave is cold. Dave is kind. Harry is cold. Harry is kind. Harry is nice. Harry is not smart. If someone is kind then they are nice. If Harry is smart then Harry is white. If someone is kind and not nice then they are big. Big people are smart. If someone is cold and not nice then they are white. Blue, white people are cold. All kind people are cold. If someone is blue and not big then they are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Harry is smart then Harry is white.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "white" "+"))
If someone is kind and not nice then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "big" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and not nice then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "white" "+"))
Blue, white people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and not big then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "cold" "+"))
Anne is smart.
True
1
proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Harry is not cold.
False
1
inv-proof
[(triple13 OR ((triple14) -> rule7))]
("Harry" "is" "cold" "-")
triple13
((triple14) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2)] Anne is smart.[(triple3)] Anne is white.[(triple4)] Bob is blue.[(triple6)] Bob is kind.[(triple7)] Bob is nice.[(triple8 OR ((triple7) -> rule1))] Bob is not big.[(triple5)] Bob is smart.[(triple9)] Dave is blue.[(triple10)] Dave is cold.[(triple11 OR ((triple12) -> rule7))] Dave is kind.[(triple12)] Harry is cold.[(triple13 OR ((triple14) -> rule7))] Harry is kind.[(triple14)] Harry is nice.[(triple15 OR ((triple14) -> rule1))] Harry is not smart.[(triple16)] @1: Bob is cold.[(((triple7) -> rule7) OR ((triple6 triple5) -> rule8))] Dave is nice.[(((triple12) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
triple8
((triple7) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not big.
("Bob" "is" "big" "-")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple9
Dave is blue.
("Dave" "is" "blue" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple11
((triple12) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple14) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
((triple14) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
triple16
Bob is cold.
("Bob" "is" "cold" "+")
((triple7) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6 triple5) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple12) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1