Dave is blue. Dave is cold. Dave is green. Dave is quiet. Dave is smart. Dave is white. Dave is young. All smart people are quiet. If Dave is green then Dave is blue. Blue, cold people are young.
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 smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is green then Dave is blue.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "blue" "+"))
Blue, cold people are young.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Dave is smart.
True
1
proof
[(triple5)]
("Dave" "is" "smart" "+")
triple5
Dave is not smart.
False
1
inv-proof
[(triple5)]
("Dave" "is" "smart" "-")
triple5
@0: Dave is blue.[(triple1 OR ((triple3) -> rule2))] Dave is cold.[(triple2)] Dave is green.[(triple3)] Dave is quiet.[(triple4 OR ((triple5) -> rule1))] Dave is smart.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7 OR ((triple1 triple2) -> rule3) OR ((((triple3) -> rule2) triple2) -> rule3))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple1 triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2