Dave is white. If something is cold then it is round. All white, young things are nice. If Dave is white then Dave is cold. Kind, nice things are white. If something is cold and young then it is kind. All round things are young. If Dave is big then Dave is white. All kind, big things are round.
Dave is white.
("Dave" "is" "white" "+")
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All white, young things are nice.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Dave is white then Dave is cold.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "cold" "+"))
Kind, nice things are white.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is cold and young then it is kind.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If Dave is big then Dave is white.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "white" "+"))
All kind, big things are round.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Dave is white.
True
1
proof
[(triple1)]
("Dave" "is" "white" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is cold.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
@0: Dave is white.[(triple1)] @1: Dave is cold.[(((triple1) -> rule3))] @2: Dave is round.[(((((triple1) -> rule3)) -> rule1))] @3: Dave is young.[(((((((triple1) -> rule3)) -> rule1)) -> rule6))] @4: Dave is kind.[(((((triple1) -> rule3) ((((((triple1) -> rule3)) -> rule1)) -> rule6)) -> rule5))] Dave is nice.[(((triple1 ((((((triple1) -> rule3)) -> rule1)) -> rule6)) -> rule2))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int4)) ((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 ((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4