Dave is blue. Dave is kind. Dave is round. If someone is blue then they are round. If someone is blue then they are quiet. If someone is kind and white then they are smart. If someone is quiet then they are smart. If someone is big then they are round. Smart people are white.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and white then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Dave is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule6))]
("Dave" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not white.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule6))]
("Dave" "is" "white" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
@0: Dave is blue.[(triple1)] Dave is kind.[(triple2)] Dave is round.[(triple3 OR ((triple1) -> rule1))] @1: Dave is quiet.[(((triple1) -> rule2))] @2: Dave is smart.[(((((triple1) -> rule2)) -> rule4))] @3: Dave is white.[(((((((triple1) -> rule2)) -> rule4)) -> rule6))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3