Dave is big. Dave is blue. Dave is green. Dave is quiet. Dave is red. Dave is rough. Gary is big. Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is young. If Gary is quiet and Gary is blue then Gary is green. If something is red then it is blue. If something is blue and quiet then it is red.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is quiet and Gary is blue then Gary is green.
((("Gary" "is" "quiet" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "green" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is blue and quiet then it is red.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Gary is young.
True
1
proof
[(triple12)]
("Gary" "is" "young" "+")
triple12
Gary is not quiet.
False
1
inv-proof
[(triple9)]
("Gary" "is" "quiet" "-")
triple9
@0: Dave is big.[(triple1)] Dave is blue.[(triple2 OR ((triple5) -> rule2))] Dave is green.[(triple3)] Dave is quiet.[(triple4)] Dave is red.[(triple5 OR ((triple2 triple4) -> rule3))] Dave is rough.[(triple6)] Gary is big.[(triple7)] Gary is green.[(triple8 OR ((triple9 ((triple10) -> rule2)) -> rule1))] Gary is quiet.[(triple9)] Gary is red.[(triple10)] Gary is rough.[(triple11)] Gary is young.[(triple12)] @1: Gary is blue.[(((triple10) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple5) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple2 triple4) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple9 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
((triple10) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1