Dave is blue. Dave is green. Dave is nice. Dave is red. Dave is round. Harry is blue. Harry is green. Harry is kind. Harry is nice. Harry is red. Harry is round. Harry is white. If something is nice then it is white. White things are kind.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
Dave is white.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "white" "+")
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "white" "-")
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Dave" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Dave" "is" "kind" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
@0: Dave is blue.[(triple1)] Dave is green.[(triple2)] Dave is nice.[(triple3)] Dave is red.[(triple4)] Dave is round.[(triple5)] Harry is blue.[(triple6)] Harry is green.[(triple7)] Harry is kind.[(triple8 OR ((triple12) -> rule2) OR ((((triple9) -> rule1)) -> rule2))] Harry is nice.[(triple9)] Harry is red.[(triple10)] Harry is round.[(triple11)] Harry is white.[(triple12 OR ((triple9) -> rule1))] @1: Dave is white.[(((triple3) -> rule1))] @2: Dave is kind.[(((((triple3) -> rule1)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple12) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is round.
("Harry" "is" "round" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple9) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2