Anne is blue. Anne is cold. Anne is kind. Anne is red. Anne is smart. Bob is blue. Bob is not cold. Bob is kind. Bob is quiet. Bob is red. Bob is not smart. Bob is not young. If someone is smart and not cold then they are quiet. All smart people are quiet. If Bob is kind and Bob is smart then Bob is not quiet. If Bob is red and Bob is not cold then Bob is quiet. If Bob is kind and Bob is not cold then Bob is blue. If someone is cold and not red then they are not blue. If someone is kind and young then they are not blue. If someone is smart and not red then they are not young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not 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 smart.
("Bob" "is" "smart" "-")
Bob is not young.
("Bob" "is" "young" "-")
If someone is smart and not cold then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "quiet" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is kind and Bob is smart then Bob is not quiet.
((("Bob" "is" "kind" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "quiet" "-"))
If Bob is red and Bob is not cold then Bob is quiet.
((("Bob" "is" "red" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "quiet" "+"))
If Bob is kind and Bob is not cold then Bob is blue.
((("Bob" "is" "kind" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "blue" "+"))
If someone is cold and not red then they are not blue.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "blue" "-"))
If someone is kind and young then they are not blue.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "-"))
If someone is smart and not red then they are not young.
((("someone" "is" "smart" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "-"))
Bob is not smart.
True
1
proof
[(triple11)]
("Bob" "is" "smart" "-")
triple11
Bob is not blue.
False
1
inv-proof
[(triple6 OR ((triple8 triple7) -> rule5))]
("Bob" "is" "blue" "-")
triple6
((triple8 triple7) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Anne is quiet.
True
2
proof
[(((triple5) -> rule2))]
("Anne" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple5) -> rule2))]
("Anne" "is" "quiet" "-")
((triple5) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is red.[(triple4)] Anne is smart.[(triple5)] Bob is blue.[(triple6 OR ((triple8 triple7) -> rule5))] Bob is kind.[(triple8)] Bob is not cold.[(triple7)] Bob is not smart.[(triple11)] Bob is not young.[(triple12)] Bob is quiet.[(triple9 OR ((triple10 triple7) -> rule4))] Bob is red.[(triple10)] @1: Anne is quiet.[(((triple5) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
((triple8 triple7) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple8
Bob is not cold.
("Bob" "is" "cold" "-")
triple7
Bob is not smart.
("Bob" "is" "smart" "-")
triple11
Bob is not young.
("Bob" "is" "young" "-")
triple12
Bob is quiet.
("Bob" "is" "quiet" "+")
triple9
((triple10 triple7) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple5) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1