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