Anne is big. Anne is blue. Anne is green. Anne is round. Anne is smart. Anne is white. Anne is young. Bob is big. Bob is blue. Bob is green. Bob is round. Bob is smart. If someone is smart then they are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
If someone is smart then they are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Anne is round.
True
1
proof
[(triple4)]
("Anne" "is" "round" "+")
triple4
Bob is not green.
False
1
inv-proof
[(triple10)]
("Bob" "is" "green" "-")
triple10
Bob is white.
True
2
proof
[(((triple12) -> rule1))]
("Bob" "is" "white" "+")
((triple12) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple12) -> rule1))]
("Bob" "is" "white" "-")
((triple12) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is green.[(triple3)] Anne is round.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple5) -> rule1))] Anne is young.[(triple7)] Bob is big.[(triple8)] Bob is blue.[(triple9)] Bob is green.[(triple10)] Bob is round.[(triple11)] Bob is smart.[(triple12)] @1: Bob is white.[(((triple12) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple5) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
triple8
Bob is blue.
("Bob" "is" "blue" "+")
triple9
Bob is green.
("Bob" "is" "green" "+")
triple10
Bob is round.
("Bob" "is" "round" "+")
triple11
Bob is smart.
("Bob" "is" "smart" "+")
triple12
Bob is white.
("Bob" "is" "white" "+")
((triple12) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1