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