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