Bob is blue. Bob is cold. Bob is kind. Bob is quiet. Bob is red. Bob is not round. Bob is white. Charlie is blue. Charlie is cold. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is not round. Charlie is white. All quiet things are red. If something is kind then it is not round. If something is blue and not quiet then it is white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is white.
("Charlie" "is" "white" "+")
All quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is not round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "-"))
If something is blue and not quiet then it is white.
((("something" "is" "blue" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
Charlie is red.
True
1
proof
[(triple12 OR ((triple11) -> rule1))]
("Charlie" "is" "red" "+")
triple12
((triple11) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple3)]
("Bob" "is" "kind" "-")
triple3
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Bob is not round.[(triple6 OR ((triple3) -> rule2))] Bob is quiet.[(triple4)] Bob is red.[(triple5 OR ((triple4) -> rule1))] Bob is white.[(triple7)] Charlie is blue.[(triple8)] Charlie is cold.[(triple9)] Charlie is kind.[(triple10)] Charlie is not round.[(triple13 OR ((triple10) -> rule2))] Charlie is quiet.[(triple11)] Charlie is red.[(triple12 OR ((triple11) -> rule1))] Charlie is white.[(triple14)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not round.
("Bob" "is" "round" "-")
triple6
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple4) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is cold.
("Charlie" "is" "cold" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is not round.
("Charlie" "is" "round" "-")
triple13
((triple10) -> (rule2 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
Charlie is red.
("Charlie" "is" "red" "+")
triple12
((triple11) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple14