Anne is furry. Anne is quiet. Anne is red. Anne is rough. Anne is round. Anne is smart. Anne is young. Charlie is furry. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is round. Charlie is smart. Charlie is young. If something is young and quiet then it is furry. Furry things are round.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If something is young and quiet then it is furry.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Anne is furry.
True
1
proof
[(triple1 OR ((triple7 triple2) -> rule1))]
("Anne" "is" "furry" "+")
triple1
((triple7 triple2) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is not furry.
False
1
inv-proof
[(triple8 OR ((triple14 triple9) -> rule1))]
("Charlie" "is" "furry" "-")
triple8
((triple14 triple9) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
@0: Anne is furry.[(triple1 OR ((triple7 triple2) -> rule1))] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Anne is round.[(triple5 OR ((triple1) -> rule2) OR ((((triple7 triple2) -> rule1)) -> rule2))] Anne is smart.[(triple6)] Anne is young.[(triple7)] Charlie is furry.[(triple8 OR ((triple14 triple9) -> rule1))] Charlie is quiet.[(triple9)] Charlie is red.[(triple10)] Charlie is rough.[(triple11)] Charlie is round.[(triple12 OR ((triple8) -> rule2) OR ((((triple14 triple9) -> rule1)) -> rule2))] Charlie is smart.[(triple13)] Charlie is young.[(triple14)]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple7 triple2) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple7 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
((triple14 triple9) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
((triple8) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple14 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple13
Charlie is young.
("Charlie" "is" "young" "+")
triple14