Charlie is blue. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is round. Charlie is young. Quiet people are round. If Charlie is blue then Charlie is young. Young people are blue.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Charlie is blue then Charlie is young.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "young" "+"))
Young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Charlie is young.
True
1
proof
[(triple7 OR ((triple1) -> rule2))]
("Charlie" "is" "young" "+")
triple7
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
@0: Charlie is blue.[(triple1 OR ((triple7) -> rule3))] Charlie is green.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4)] Charlie is red.[(triple5)] Charlie is round.[(triple6 OR ((triple4) -> rule1))] Charlie is young.[(triple7 OR ((triple1) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple7) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple4) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple1) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1