Dave is cold. Dave is green. Dave is quiet. Dave is red. Harry is blue. Harry is cold. Harry is green. Harry is nice. Harry is red. Harry is smart. All green, blue people are nice. Red people are blue. If Dave is nice and Dave is red then Dave is smart.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All green, blue people are nice.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Dave is nice and Dave is red then Dave is smart.
((("Dave" "is" "nice" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "smart" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Dave is blue.
True
2
proof
[(((triple4) -> rule2))]
("Dave" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "blue" "-")
((triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
True
4
proof
[(((triple2 ((triple4) -> rule2)) -> rule1))]
("Dave" "is" "nice" "+")
((triple2 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple2 ((triple4) -> rule2)) -> rule1))]
("Dave" "is" "nice" "-")
((triple2 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
True
6
proof
[(((((triple2 ((triple4) -> rule2)) -> rule1) triple4) -> rule3))]
("Dave" "is" "smart" "+")
((((triple2 ((triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not smart.
False
6
inv-proof
[(((((triple2 ((triple4) -> rule2)) -> rule1) triple4) -> rule3))]
("Dave" "is" "smart" "-")
((((triple2 ((triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
@0: Dave is cold.[(triple1)] Dave is green.[(triple2)] Dave is quiet.[(triple3)] Dave is red.[(triple4)] Harry is blue.[(triple5 OR ((triple9) -> rule2))] Harry is cold.[(triple6)] Harry is green.[(triple7)] Harry is nice.[(triple8 OR ((triple7 triple5) -> rule1) OR ((triple7 ((triple9) -> rule2)) -> rule1))] Harry is red.[(triple9)] Harry is smart.[(triple10)] @1: Dave is blue.[(((triple4) -> rule2))] @2: Dave is nice.[(((triple2 ((triple4) -> rule2)) -> rule1))] @3: Dave is smart.[(((((triple2 ((triple4) -> rule2)) -> rule1) triple4) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
((triple9) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7 triple5) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple7 ((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2 ((triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3