Dave is blue. Dave is cold. Dave is green. Dave is quiet. Dave is rough. Dave is round. Dave is young. Harry is blue. Harry is cold. Harry is green. Harry is quiet. Harry is rough. Harry is round. Harry is young. If Harry is young then Harry is rough. Rough, cold people are round. If someone is round and quiet then they are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young then Harry is rough.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "rough" "+"))
Rough, cold people are round.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is round and quiet then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Dave is quiet.
True
1
proof
[(triple4)]
("Dave" "is" "quiet" "+")
triple4
Dave is not round.
False
1
inv-proof
[(triple6 OR ((triple5 triple2) -> rule2))]
("Dave" "is" "round" "-")
triple6
((triple5 triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
@0: Dave is blue.[(triple1 OR ((triple6 triple4) -> rule3) OR ((((triple5 triple2) -> rule2) triple4) -> rule3))] Dave is cold.[(triple2)] Dave is green.[(triple3)] Dave is quiet.[(triple4)] Dave is rough.[(triple5)] Dave is round.[(triple6 OR ((triple5 triple2) -> rule2))] Dave is young.[(triple7)] Harry is blue.[(triple8 OR ((triple13 triple11) -> rule3) OR ((((triple12 triple9) -> rule2) triple11) -> rule3) OR ((((((triple14) -> rule1) triple9) -> rule2) triple11) -> rule3))] Harry is cold.[(triple9)] Harry is green.[(triple10)] Harry is quiet.[(triple11)] Harry is rough.[(triple12 OR ((triple14) -> rule1))] Harry is round.[(triple13 OR ((triple12 triple9) -> rule2) OR ((((triple14) -> rule1) triple9) -> rule2))] Harry is young.[(triple14)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple6 triple4) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple5 triple2) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
((triple5 triple2) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple13 triple11) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple12 triple9) -> (rule2 % int2)) triple11) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple14) -> (rule1 % int3)) triple9) -> (rule2 % int2)) triple11) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
((triple14) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple12 triple9) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple14) -> (rule1 % int2)) triple9) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple14