Anne is big. Anne is blue. Anne is quiet. Anne is smart. Anne is not white. Bob is big. Bob is blue. Bob is kind. Bob is quiet. Bob is not red. Bob is smart. Bob is white. If someone is smart and quiet then they are big. All kind people are blue. Big people are not red.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
If someone is smart and quiet then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Big people are not red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "-"))
Bob is blue.
True
1
proof
[(triple7 OR ((triple8) -> rule2))]
("Bob" "is" "blue" "+")
triple7
((triple8) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not quiet.
False
1
inv-proof
[(triple9)]
("Bob" "is" "quiet" "-")
triple9
Anne is not red.
True
2
proof
[(((triple1) -> rule3) OR ((((triple4 triple3) -> rule1)) -> rule3))]
("Anne" "is" "red" "-")
((triple1) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple4 triple3) -> rule1)) -> rule3))]
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
@0: Anne is big.[(triple1 OR ((triple4 triple3) -> rule1))] Anne is blue.[(triple2)] Anne is not white.[(triple5)] Anne is quiet.[(triple3)] Anne is smart.[(triple4)] Bob is big.[(triple6 OR ((triple11 triple9) -> rule1))] Bob is blue.[(triple7 OR ((triple8) -> rule2))] Bob is kind.[(triple8)] Bob is not red.[(triple10 OR ((triple6) -> rule3) OR ((((triple11 triple9) -> rule1)) -> rule3))] Bob is quiet.[(triple9)] Bob is smart.[(triple11)] Bob is white.[(triple12)] @1: Anne is not red.[(((triple1) -> rule3) OR ((((triple4 triple3) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4 triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple6
((triple11 triple9) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple7
((triple8) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple8
Bob is not red.
("Bob" "is" "red" "-")
triple10
((triple6) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
((((triple11 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple9
Bob is smart.
("Bob" "is" "smart" "+")
triple11
Bob is white.
("Bob" "is" "white" "+")
triple12
Anne is not red.
("Anne" "is" "red" "-")
((triple1) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2