Dave is big. Dave is kind. Dave is nice. Nice, rough people are green. All kind people are green. White people are rough. If Dave is kind then Dave is white. All rough, big people are white. If someone is kind and rough then they are red.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Nice, rough people are green.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
White people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Dave is kind then Dave is white.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "white" "+"))
All rough, big people are white.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is kind and rough then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is white.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "white" "+")
((triple2) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "white" "-")
((triple2) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule6))]
("Dave" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule6))]
("Dave" "is" "red" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is nice.[(triple3)] @1: Dave is green.[(((triple2) -> rule2) OR ((triple3 ((((triple2) -> rule4)) -> rule3)) -> rule1))] Dave is white.[(((triple2) -> rule4))] @2: Dave is rough.[(((((triple2) -> rule4)) -> rule3))] @3: Dave is red.[(((triple2 ((((triple2) -> rule4)) -> rule3)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3