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