Dave is round. If Dave is nice then Dave is white. If Dave is white and Dave is round then Dave is cold. All blue things are smart. Blue, round things are white. If something is cold and nice then it is smart. If something is round and quiet then it is cold. If Dave is round then Dave is blue. If Dave is cold then Dave is quiet.
Dave is round.
("Dave" "is" "round" "+")
If Dave is nice then Dave is white.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "white" "+"))
If Dave is white and Dave is round then Dave is cold.
((("Dave" "is" "white" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "cold" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Blue, round things are white.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If something is cold and nice then it is smart.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is round and quiet then it is cold.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Dave is round then Dave is blue.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "+"))
If Dave is cold then Dave is quiet.
((("Dave" "is" "cold" "+")) -> ("Dave" "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 blue.
True
2
proof
[(((triple1) -> rule7))]
("Dave" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "blue" "-")
((triple1) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
True
4
proof
[(((((triple1) -> rule7) triple1) -> rule4))]
("Dave" "is" "white" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
True
6
proof
[(((((((triple1) -> rule7) triple1) -> rule4) triple1) -> rule2))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not cold.
False
6
inv-proof
[(((((((triple1) -> rule7) triple1) -> rule4) triple1) -> rule2))]
("Dave" "is" "cold" "-")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
@0: Dave is round.[(triple1)] @1: Dave is blue.[(((triple1) -> rule7))] @2: Dave is smart.[(((((triple1) -> rule7)) -> rule3))] Dave is white.[(((((triple1) -> rule7) triple1) -> rule4))] @3: Dave is cold.[(((((((triple1) -> rule7) triple1) -> rule4) triple1) -> rule2))] @4: Dave is quiet.[(((((((((triple1) -> rule7) triple1) -> rule4) triple1) -> rule2)) -> rule8))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((((triple1) -> (rule7 % int4)) triple1) -> (rule4 % int3)) triple1) -> (rule2 % int2))) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4