Charlie is not big. Charlie is blue. Charlie is not green. Charlie is quiet. Charlie is smart. Charlie is white. Charlie is young. All young, big people are not smart. All big people are white. If Charlie is white and Charlie is quiet then Charlie is young. If Charlie is white then Charlie is quiet. If someone is blue and not young then they are green. If someone is young and not white then they are not green.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All young, big people are not smart.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "-"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Charlie is white and Charlie is quiet then Charlie is young.
((("Charlie" "is" "white" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "young" "+"))
If Charlie is white then Charlie is quiet.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "quiet" "+"))
If someone is blue and not young then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
If someone is young and not white then they are not green.
((("someone" "is" "young" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "green" "-"))
Charlie is quiet.
True
1
proof
[(triple4 OR ((triple6) -> rule4))]
("Charlie" "is" "quiet" "+")
triple4
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule4))]
("Charlie" "is" "quiet" "-")
triple4
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
@0: Charlie is blue.[(triple2)] Charlie is not big.[(triple1)] Charlie is not green.[(triple3)] Charlie is quiet.[(triple4 OR ((triple6) -> rule4))] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple6 triple4) -> rule3) OR ((triple6 ((triple6) -> rule4)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not green.
("Charlie" "is" "green" "-")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple6) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple6 triple4) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2