Anne is blue. Anne is rough. Erin is blue. Erin is green. Erin is red. Erin is rough. Erin is young. All furry, red people are young. All red, young people are green. Blue people are quiet. If someone is green then they are red. Green people are rough. If Anne is blue then Anne is furry. Young, red people are quiet. If Anne is blue then Anne is green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
All furry, red people are young.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
All red, young people are green.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Anne is blue then Anne is furry.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "furry" "+"))
Young, red people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is blue then Anne is green.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "green" "+"))
Anne is rough.
True
1
proof
[(triple2 OR ((((triple1) -> rule8)) -> rule5))]
("Anne" "is" "rough" "+")
triple2
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is not green.
False
1
inv-proof
[(triple4 OR ((triple5 triple7) -> rule2))]
("Erin" "is" "green" "-")
triple4
((triple5 triple7) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
True
2
proof
[(((triple3) -> rule3) OR ((triple7 triple5) -> rule7) OR ((triple7 ((triple4) -> rule4)) -> rule7))]
("Erin" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 triple5) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((((triple1) -> rule6) ((((triple1) -> rule8)) -> rule4)) -> rule1) ((((triple1) -> rule8)) -> rule4)) -> rule7))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((((triple1) -> (rule6 % int5)) ((((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Anne is red.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("Anne" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("Anne" "is" "red" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule8)) -> rule4)) -> rule1))]
("Anne" "is" "young" "+")
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not young.
False
6
inv-proof
[(((((triple1) -> rule6) ((((triple1) -> rule8)) -> rule4)) -> rule1))]
("Anne" "is" "young" "-")
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
@0: Anne is blue.[(triple1)] Anne is rough.[(triple2 OR ((((triple1) -> rule8)) -> rule5))] Erin is blue.[(triple3)] Erin is green.[(triple4 OR ((triple5 triple7) -> rule2))] Erin is red.[(triple5 OR ((triple4) -> rule4))] Erin is rough.[(triple6 OR ((triple4) -> rule5) OR ((((triple5 triple7) -> rule2)) -> rule5))] Erin is young.[(triple7)] @1: Anne is furry.[(((triple1) -> rule6))] Anne is green.[(((triple1) -> rule8))] Anne is quiet.[(((triple1) -> rule3) OR ((((((triple1) -> rule6) ((((triple1) -> rule8)) -> rule4)) -> rule1) ((((triple1) -> rule8)) -> rule4)) -> rule7))] Erin is quiet.[(((triple3) -> rule3) OR ((triple7 triple5) -> rule7) OR ((triple7 ((triple4) -> rule4)) -> rule7))] @2: Anne is red.[(((((triple1) -> rule8)) -> rule4))] @3: Anne is young.[(((((triple1) -> rule6) ((((triple1) -> rule8)) -> rule4)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
((triple5 triple7) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple4) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple4) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple5 triple7) -> (rule2 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((((triple1) -> (rule6 % int5)) ((((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 triple5) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule6 % int4)) ((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4