Dave is big. Dave is furry. Dave is not white. If Dave is red and Dave is not big then Dave is not quiet. All quiet, furry people are red. Furry people are quiet. Round people are not smart. Red people are smart. If someone is smart and not red then they are not round.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not white.
("Dave" "is" "white" "-")
If Dave is red and Dave is not big then Dave is not quiet.
((("Dave" "is" "red" "+") ("Dave" "is" "big" "~")) -> ("Dave" "is" "quiet" "-"))
All quiet, furry people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Round people are not smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "-"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not red then they are not round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "round" "-"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "+")
triple3
Dave is quiet.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("Dave" "is" "red" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not red.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("Dave" "is" "red" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
True
5
proof
[(((((((triple2) -> rule3) triple2) -> rule2)) -> rule5))]
("Dave" "is" "smart" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((((triple2) -> rule3) triple2) -> rule2)) -> rule5))]
("Dave" "is" "smart" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is not white.[(triple3)] @1: Dave is quiet.[(((triple2) -> rule3))] @2: Dave is red.[(((((triple2) -> rule3) triple2) -> rule2))] @3: Dave is smart.[(((((((triple2) -> rule3) triple2) -> rule2)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3