Charlie is blue. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is white. Gary is blue. Gary is not furry. Gary is kind. Gary is nice. Gary is quiet. Gary is red. Gary is white. If something is blue and not red then it is furry. If Charlie is red then Charlie is nice. If Charlie is furry then Charlie is nice. If Gary is nice and Gary is white then Gary is not furry. If Gary is blue and Gary is furry then Gary is white. If something is quiet then it is white. If something is nice then it is blue. If Charlie is furry and Charlie is not nice then Charlie is white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is blue and not red then it is furry.
((("something" "is" "blue" "+") ("something" "is" "red" "~")) -> ("something" "is" "furry" "+"))
If Charlie is red then Charlie is nice.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is furry then Charlie is nice.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "nice" "+"))
If Gary is nice and Gary is white then Gary is not furry.
((("Gary" "is" "nice" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "furry" "-"))
If Gary is blue and Gary is furry then Gary is white.
((("Gary" "is" "blue" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "white" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Charlie is furry and Charlie is not nice then Charlie is white.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "white" "+"))
Gary is nice.
True
1
proof
[(triple11)]
("Gary" "is" "nice" "+")
triple11
Charlie is not nice.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule3) OR ((triple6) -> rule2))]
("Charlie" "is" "nice" "-")
triple4
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
@0: Charlie is blue.[(triple1 OR ((triple4) -> rule7) OR ((((triple2) -> rule3)) -> rule7) OR ((((triple6) -> rule2)) -> rule7))] Charlie is furry.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4 OR ((triple2) -> rule3) OR ((triple6) -> rule2))] Charlie is quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is white.[(triple7 OR ((triple5) -> rule6))] Gary is blue.[(triple8 OR ((triple11) -> rule7))] Gary is kind.[(triple10)] Gary is nice.[(triple11)] Gary is not furry.[(triple9 OR ((triple11 triple14) -> rule4) OR ((triple11 ((triple12) -> rule6)) -> rule4))] Gary is quiet.[(triple12)] Gary is red.[(triple13)] Gary is white.[(triple14 OR ((triple12) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple4) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple5) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
((triple11) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is not furry.
("Gary" "is" "furry" "-")
triple9
((triple11 triple14) -> (rule4 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
((triple11 ((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14
((triple12) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1