Dave is nice. Dave is quiet. Dave is red. Dave is white. Gary is furry. Gary is quiet. Gary is red. All nice, red people are quiet. All quiet people are green. All nice, furry people are green. If someone is white and nice then they are furry. All green, red people are rough. If someone is quiet and furry then they are rough. Red, furry people are nice. If someone is quiet and nice then they are rough.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
All nice, red people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All nice, furry people are green.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is white and nice then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All green, red people are rough.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and furry then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Red, furry people are nice.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and nice then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Gary is furry.
True
1
proof
[(triple5)]
("Gary" "is" "furry" "+")
triple5
Gary is not red.
False
1
inv-proof
[(triple7)]
("Gary" "is" "red" "-")
triple7
Gary is green.
True
2
proof
[(((triple6) -> rule2) OR ((((triple7 triple5) -> rule7) triple5) -> rule3) OR ((((((triple7 triple5) -> rule7) triple7) -> rule1)) -> rule2))]
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple7 triple5) -> (rule7 % int2)) triple5) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple7 triple5) -> (rule7 % int3)) triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple1 triple3) -> rule1)) -> rule2) OR ((triple1 ((triple4 triple1) -> rule4)) -> rule3))]
("Dave" "is" "green" "-")
((triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple1 ((triple4 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
@0: Dave is nice.[(triple1)] Dave is quiet.[(triple2 OR ((triple1 triple3) -> rule1))] Dave is red.[(triple3)] Dave is white.[(triple4)] Gary is furry.[(triple5)] Gary is quiet.[(triple6 OR ((((triple7 triple5) -> rule7) triple7) -> rule1))] Gary is red.[(triple7)] @1: Dave is furry.[(((triple4 triple1) -> rule4))] Dave is green.[(((triple2) -> rule2) OR ((((triple1 triple3) -> rule1)) -> rule2) OR ((triple1 ((triple4 triple1) -> rule4)) -> rule3))] Dave is rough.[(((triple2 triple1) -> rule8) OR ((triple2 ((triple4 triple1) -> rule4)) -> rule6) OR ((((triple2) -> rule2) triple3) -> rule5) OR ((((triple1 triple3) -> rule1) triple1) -> rule8) OR ((((triple1 triple3) -> rule1) ((triple4 triple1) -> rule4)) -> rule6) OR ((((((triple1 triple3) -> rule1)) -> rule2) triple3) -> rule5) OR ((((triple1 ((triple4 triple1) -> rule4)) -> rule3) triple3) -> rule5))] Gary is green.[(((triple6) -> rule2) OR ((((triple7 triple5) -> rule7) triple5) -> rule3) OR ((((((triple7 triple5) -> rule7) triple7) -> rule1)) -> rule2))] Gary is nice.[(((triple7 triple5) -> rule7))] Gary is rough.[(((triple6 triple5) -> rule6) OR ((triple6 ((triple7 triple5) -> rule7)) -> rule8) OR ((((triple6) -> rule2) triple7) -> rule5) OR ((((((triple7 triple5) -> rule7) triple5) -> rule3) triple7) -> rule5) OR ((((((triple7 triple5) -> rule7) triple7) -> rule1) triple5) -> rule6) OR ((((((triple7 triple5) -> rule7) triple7) -> rule1) ((triple7 triple5) -> rule7)) -> rule8) OR ((((((((triple7 triple5) -> rule7) triple7) -> rule1)) -> rule2) triple7) -> rule5))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
((triple1 triple3) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
((((triple7 triple5) -> (rule7 % int2)) triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple7
Dave is furry.
("Dave" "is" "furry" "+")
((triple4 triple1) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((triple1 ((triple4 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple2 triple1) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple2 ((triple4 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple2) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple1 triple3) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple1 triple3) -> (rule1 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((((triple1 triple3) -> (rule1 % int3))) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
((((triple1 ((triple4 triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple7 triple5) -> (rule7 % int2)) triple5) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple7 triple5) -> (rule7 % int3)) triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple7 triple5) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6 triple5) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple6 ((triple7 triple5) -> (rule7 % int2))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple6) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((((triple7 triple5) -> (rule7 % int3)) triple5) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple7 triple5) -> (rule7 % int3)) triple7) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple7 triple5) -> (rule7 % int3)) triple7) -> (rule1 % int2)) ((triple7 triple5) -> (rule7 % int3))) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((((triple7 triple5) -> (rule7 % int4)) triple7) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4