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