Dave is blue. Dave is cold. Dave is quiet. Dave is red. Dave is rough. Dave is round. Dave is young. Quiet things are rough. All quiet, round things are blue. All rough things are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All quiet, round things are blue.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
@0: Dave is blue.[(triple1 OR ((triple5) -> rule3) OR ((triple3 triple6) -> rule2) OR ((((triple3) -> rule1)) -> rule3))] Dave is cold.[(triple2)] Dave is quiet.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5 OR ((triple3) -> rule1))] Dave is round.[(triple6)] Dave is young.[(triple7)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple5) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple3 triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7