Bob is green. Bob is kind. Bob is nice. Bob is smart. Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is round. Dave is smart. Gary is green. Gary is nice. Gary is quiet. Gary is red. Gary is smart. If Dave is green and Dave is red then Dave is kind. Kind, round people are red. If someone is round and smart then they are quiet. All nice, smart people are round. If Gary is quiet and Gary is smart then Gary is red. Round people are nice.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Dave is green and Dave is red then Dave is kind.
((("Dave" "is" "green" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "kind" "+"))
Kind, round people are red.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is round and smart then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All nice, smart people are round.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Gary is quiet and Gary is smart then Gary is red.
((("Gary" "is" "quiet" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "red" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple15 OR ((triple14 triple16) -> rule5) OR ((((((triple13 triple16) -> rule4) triple16) -> rule3) triple16) -> rule5))]
("Gary" "is" "red" "-")
triple15
((triple14 triple16) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((((triple13 triple16) -> (rule4 % int3)) triple16) -> (rule3 % int2)) triple16) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Bob is round.
True
3
proof
[(((triple3 triple4) -> rule4))]
("Bob" "is" "round" "+")
((triple3 triple4) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
3
inv-proof
[(((triple3 triple4) -> rule4))]
("Bob" "is" "round" "-")
((triple3 triple4) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
True
5
proof
[(((triple2 ((triple3 triple4) -> rule4)) -> rule2))]
("Bob" "is" "red" "+")
((triple2 ((triple3 triple4) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not quiet.
False
5
inv-proof
[(((((triple3 triple4) -> rule4) triple4) -> rule3))]
("Bob" "is" "quiet" "-")
((((triple3 triple4) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is nice.[(triple3)] Bob is smart.[(triple4)] Dave is green.[(triple5)] Dave is kind.[(triple6 OR ((triple5 triple9) -> rule1))] Dave is nice.[(triple7 OR ((triple10) -> rule6))] Dave is quiet.[(triple8 OR ((triple10 triple11) -> rule3) OR ((((triple7 triple11) -> rule4) triple11) -> rule3))] Dave is red.[(triple9 OR ((triple6 triple10) -> rule2) OR ((triple6 ((triple7 triple11) -> rule4)) -> rule2))] Dave is round.[(triple10 OR ((triple7 triple11) -> rule4))] Dave is smart.[(triple11)] Gary is green.[(triple12)] Gary is nice.[(triple13)] Gary is quiet.[(triple14 OR ((((triple13 triple16) -> rule4) triple16) -> rule3))] Gary is red.[(triple15 OR ((triple14 triple16) -> rule5) OR ((((((triple13 triple16) -> rule4) triple16) -> rule3) triple16) -> rule5))] Gary is smart.[(triple16)] @1: Bob is round.[(((triple3 triple4) -> rule4))] Gary is round.[(((triple13 triple16) -> rule4))] @2: Bob is quiet.[(((((triple3 triple4) -> rule4) triple4) -> rule3))] Bob is red.[(((triple2 ((triple3 triple4) -> rule4)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
((triple5 triple9) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple7
((triple10) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple10 triple11) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple7 triple11) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple6 triple10) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple6 ((triple7 triple11) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple10
((triple7 triple11) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Gary is green.
("Gary" "is" "green" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
((((triple13 triple16) -> (rule4 % int2)) triple16) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple15
((triple14 triple16) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((((triple13 triple16) -> (rule4 % int3)) triple16) -> (rule3 % int2)) triple16) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple16
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple4) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple13 triple16) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple3 triple4) -> (rule4 % int2)) triple4) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple2 ((triple3 triple4) -> (rule4 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2