Anne is rough. Anne is round. Anne is smart. Anne is white. Anne is young. Charlie is kind. Charlie is rough. Charlie is round. Charlie is not white. Charlie is young. If Charlie is kind then Charlie is blue. If someone is rough then they are smart. If someone is blue and kind then they are smart. If Anne is rough then Anne is blue. If Anne is rough and Anne is young then Anne is round. If Charlie is not blue then Charlie is white.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is kind then Charlie is blue.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and kind then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Anne is rough then Anne is blue.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "blue" "+"))
If Anne is rough and Anne is young then Anne is round.
((("Anne" "is" "rough" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "round" "+"))
If Charlie is not blue then Charlie is white.
((("Charlie" "is" "blue" "~")) -> ("Charlie" "is" "white" "+"))
Charlie is young.
True
1
proof
[(triple10)]
("Charlie" "is" "young" "+")
triple10
Anne is not round.
False
1
inv-proof
[(triple2 OR ((triple1 triple5) -> rule5))]
("Anne" "is" "round" "-")
triple2
((triple1 triple5) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
@0: Anne is rough.[(triple1)] Anne is round.[(triple2 OR ((triple1 triple5) -> rule5))] Anne is smart.[(triple3 OR ((triple1) -> rule2))] Anne is white.[(triple4)] Anne is young.[(triple5)] Charlie is kind.[(triple6)] Charlie is not white.[(triple9)] Charlie is rough.[(triple7)] Charlie is round.[(triple8)] Charlie is young.[(triple10)] @1: Anne is blue.[(((triple1) -> rule4))] Charlie is blue.[(((triple6) -> rule1))] Charlie is smart.[(((triple7) -> rule2) OR ((((triple6) -> rule1) triple6) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
((triple1 triple5) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is kind.
("Charlie" "is" "kind" "+")
triple6
Charlie is not white.
("Charlie" "is" "white" "-")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple6) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2