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