Erin is green. Erin is kind. Erin is quiet. Erin is red. Erin is round. Erin is not white. Erin is not young. Gary is green. Gary is not kind. Gary is round. Gary is white. Gary is young. All young people are not kind. If Gary is not kind then Gary is not red. If someone is white and not red then they are quiet. If Erin is green and Erin is not kind then Erin is not quiet. If Gary is red and Gary is not quiet then Gary is round. All young, round people are green.
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is not white.
("Erin" "is" "white" "-")
Erin is not young.
("Erin" "is" "young" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All young people are not kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "-"))
If Gary is not kind then Gary is not red.
((("Gary" "is" "kind" "~")) -> ("Gary" "is" "red" "-"))
If someone is white and not red then they are quiet.
((("someone" "is" "white" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "quiet" "+"))
If Erin is green and Erin is not kind then Erin is not quiet.
((("Erin" "is" "green" "+") ("Erin" "is" "kind" "~")) -> ("Erin" "is" "quiet" "-"))
If Gary is red and Gary is not quiet then Gary is round.
((("Gary" "is" "red" "+") ("Gary" "is" "quiet" "~")) -> ("Gary" "is" "round" "+"))
All young, round people are green.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple4)]
("Erin" "is" "red" "-")
triple4
Gary is not red.
True
2
proof
[(((triple9) -> rule2) OR ((((triple12) -> rule1)) -> rule2))]
("Gary" "is" "red" "-")
((triple9) -> (rule2 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
int2
Gary is red.
False
2
inv-proof
[(((triple9) -> rule2) OR ((((triple12) -> rule1)) -> rule2))]
("Gary" "is" "red" "+")
((triple9) -> (rule2 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
int2
Gary is quiet.
True
4
proof
[(((triple11 ((triple9) -> rule2)) -> rule3) OR ((triple11 ((((triple12) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "+")
((triple11 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
int2
((triple11 ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
int3
Gary is not quiet.
False
4
inv-proof
[(((triple11 ((triple9) -> rule2)) -> rule3) OR ((triple11 ((((triple12) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "-")
((triple11 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
int2
((triple11 ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
int3
@0: Erin is green.[(triple1)] Erin is kind.[(triple2)] Erin is not white.[(triple6)] Erin is not young.[(triple7)] Erin is quiet.[(triple3)] Erin is red.[(triple4)] Erin is round.[(triple5)] Gary is green.[(triple8 OR ((triple12 triple10) -> rule6))] Gary is not kind.[(triple9 OR ((triple12) -> rule1))] Gary is round.[(triple10)] Gary is white.[(triple11)] Gary is young.[(triple12)] @1: Gary is not red.[(((triple9) -> rule2) OR ((((triple12) -> rule1)) -> rule2))] @2: Gary is quiet.[(((triple11 ((triple9) -> rule2)) -> rule3) OR ((triple11 ((((triple12) -> rule1)) -> rule2)) -> rule3))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is not white.
("Erin" "is" "white" "-")
triple6
Erin is not young.
("Erin" "is" "young" "-")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple8
((triple12 triple10) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
triple9
((triple12) -> (rule1 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Gary is not red.
("Gary" "is" "red" "-")
((triple9) -> (rule2 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple11 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
int2
((triple11 ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
int3