Dave is blue. Dave is cold. Dave is green. Dave is quiet. Dave is rough. Dave is not round. Gary is blue. Gary is green. Gary is kind. Gary is quiet. Gary is not rough. Gary is round. If something is kind and not round then it is green. If Dave is not round then Dave is kind.
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 not round.
("Dave" "is" "round" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is round.
("Gary" "is" "round" "+")
If something is kind and not round then it is green.
((("something" "is" "kind" "+") ("something" "is" "round" "~")) -> ("something" "is" "green" "+"))
If Dave is not round then Dave is kind.
((("Dave" "is" "round" "~")) -> ("Dave" "is" "kind" "+"))
Dave is green.
True
1
proof
[(triple3 OR ((((triple6) -> rule2) triple6) -> rule1))]
("Dave" "is" "green" "+")
triple3
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Gary is not round.
False
1
inv-proof
[(triple12)]
("Gary" "is" "round" "-")
triple12
Dave is kind.
True
2
proof
[(((triple6) -> rule2))]
("Dave" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple6) -> rule2))]
("Dave" "is" "kind" "-")
((triple6) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is green.[(triple3 OR ((((triple6) -> rule2) triple6) -> rule1))] Dave is not round.[(triple6)] Dave is quiet.[(triple4)] Dave is rough.[(triple5)] Gary is blue.[(triple7)] Gary is green.[(triple8)] Gary is kind.[(triple9)] Gary is not rough.[(triple11)] Gary is quiet.[(triple10)] Gary is round.[(triple12)] @1: Dave is kind.[(((triple6) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((((triple6) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is not rough.
("Gary" "is" "rough" "-")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1