Anne is blue. Anne is green. Anne is red. Anne is smart. Anne is white. Erin is blue. Erin is red. Erin is smart. Fiona is blue. Fiona is red. Fiona is smart. Fiona is white. If Anne is red and Anne is blue then Anne is quiet. Quiet people are smart. All smart, green people are blue. If someone is blue and smart then they are young. All red, young people are white. White, blue people are green. If Fiona is red and Fiona is green then Fiona is smart. If someone is young then they are quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Anne is red and Anne is blue then Anne is quiet.
((("Anne" "is" "red" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "quiet" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All smart, green people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and smart then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All red, young people are white.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
White, blue people are green.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Fiona is red and Fiona is green then Fiona is smart.
((("Fiona" "is" "red" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "smart" "+"))
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Fiona is red.
True
1
proof
[(triple10)]
("Fiona" "is" "red" "+")
triple10
Fiona is not smart.
False
1
inv-proof
[(triple11 OR ((triple10 ((triple12 triple9) -> rule6)) -> rule7))]
("Fiona" "is" "smart" "-")
triple11
((triple10 ((triple12 triple9) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is quiet.
True
3
proof
[(((triple3 triple1) -> rule1) OR ((((triple1 triple4) -> rule4)) -> rule8) OR ((triple3 ((triple4 triple2) -> rule3)) -> rule1) OR ((((((triple4 triple2) -> rule3) triple4) -> rule4)) -> rule8))]
("Anne" "is" "quiet" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1 triple4) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple3 ((triple4 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple4 triple2) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Fiona is not green.
False
3
inv-proof
[(((triple12 triple9) -> rule6) OR ((((triple10 ((triple9 triple11) -> rule4)) -> rule5) triple9) -> rule6))]
("Fiona" "is" "green" "-")
((triple12 triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple10 ((triple9 triple11) -> (rule4 % int3))) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is quiet.
True
4
proof
[(((((triple9 triple11) -> rule4)) -> rule8) OR ((((triple9 ((triple10 ((triple12 triple9) -> rule6)) -> rule7)) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "+")
((((triple9 triple11) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple9 ((triple10 ((triple12 triple9) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is not quiet.
False
4
inv-proof
[(((((triple9 triple11) -> rule4)) -> rule8) OR ((((triple9 ((triple10 ((triple12 triple9) -> rule6)) -> rule7)) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "-")
((((triple9 triple11) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple9 ((triple10 ((triple12 triple9) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Erin is green.
True
7
proof
[(((((triple7 ((triple6 triple8) -> rule4)) -> rule5) triple6) -> rule6))]
("Erin" "is" "green" "+")
((((triple7 ((triple6 triple8) -> (rule4 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not green.
False
7
inv-proof
[(((((triple7 ((triple6 triple8) -> rule4)) -> rule5) triple6) -> rule6))]
("Erin" "is" "green" "-")
((((triple7 ((triple6 triple8) -> (rule4 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
@0: Anne is blue.[(triple1 OR ((triple4 triple2) -> rule3))] Anne is green.[(triple2 OR ((triple5 triple1) -> rule6) OR ((((triple3 ((triple1 triple4) -> rule4)) -> rule5) triple1) -> rule6) OR ((((triple3 ((triple1 ((((triple3 triple1) -> rule1)) -> rule2)) -> rule4)) -> rule5) triple1) -> rule6))] Anne is red.[(triple3)] Anne is smart.[(triple4 OR ((((triple3 triple1) -> rule1)) -> rule2))] Anne is white.[(triple5 OR ((triple3 ((triple1 triple4) -> rule4)) -> rule5) OR ((triple3 ((((triple4 triple2) -> rule3) triple4) -> rule4)) -> rule5) OR ((triple3 ((triple1 ((((triple3 triple1) -> rule1)) -> rule2)) -> rule4)) -> rule5) OR ((triple3 ((((triple4 triple2) -> rule3) ((((triple3 triple1) -> rule1)) -> rule2)) -> rule4)) -> rule5))] Erin is blue.[(triple6)] Erin is red.[(triple7)] Erin is smart.[(triple8)] Fiona is blue.[(triple9)] Fiona is red.[(triple10)] Fiona is smart.[(triple11 OR ((triple10 ((triple12 triple9) -> rule6)) -> rule7))] Fiona is white.[(triple12 OR ((triple10 ((triple9 triple11) -> rule4)) -> rule5))] @1: Anne is quiet.[(((triple3 triple1) -> rule1) OR ((((triple1 triple4) -> rule4)) -> rule8) OR ((triple3 ((triple4 triple2) -> rule3)) -> rule1) OR ((((((triple4 triple2) -> rule3) triple4) -> rule4)) -> rule8))] Anne is young.[(((triple1 triple4) -> rule4) OR ((((triple4 triple2) -> rule3) triple4) -> rule4) OR ((triple1 ((((triple3 triple1) -> rule1)) -> rule2)) -> rule4) OR ((((triple4 triple2) -> rule3) ((((triple3 triple1) -> rule1)) -> rule2)) -> rule4))] Erin is young.[(((triple6 triple8) -> rule4))] Fiona is green.[(((triple12 triple9) -> rule6) OR ((((triple10 ((triple9 triple11) -> rule4)) -> rule5) triple9) -> rule6))] Fiona is young.[(((triple9 triple11) -> rule4) OR ((triple9 ((triple10 ((triple12 triple9) -> rule6)) -> rule7)) -> rule4))] @2: Erin is quiet.[(((((triple6 triple8) -> rule4)) -> rule8))] Erin is white.[(((triple7 ((triple6 triple8) -> rule4)) -> rule5))] Fiona is quiet.[(((((triple9 triple11) -> rule4)) -> rule8) OR ((((triple9 ((triple10 ((triple12 triple9) -> rule6)) -> rule7)) -> rule4)) -> rule8))] @3: Erin is green.[(((((triple7 ((triple6 triple8) -> rule4)) -> rule5) triple6) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple5 triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3 ((triple1 triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((triple3 ((triple1 ((((triple3 triple1) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
int5
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
((triple3 ((triple1 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple3 ((((triple4 triple2) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((triple3 ((triple1 ((((triple3 triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
((triple3 ((((triple4 triple2) -> (rule3 % int5)) ((((triple3 triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
((triple10 ((triple12 triple9) -> (rule6 % int2))) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((triple10 ((triple9 triple11) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1 triple4) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple3 ((triple4 triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple4 triple2) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((triple1 triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple4 triple2) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple1 ((((triple3 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((triple4 triple2) -> (rule3 % int4)) ((((triple3 triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((triple6 triple8) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple12 triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple10 ((triple9 triple11) -> (rule4 % int3))) -> (rule5 % int2)) triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((triple9 triple11) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple9 ((triple10 ((triple12 triple9) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple6 triple8) -> (rule4 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple7 ((triple6 triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple9 triple11) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple9 ((triple10 ((triple12 triple9) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
((((triple7 ((triple6 triple8) -> (rule4 % int3))) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3