Charlie is big. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is round. Charlie is white. Dave is not furry. Dave is kind. Dave is not quiet. Dave is round. Dave is white. If something is furry and white then it is kind. All furry, kind things are quiet. All kind things are white. Kind, round things are big. If something is round and big then it is nice. If something is white and not big then it is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If something is furry and white then it is kind.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
All furry, kind things are quiet.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Kind, round things are big.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is round and big then it is nice.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is white and not big then it is nice.
((("something" "is" "white" "+") ("something" "is" "big" "~")) -> ("something" "is" "nice" "+"))
Dave is round.
True
1
proof
[(triple11)]
("Dave" "is" "round" "+")
triple11
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Dave is big.
True
3
proof
[(((triple9 triple11) -> rule4))]
("Dave" "is" "big" "+")
((triple9 triple11) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
3
inv-proof
[(((triple9 triple11) -> rule4))]
("Dave" "is" "big" "-")
((triple9 triple11) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
True
5
proof
[(((triple11 ((triple9 triple11) -> rule4)) -> rule5))]
("Dave" "is" "nice" "+")
((triple11 ((triple9 triple11) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not nice.
False
5
inv-proof
[(((triple11 ((triple9 triple11) -> rule4)) -> rule5))]
("Dave" "is" "nice" "-")
((triple11 ((triple9 triple11) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
@0: Charlie is big.[(triple1 OR ((triple3 triple6) -> rule4) OR ((((triple2 triple7) -> rule1) triple6) -> rule4))] Charlie is furry.[(triple2)] Charlie is kind.[(triple3 OR ((triple2 triple7) -> rule1))] Charlie is nice.[(triple4 OR ((triple6 triple1) -> rule5) OR ((triple6 ((triple3 triple6) -> rule4)) -> rule5) OR ((triple6 ((((triple2 triple7) -> rule1) triple6) -> rule4)) -> rule5))] Charlie is quiet.[(triple5 OR ((triple2 triple3) -> rule2) OR ((triple2 ((triple2 triple7) -> rule1)) -> rule2))] Charlie is round.[(triple6)] Charlie is white.[(triple7 OR ((triple3) -> rule3))] Dave is kind.[(triple9)] Dave is not furry.[(triple8)] Dave is not quiet.[(triple10)] Dave is round.[(triple11)] Dave is white.[(triple12 OR ((triple9) -> rule3))] @1: Dave is big.[(((triple9 triple11) -> rule4))] @2: Dave is nice.[(((triple11 ((triple9 triple11) -> rule4)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3 triple6) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple2 triple7) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple2 triple7) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple6 triple1) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple6 ((triple3 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple6 ((((triple2 triple7) -> (rule1 % int3)) triple6) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple2 triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2 ((triple2 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple3) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is not furry.
("Dave" "is" "furry" "-")
triple8
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
((triple9) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple9 triple11) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple11 ((triple9 triple11) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2