Dave is blue. Dave is cold. Dave is kind. Dave is nice. Dave is quiet. Dave is rough. Dave is round. Harry is blue. Harry is cold. Harry is nice. Harry is quiet. Harry is round. Quiet things are kind. Quiet, kind things are rough.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Quiet, kind things are rough.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Dave is round.
True
1
proof
[(triple7)]
("Dave" "is" "round" "+")
triple7
Harry is not quiet.
False
1
inv-proof
[(triple11)]
("Harry" "is" "quiet" "-")
triple11
Harry is kind.
True
2
proof
[(((triple11) -> rule1))]
("Harry" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "kind" "-")
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
True
4
proof
[(((triple11 ((triple11) -> rule1)) -> rule2))]
("Harry" "is" "rough" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((triple11 ((triple11) -> rule1)) -> rule2))]
("Harry" "is" "rough" "-")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is kind.[(triple3 OR ((triple5) -> rule1))] Dave is nice.[(triple4)] Dave is quiet.[(triple5)] Dave is rough.[(triple6 OR ((triple5 triple3) -> rule2) OR ((triple5 ((triple5) -> rule1)) -> rule2))] Dave is round.[(triple7)] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is nice.[(triple10)] Harry is quiet.[(triple11)] Harry is round.[(triple12)] @1: Harry is kind.[(((triple11) -> rule1))] @2: Harry is rough.[(((triple11 ((triple11) -> rule1)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple5) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
((triple5 triple3) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2