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