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