Dave is big. Dave is blue. Dave is young. If something is big and round then it is kind. If something is big and young then it is nice. If something is furry then it is round. If Dave is nice then Dave is big. All big, blue things are round. If Dave is young then Dave is blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is big and round then it is kind.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is big and young then it is nice.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Dave is nice then Dave is big.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "big" "+"))
All big, blue things are round.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Dave is young then Dave is blue.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
@0: Dave is big.[(triple1)] Dave is blue.[(triple2 OR ((triple3) -> rule6))] Dave is young.[(triple3)] @1: Dave is nice.[(((triple1 triple3) -> rule2))] Dave is round.[(((triple1 triple2) -> rule5) OR ((triple1 ((triple3) -> rule6)) -> rule5))] @2: Dave is kind.[(((triple1 ((triple1 triple2) -> rule5)) -> rule1) OR ((triple1 ((triple1 ((triple3) -> rule6)) -> rule5)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple3) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple1 triple2) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 ((triple1 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple1 ((triple1 ((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3