Charlie is big. Charlie is furry. Charlie is nice. If Charlie is rough then Charlie is quiet. All nice people are young. If someone is big and young then they are nice. Rough people are young. If Charlie is nice then Charlie is rough. All quiet, young people are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
If Charlie is rough then Charlie is quiet.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "quiet" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is big and young then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Charlie is nice then Charlie is rough.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "rough" "+"))
All quiet, young people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple3) -> rule5))]
("Charlie" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple3) -> rule5))]
("Charlie" "is" "rough" "-")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is nice.[(triple3)] @1: Charlie is rough.[(((triple3) -> rule5))] Charlie is young.[(((triple3) -> rule2) OR ((((triple3) -> rule5)) -> rule4))] @2: Charlie is quiet.[(((((triple3) -> rule5)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2